diffGeoStructureCount
plain-language theorem explainer
The theorem establishes that the recognition manifold admits exactly five canonical differential geometric structures. Researchers deriving differential geometry from Recognition Science axioms would cite this count when verifying manifold structure. The proof is a one-line wrapper that invokes the decide tactic on the finite inductive type enumerating the structures.
Claim. The finite set of canonical differential geometric structures on the recognition manifold, consisting of the smooth manifold, Riemannian, pseudo-Riemannian, Kähler, and symplectic cases, has cardinality five.
background
The module develops differential geometry from Recognition Science on the recognition manifold, defined as a smooth 3-manifold with D=3. Five canonical structures are enumerated by an inductive type: smooth manifold, Riemannian metric, pseudo-Riemannian metric, Kähler structure, and symplectic structure. This count equals configDim D = 5, and the RS metric is pseudo-Riemannian, yielding 4-dimensional spacetime as D+1. The upstream inductive definition supplies the finite type whose cardinality is computed here.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype instance derived from the inductive type with five constructors, directly yielding the cardinality five.
why it matters
This theorem supplies the five_structures field to the diffGeoCert definition, which also incorporates the spacetime dimension equality. It anchors the differential geometry layer in the Recognition Science framework, confirming D=3 spatial dimensions and D+1=4 spacetime. It aligns with the forcing chain result T8 that fixes three dimensions and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.