DiffGeoStructure
plain-language theorem explainer
DiffGeoStructure enumerates the five canonical differential geometric structures on the recognition manifold: smooth manifold, Riemannian, pseudo-Riemannian, Kähler, and symplectic. Researchers deriving spacetime from Recognition Science cite this list when confirming the RS metric is pseudo-Riemannian with dimension 4. The declaration is a direct inductive type whose Fintype instance is supplied automatically by the deriving clauses.
Claim. Let $S$ be the finite set of differential geometric structures on the recognition manifold, consisting of the smooth manifold structure, the Riemannian metric, the pseudo-Riemannian metric, the Kähler structure, and the symplectic structure.
background
The module starts from the recognition manifold as a smooth 3-manifold with $D=3$. It lists five canonical structures whose cardinality equals the configuration dimension for this $D$. The RS metric is identified as pseudo-Riemannian, so spacetime dimension equals $D+1=4$ and carries Lorentzian signature.
proof idea
The declaration is an inductive type definition that introduces five constructors and derives DecidableEq, Repr, BEq, and Fintype instances in a single line.
why it matters
DiffGeoStructure supplies the enumeration required by DiffGeoCert to certify both five structures and spacetime dimension 4. It connects the Recognition Science forcing chain (T8 sets $D=3$) to the emergence of 3+1 Lorentzian spacetime. The downstream theorem diffGeoStructureCount simply evaluates the cardinality of this inductive type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.