TopologicalInvariant
plain-language theorem explainer
Recognition Science equates exactly five topological invariants with its configuration dimension D=5. Researchers in discrete geometry or RS foundations cite this enumeration when counting invariants or certifying Euler characteristics of complexes such as Q3. The declaration is a direct inductive definition that derives Fintype to support immediate cardinality proofs by decision.
Claim. Let $T$ be the inductive type whose constructors are the Euler characteristic, the fundamental group, homology groups, cohomology groups, and the homotopy type.
background
The module TopologyFromRS defines five canonical topological invariants that Recognition Science identifies with configuration dimension D=5. In this setting the complex Q3 satisfies Euler characteristic chi(Q3) = 8-12+6=2, matching the value for the sphere S2. The inductive definition enumerates these invariants and equips them with Fintype for automatic cardinality computation.
proof idea
The declaration is the inductive type definition itself, introducing five constructors and deriving the instances DecidableEq, Repr, BEq, and Fintype in a single declaration line.
why it matters
This definition supplies the type whose cardinality equals 5 in the downstream theorem topologicalInvariantCount and populates the TopologyCert structure. It implements the module claim that five invariants correspond to configDim D=5 and supports the explicit computation chi(Q3)=2. Within the Recognition Science framework it contributes to topological consistency with the eight-tick octave and spatial dimension D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.