AxisIRobust
plain-language theorem explainer
Axis I is the proposition that tracked-invariant perturbations leave the forced spatial dimension at three once the recognized-object dimension is fixed at one. It is presently the constant-true predicate, so the surface theorem is immediate. Anyone citing multi-axis robustness of the dimension route uses this slot to mark that the invariant axis does not move D.
Claim. The Axis-I robustness predicate asserts that perturbations along the tracked-invariant axis preserve the conclusion $D = 3$ once the recognized-object dimension is fixed at $p = 1$. In the present formalization the predicate is definitionally $\mathrm{True}$.
background
The module records the multi-axis robustness theorem from the revised paper on three-dimensional space from recognition cost. Content is intentionally structural: coefficient-ring, tracked-invariant, and acyclicity axes are predicate-level interfaces for later algebraic-topology work. Only the arithmetical axis moves dimension: changing the recognized-object dimension $p$ changes the codimension formula to $D = 2p + 1$.
Upstream, spatial dimension is fixed at three in several places (T8/T9 forcing): $D := 3$ in the gap derivation, alpha derivation, and fermion DOF bridge. Active-edge count $A$ is likewise pinned at one. Axis I is the tracked-invariant slot in that bundle: once $p = 1$ is chosen, invariant-preserving deformations are not allowed to reopen the dimension question.
proof idea
Definitional, not a derived proof. The declaration is Prop := True, so any inhabitant is obtained by trivial (as in the surface theorem axis_I_robust). No lemmas are applied; the mathematical content is deferred to a future topology formalization that would replace True by a nontrivial invariance statement.
why it matters
Feeds the surface theorem axis_I_robust and the bundled multi_axis_robustness, whose doc-comment states: only Axis P can move the dimension away from 3; Axes C, I, and A are stable at the theorem-surface level. That bundle is the Lean face of the paper's robustness claim for the dimension route.
In the Recognition forcing chain, T8 forces $D = 3$ spatial dimensions and T7 the eight-tick octave. Axis I records that tracked-invariant perturbations do not undo that conclusion once $p = 1$ is fixed. The open work is replacing this constant-true interface with a genuine invariance theorem in the planned algebraic-topology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.