KnotInvariantCert
plain-language theorem explainer
KnotInvariantCert packages the assertion that precisely five knot invariant families exist within the Recognition Science model of low-dimensional topology. Topologists and mathematical physicists studying knot complexity would cite this when connecting RS forcing chains to classical invariants such as the Jones polynomial. The declaration is a bare structure definition whose single field records the Fintype cardinality of the inductive enumeration KnotInvariant.
Claim. Let $K$ be the finite set of knot invariants consisting of genus, crossing number, Alexander polynomial, Jones polynomial, and Khovanov homology. The structure asserts that $|K| = 5$.
background
The module establishes five canonical knot invariant families that correspond to configDim D = 5 in the Recognition Science framework. These families are genus, crossing number, Alexander polynomial, Jones polynomial, and Khovanov homology, each serving as a rung on the complexity ladder for distinguishing knot types. The upstream inductive definition KnotInvariant enumerates exactly these five cases and derives DecidableEq, Repr, BEq, and Fintype instances. This local setting provides structural depth for low-dimensional topology without introducing axioms or sorry placeholders.
proof idea
The declaration is a structure definition with a single field that directly states the cardinality condition Fintype.card KnotInvariant = 5. No tactics or lemmas are applied; the proof body is empty because the claim is definitional.
why it matters
This definition supplies the certificate type consumed by the downstream construction knotInvariantCert, which populates the field using knotInvariant_count. It fills the structural slot for the five invariants in the RS low-dim topology development, aligning with the configDim D = 5 landmark. No open questions are addressed here; the declaration closes the enumeration of the inductive type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.