topologicalInvariantCount
plain-language theorem explainer
Exactly five topological invariants are defined in the Recognition Science framework, matching the configuration dimension D=5. Researchers studying the topology of the recognition manifold cite this count when confirming the Euler characteristic of Q3 equals that of S2. The proof reduces to a single decide tactic that computes the Fintype cardinality of the inductive enumeration of the five invariants.
Claim. The set of topological invariants has cardinality 5: $|$Euler characteristic, fundamental group, homology, cohomology, homotopy type$| = 5$.
background
The Topology from RS module identifies five canonical topological invariants (Euler characteristic, fundamental group, homology groups, cohomology, homotopy type) and sets their count equal to the configuration dimension D=5. These are formalized as the inductive type with five constructors that derives DecidableEq, Repr, BEq, and Fintype. The module states that Q3 has Euler characteristic V - E + F = 8 - 12 + 6 = 2, matching the 2-sphere.
proof idea
The proof is a term-mode application of the decide tactic to Fintype.card on the inductive type. The tactic succeeds directly because the type has exactly five constructors and the derived Fintype instance is computable.
why it matters
This theorem supplies the five_invariants component of the topologyCert definition, which also records the Euler characteristic equality for Q3. It fills the topological foundation for the Recognition Science claim that the number of invariants equals configDim D=5, connecting to the forcing chain step T8 that fixes spatial dimension D=3 and the eight-tick octave. No open questions remain in the supplied scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.