axis_P_moves_D
plain-language theorem explainer
When the recognized-object dimension p is a natural number with p ≥ 1 and p ≠ 1, the codimension value 2p+1 is never 3. Dimension-forcing and multi-axis robustness arguments cite this to isolate Axis P as the only axis that can shift spatial dimension off three. The proof unfolds the arithmetic definition and closes by linear integer arithmetic.
Claim. For every natural number $p$ satisfying $p \ge 1$ and $p \neq 1$, the codimension $2p+1$ is not equal to $3$.
background
The module records the multi-axis robustness theorem from the revised paper Three-Dimensional Space from Recognition Cost. Four axes of the dimension route are separated: coefficient ring (C), tracked invariant (I), acyclicity (A), and the recognized-object dimension parameter (P). C, I, and A are predicate-level interfaces for later algebraic-topology work; Axis P is purely arithmetical.
The codimension formula sends a recognized object of dimension $p$ to $D = 2p+1$. In the Recognition Science forcing chain, T8 forces three spatial dimensions, which is exactly the case $p = 1$. This lemma is the complementary fact: any other admissible $p$ moves $D$ off 3.
proof idea
Short term proof. Unfold the codimension definition $D(p) = 2p+1$, then discharge $2p+1 \neq 3$ from the hypotheses $p \ge 1$ and $p \neq 1$ by the omega tactic (Presburger / linear integer arithmetic). No external lemmas are invoked.
why it matters
Supplies the Axis-P conjunct of the bundled multi-axis robustness theorem, which states that only Axis P can move dimension away from 3 while Axes C, I, and A stay stable at the theorem-surface level. That bundle is the formal reading of the paper claim that the dimension route is robust under changes of coefficient ring, invariant tracking, and acyclicity, with the sole movable parameter being the recognized-object dimension $p$. In the forcing chain this protects T8 ($D = 3$): once $p$ is fixed at 1, the other axes cannot reopen the dimension question. Companion results handle the positive selection $p = 1 \Rightarrow D = 3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.