SubstrateSymmetryProperties
plain-language theorem explainer
Bundles the five substrate symmetry axioms (homogeneous, orientable, compact, φ-self-similar, isotropic) that jointly pin spatial topology. Downstream topology-forcing arguments cite this record as the hypothesis package. As a structure definition there is no proof: it only names the Prop fields.
Claim. A record of five propositions on the recognition substrate: homogeneity (no preferred cell), orientability, compactness (finite total volume), $\varphi$-self-similarity (scale invariance of the comparison law at golden-ratio spacing), and isotropy (no preferred direction).
background
The module derives spatial topology from substrate constraints: the recognition substrate is treated as a compact orientable 3-manifold, and three linked properties force $T^3$ topology. Homogeneity comes from the comparison cost $J(x)=\cosh(\log x)-1$, which depends only on the ratio $x$, so every cell is equivalent and there is no boundary or distinguished point. Flatness is argued from $\varphi$-self-similarity: a scaling $x\mapsto x^\varphi$ needs a metric with no preferred curvature radius; spherical and hyperbolic geometries break that invariance, leaving only flat geometry.
Among compact orientable flat 3-manifolds, the Bieberbach list has six types. First Betti number $b_1$ separates them: only the 3-torus has $b_1=3$; the turn-flat quotients have $b_1=1$, and Hantzsche–Wendt has $b_1=0$. This structure packages the five Prop fields those arguments consume, including isotropy used later to force $b_1=3$.
proof idea
No proof body: this is a structure declaration. Each field is an uninterpreted Prop with a doc-comment fixing its intended meaning (homogeneous, orientable, compact, phi-self-similar, isotropic). Instantiation is deferred to recognitionSubstrateProperties, which sets every field to True.
why it matters
This is the hypothesis package for the spatial-topology forcing chain in the same module (flatness from $\varphi$-self-similarity, Bieberbach-type classification, isotropy forcing $b_1=3$, and the uniqueness claim that the spatial topology is $T^3$). It feeds recognitionSubstrateProperties, which asserts that the recognition substrate realizes all five properties. In the broader RS forcing chain this sits next to T8 ($D=3$ spatial dimensions) and the eight-tick octave: once dimension and substrate symmetries are fixed, topology is no longer free data. The structure itself does not close any open gap; it only names the constraints the structural theorem uses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.