multi_axis_robustness
plain-language theorem explainer
Bundles multi-axis stability for the dimension-forcing route: coefficient-ring, tracked-invariant, and acyclicity axes leave spatial dimension fixed at 3 once the recognized-object dimension is p=1, while only the p-axis can move the codimension formula off 3. Cite this as the structural summary of the revised Three-Dimensional Space from Recognition Cost paper. Proof is a one-line conjunction of the four axis lemmas.
Claim. Coefficient-ring, tracked-invariant, and substrate-acyclicity axes are stable (they preserve $D=3$ once $p=1$ is fixed), and for every natural number $p\geq 1$ with $p\neq 1$, the codimension formula $2p+1$ is not equal to $3$.
background
The module records the multi-axis stability theorem from the revised Three-Dimensional Space from Recognition Cost paper. The setting is structural: three axes (coefficient ring, tracked invariant, substrate acyclicity) are predicate-level interfaces reserved for later algebraic-topology work; the fourth axis is purely arithmetical.
The codimension formula assigns to a recognized object of dimension $p$ the substrate dimension $D=2p+1$. When $p=1$ this recovers $D=3$, matching the forced spatial dimension (T8). Axis C asserts that coefficient-ring perturbations preserve $D=3$ once $p=1$; Axis I does the same for tracked-invariant perturbations; Axis A does so inside the named 1-acyclic class. At present each of those three predicates is definitionally True.
Axis P is dimension-selecting: varying $p$ changes $D=2p+1$, so only that axis can move the conclusion away from 3.
proof idea
Term-mode one-liner. The goal is a four-fold conjunction; exact supplies the pair of the four upstream lemmas axis_C_robust, axis_I_robust, axis_A_robust, and axis_P_moves_D. Each of the first three is itself a trivial discharge of a definitionally-true predicate. The fourth is the arithmetic statement that $p\neq 1$ forces $2p+1\neq 3$.
why it matters
This is the top-level packaging of the multi-axis stability claim for the dimension route. It isolates the single movable axis (recognized-object dimension $p$) from the three currently placeholder axes, so that the forced $D=3$ conclusion (T8 in the forcing chain) is visibly insensitive to the unfinished algebraic-topology interfaces.
No downstream consumers are wired yet (used_by is empty). The immediate companion in-module is the compatibility remark that once $p=1$, the codimension route agrees with the existing dimension-forcing result from DimensionForcing. The open work is to replace the three True predicates by genuine equivalences once the coefficient-ring, tracked-invariant, and acyclicity formalizations land.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.