diffGeoCert
plain-language theorem explainer
diffGeoCert assembles the DiffGeoCert structure by populating its two fields from upstream decidable theorems. It certifies five differential geometric structures on the recognition manifold and a spacetime dimension of four. A researcher tracing the derivation of geometry from the Recognition Science functional equation would cite this certificate to confirm the dimension count. The construction applies the two prior results directly without further proof steps.
Claim. Let DiffGeoCert be the structure asserting that the cardinality of the set of differential geometric structures on the recognition manifold equals 5 and that the spacetime dimension equals 4. The definition provides the instance in which the first assertion is witnessed by the theorem establishing that cardinality equals 5 and the second by the theorem establishing the dimension equals 4.
background
The module DifferentialGeometryFromRS derives differential geometry from the Recognition Science framework. The recognition manifold is a smooth 3-manifold with D=3. Five canonical structures (smooth manifold, Riemannian, pseudo-Riemannian, Kähler, symplectic) correspond to configDim D=5. The RS metric is pseudo-Riemannian, yielding 4-dimensional spacetime as D+1.
proof idea
The definition constructs the DiffGeoCert record by assigning the five_structures field the value from diffGeoStructureCount and the spacetime_4 field the value from rsSpacetimeDim_eq_4. Each upstream theorem is proved by a one-line decide tactic, so the definition simply assembles the certificate.
why it matters
This definition supplies the DiffGeoCert instance that certifies the geometric structures and dimension in the Recognition Science derivation. It supports the claim that the 3-manifold yields five structures and 4D spacetime, consistent with T8 forcing D=3 spatial dimensions. It closes the local certification step without addressing further physical constants or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.