7 Certified paths as a category
On this page · Permalink · Source line 522
The hypergraph model records local justifications. A complementary construction treats complete certified transformations as morphisms. It uses the usual category of paths [7].
Definition 7.1: Certified proof category
Fix a directed graph of typed mathematical states and certified primitive transformations. Its path category \(\mathsf{Cert}\) has these states as objects and finite composable paths as morphisms. The empty path is an identity, and composition is concatenation. One may further identify paths by a declared congruence compatible with concatenation. Associativity and the identity laws then hold by construction.
A state may be a proposition, a diagram, an exact finite computation, a coordinate representation, or a structured collection of claims. Candidate analogies may live in a larger discovery graph, but they do not enter \(\mathsf{Cert}\) until their logical force and domain have been certified.
Proposition 7.2: Functorial transport
Let \(F:\mathsf{Cert}_1\to\mathsf{Cert}_2\) be a functor. If
is a certified path in \(\mathsf{Cert}_1\), then
is a certified path in \(\mathsf{Cert}_2\).
Proof
A functor maps objects to objects and morphisms to morphisms. It preserves identities and composition. The image of the composite path is therefore the composite of the image morphisms, which is certified in the target category.
The proposition transports certification inside the two declared categories. To interpret that transport as preservation of a mathematical judgment, the target category and functor must also have sound interpretations of their objects and rules. These requirements cannot be inferred merely from the word functor. Under that contract, different representations can preserve a judgment while exposing different features of its argument. The category language is standard [7].
Definition 7.3: Compositional certificate map
A compositional certificate map is a functor
that sends expanded certified paths to checkable certificate paths and preserves identity and composition.
Proposition 7.4: Local audit composes
If every primitive morphism in a finite path has an auditable certificate and the certificate map is compositional, then the composite path is auditable from the primitive certificates and the declared composition rules.
Proof
Proceed by induction on path length. The length-zero case is an identity. Assume the first \(r\) morphisms have an auditable composite certificate and append one certified morphism. Functoriality identifies the new certificate with the composition of the earlier certificate and the primitive certificate of the appended morphism. The declared composition rule completes the audit.