CodimensionDimension

The module Multi-Axis Robustness records the structural robustness theorem from the revised Three-Dimensional Space from Recognition Cost paper. Most axes (coefficient ring, tracked invariant, acyclicity) are predicate-level interfaces awaiting fuller algebraic-topology formalization. Axis P is the exception: it is purely arithmetical.

Here $p$ is the dimension of the recognized object. The codimension formula maps that object dimension to a substrate dimension via $D = 2p + 1$. In the Recognition forcing chain this is the arithmetic handle that selects spatial dimension (T8), with the special case $p = 1$ recovering $D = 3$.

The definition sits next to predicates such as CodimensionFormulaHolds and SubstrateDimensionEquals, which package the claim that the formula has been supplied and that the substrate dimension equals the value it returns.

Pure definitional abbreviation: the body is the arithmetic expression $2p + 1$. No lemmas, tactics, or upstream theorems are applied. Downstream results unfold this name and discharge goals by rfl or omega.

This is the arithmetic content of Axis P in the multi-axis robustness theorem. Downstream, axis_P_selects_D states that whenever the codimension formula holds for $p$, the substrate dimension equals $2p+1$; p_one_gives_D3 specializes to $D(1) = 3$; and axis_P_moves_D shows that any $p \ge 1$ with $p \ne 1$ yields $D \ne 3$. The bundled multi_axis_robustness theorem then asserts that only Axis P can move the dimension away from 3, while Axes C, I, and A stay fixed at the theorem-surface level.

Compatibility with the existing dimension-forcing result is recorded by p_one_route_agrees_with_dimension_forced: once $p = 1$, the codimension route agrees with the forced RS-compatible dimension. In the framework landmarks this is the concrete arithmetic realization of T8 ($D = 3$ spatial dimensions) under the recognition-cost route.