knotInvariantCert
plain-language theorem explainer
This definition constructs a certificate asserting that exactly five knot invariants exist in the Recognition Science framework by assigning the precomputed cardinality to the five_invariants field. Low-dimensional topologists or RS foundation builders would cite it to confirm the count of knot-type discriminators. It is realized as a direct one-line construction that invokes the decided theorem establishing the cardinality equals five.
Claim. Define the certificate $c$ of type KnotInvariantCert by setting its five_invariants component to the proposition that the finite cardinality of the knot invariant type equals 5.
background
The module treats knot invariants from Recognition Science as five canonical families under configuration dimension 5: genus, crossing number, Alexander polynomial, Jones polynomial, and Khovanov homology. Each family functions as a rung on the complexity ladder for distinguishing knot types. The upstream theorem knotInvariant_count establishes by direct decision that the cardinality of the KnotInvariant type is exactly 5, which populates the structure KnotInvariantCert requiring Fintype.card KnotInvariant = 5.
proof idea
This is a one-line wrapper that directly supplies the value of knotInvariant_count to the five_invariants field of the KnotInvariantCert structure.
why it matters
This definition completes the certification of the five knot invariants within the RS mathematics module, aligning with the framework's assignment of configuration dimension D = 5 to low-dimensional topology structures. It supports the broader claim that RS derives structural depth in knot discrimination from the same forcing chain that yields physical constants. No downstream uses are recorded, leaving open whether it integrates into larger proofs of knot invariant relations under the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.