axis_P_selects_D
plain-language theorem explainer
Axis P is dimension-selecting: for recognized-object dimension p ≥ 1, the structural codimension formula yields substrate dimension 2p+1. Anyone tracking the multi-axis robustness of the D=3 route (or the revised three-dimensional-space paper) cites this as the arithmetic content of that axis. The proof is a one-line discharge: the formula-holds hypothesis is vacuous and the substrate-equality predicate is reflexivity.
Claim. For every natural number $p \ge 1$, if the structural codimension formula has been supplied for $p$, then the substrate dimension equals the codimension value $2p+1$.
background
The module records the robustness theorem from the revised paper Three-Dimensional Space from Recognition Cost. Three axes (coefficient ring, tracked invariant, acyclicity) are left as predicate-level interfaces for later algebraic-topology work. The remaining axis, Axis P, is purely arithmetic: the recognized-object dimension $p$ enters a fixed codimension formula.
That formula is defined by $\mathrm{CodimensionDimension}(p) := 2p+1$. The hypothesis that the formula has been supplied is the trivial proposition $\mathrm{True}$. A substrate-dimension statement is likewise the reflexive predicate $D=D$. Upstream constants across AlphaDerivation, GapDerivation, and FermionDOFGapBridge fix the spatial dimension $D:=3$ (T8/T9), which is the $p=1$ specialization of the same formula.
proof idea
Term-mode proof with two steps. Introduce the vacuous hypothesis that the codimension formula holds for $p$ (its type is $\mathrm{True}$). The goal reduces to $\mathrm{SubstrateDimensionEquals}(2p+1)$, which unfolds to the identity $2p+1=2p+1$ and is closed by $\mathrm{rfl}$. No external lemmas are required beyond the three in-module definitions.
why it matters
This is the structural content of Axis P in the multi-axis robustness package: only changes in the recognized-object dimension $p$ move the predicted substrate dimension, via $D=2p+1$. The module doc states explicitly that this axis is fully arithmetical, while Axes C, I, and A are robustness (non-moving) interfaces once $p=1$ is fixed.
The $p=1$ case recovers the framework landmark $D=3$ forced by T8 in the UnifiedForcingChain (and restated as T9 linking in AlphaDerivation). Sibling results such as $p_\mathrm{one}_\mathrm{gives}_D3$ and $\mathrm{axis}_P_\mathrm{moves}_D$ specialize or contrast this selection. No downstream consumers are wired yet; the declaration stands as the clean interface between the codimension arithmetic and the robustness narrative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.