knotInvariant_count
plain-language theorem explainer
Recognition Science enumerates exactly five canonical knot invariant families in its low-dimensional topology setting. Researchers classifying knots via complexity ladders would cite this cardinality when referencing configDim D equals 5. The proof is a direct decision on the finite inductive type that lists the five constructors.
Claim. $|KnotInvariant| = 5$, where the inductive type KnotInvariant consists of the five constructors genus, crossing number, Alexander polynomial, Jones polynomial, and Khovanov homology.
background
The module Knot Invariants from RS sets the local theoretical context for five canonical knot invariant families as rungs on the complexity ladder of knot-type discrimination, with Lean status of zero sorry and zero axiom. The upstream inductive definition KnotInvariant enumerates these cases explicitly. This supplies the finite type whose cardinality is asserted in the present declaration.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute Fintype.card directly on the inductive type KnotInvariant, which has five constructors.
why it matters
This theorem supplies the five_invariants field in the downstream knotInvariantCert definition. It realizes the module assertion of five families for configDim D equals 5 in Recognition Science low-dimensional topology structural depth. The declaration closes the enumeration step without touching the forcing chain or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.