AxisARobust
plain-language theorem explainer
Axis A robustness asserts that substrate-acyclicity perturbations preserve the D = 3 conclusion inside the named 1-acyclic class. It is the predicate-level interface for the acyclicity axis in the multi-axis robustness theorem of the dimension-forcing paper. Presently defined as the unit proposition True, so the theorem surface discharges by triviality pending fuller algebraic-topology content.
Claim. Substrate-acyclicity perturbations inside the named $1$-acyclic class preserve the conclusion that spatial dimension equals $3$.
background
The module records multi-axis robustness for the dimension route from the revised Three-Dimensional Space from Recognition Cost paper. Content is intentionally structural: coefficient-ring, tracked-invariant, and acyclicity-axis equivalences are predicate-level interfaces for future algebraic-topology work. Only the recognized-object dimension axis is fully arithmetical: changing $p$ changes the codimension formula to $D = 2p + 1$.
Axis A is the acyclicity axis. Its robustness claim is that, inside a fixed named $1$-acyclic class, perturbations of substrate-acyclicity data do not move the forced spatial dimension away from three. Companion axes cover coefficient-ring and tracked-invariant stability; Axis P is the one that can change $D$.
This sits beside the foundation forcing chain that already selects $D = 3$ (T8) once the eight-tick octave and related structure are fixed.
proof idea
Definitional abbreviation: the proposition is set equal to True. No lemmas are applied. Downstream theorems such as axis_A_robust discharge the surface by trivial.
why it matters
Feeds the Axis A robustness theorem surface and the bundled multi-axis robustness theorem. The bundle states that only Axis P can move dimension away from $3$; Axes C, I, and A remain stable at the theorem-surface level. That packages the paper claim that the dimension route is robust under acyclicity, coefficient, and invariant perturbations, while the arithmetical $p$-axis alone changes $D = 2p + 1$.
In the Recognition framework this protects the T8 conclusion $D = 3$ against the named acyclicity deformations, so the spatial-dimension step of the forcing chain is not an artifact of a brittle acyclicity hypothesis. The definition is a placeholder interface until the algebraic-topology formalization of the $1$-acyclic class is filled in.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.