CodimensionFormulaHolds
plain-language theorem explainer
Marks that the structural codimension formula has been supplied for a recognized-object dimension p. Downstream dimension-selection theorems treat it as a discharged hypothesis and conclude the substrate dimension is 2p+1. The body is the constant true proposition, so the interface is definitional rather than proved.
Claim. For every natural number $p$, the predicate ``the structural codimension formula has been supplied at $p$'' holds (it is definitionally true).
background
The Multi-Axis Robustness module records the robustness theorem from the revised paper on three-dimensional space from recognition cost. Most axes (coefficient ring, tracked invariant, acyclicity) are predicate-level interfaces awaiting algebraic-topology formalization. The dimension-moving axis is purely arithmetical: the recognized-object dimension $p$ enters a codimension formula that forces the substrate dimension $D = 2p + 1$.
This declaration is the structural flag that the codimension formula has been supplied at a given $p$. Sibling material in the same module defines the associated dimension expression and the equality predicate used when the substrate dimension is identified with that expression. In the Recognition forcing chain, spatial dimension $D = 3$ is the T8 landmark; here it arises as the $p = 1$ case of the same formula.
proof idea
Definitional, not a proof. The predicate is defined as the constant proposition $\mathrm{True}$ on every natural $p$, so inhabitation is immediate (True.intro) and no lemmas are applied. Downstream theorems simply introduce the hypothesis and discard it.
why it matters
Feeds axis_P_selects_D, which states that axis P is dimension-selecting: whenever the codimension formula is supplied at $p$ (with $p \ge 1$), the substrate dimension equals the codimension expression $2p+1$. The $p=1$ specialization is the route to $D=3$ in this module, aligning with the T8 forcing step that spatial dimension is three. The declaration is intentionally thin: it separates the structural claim ``formula supplied'' from the arithmetic identification of $D$, keeping the multi-axis robustness statement modular while the coefficient-ring and acyclicity axes remain future topology interfaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.