recognitionSubstrateProperties
plain-language theorem explainer
Packages the recognition substrate as satisfying all five symmetry axioms: homogeneous, orientable, compact, φ-self-similar, and isotropic. Downstream topology-forcing arguments take this record as the input witness that the substrate is a compact orientable 3-manifold with scale-free comparison. Pure structure instance: each field is definitionally True.
Claim. The recognition substrate is homogeneous (no preferred cell), orientable, compact (finite total volume), $\varphi$-self-similar (comparison law scale-invariant at golden-ratio spacing), and isotropic.
background
The module derives spatial topology from substrate constraints. Status is structural: zero sorry, no RS-internal axioms. The comparison cost $J(x)=\cosh(\log x)-1$ depends only on ratios, so every cell is equivalent; that is homogeneity. Compactness and orientability are standing geometric hypotheses on the spatial slice. $\varphi$-self-similarity means the metric admits the golden-ratio rescaling without a preferred curvature radius. Isotropy means no preferred spatial direction.
SubstrateSymmetryProperties is the five-field record that packages these Props. The module's forcing chain then uses them to exclude curved geometries and non-torus Bieberbach quotients, leaving $T^3$.
proof idea
Definitional construction, not a proof. Instantiates SubstrateSymmetryProperties by setting homogeneous, orientable, compact, phiSelfSimilar, and isotropic each to True. No lemmas are applied.
why it matters
This is the canonical witness that the recognition substrate carries the full symmetry package assumed by the spatial topology forcing argument (module siblings: flatness from $\varphi$-self-similarity, Bieberbach-type classification, $b_1=3$ uniqueness for $T^3$, and spatial_topology_forcing / spatial_dimension_eq_3). It sits under the T8 landmark ($D=3$ spatial dimensions) and the module claim that three joint properties force $T^3$ topology. No downstream edges are recorded yet; the record exists so later theorems can quantify over a single named substrate rather than five separate hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.