p_one_gives_D3
plain-language theorem explainer
When the recognized-object dimension is one, the codimension formula forces spatial dimension three. Anyone citing multi-axis robustness of the D=3 route needs this arithmetic base case. The proof is pure definitional reduction: 2·1+1 equals 3 by reflexivity.
Claim. For recognized-object dimension $p=1$, the codimension formula gives spatial dimension $D=2p+1=3$.
background
The module records the robustness theorem from the revised paper Three-Dimensional Space from Recognition Cost. Coefficient-ring, tracked-invariant, and acyclicity axes are predicate-level interfaces for later algebraic topology. The axis that actually moves dimension is purely arithmetical.
The codimension formula assigns to a recognized object of dimension $p$ the ambient dimension $D=2p+1$. That definition is the only content needed here: substituting $p=1$ yields $D=3$. In the broader Recognition forcing chain this is the T8 landmark (three spatial dimensions), reached once the recognized-object dimension is fixed at one.
Sibling statements in the same file record that other axes (C, I, A) leave $D$ unchanged, while varying $p$ moves $D$. This lemma is the concrete $p=1$ evaluation of that formula.
proof idea
One-line reflexivity proof. Unfold CodimensionDimension 1, which is defined as $2\cdot 1+1$, and reduce to the numeral equality $3=3$ by rfl. No lemmas are applied.
why it matters
Pins the arithmetic base case of the dimension-moving axis in the multi-axis robustness story: only $p=1$ yields $D=3$. That is the T8 step of the Recognition forcing chain (three spatial dimensions). The module header states that changing the recognized-object dimension $p$ changes the codimension formula to $D=2p+1$; this theorem discharges the distinguished value used throughout the paper.
No downstream consumers are wired yet in the graph. The immediate siblings are the robustness certificates for the non-moving axes and the general statement that the P-axis selects $D$. Together they separate the unique arithmetical lever from the structural axes that stay inert under the same hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.