SubstrateDimensionEquals
plain-language theorem explainer
Names the proposition that the substrate spatial dimension equals a given natural number D. Downstream dimension-route theorems cite it as the conclusion once the codimension formula is fixed. The body is the tautology D = D, so the claim holds definitionally for every D and is discharged by reflexivity.
Claim. For any natural number $D$, the substrate-dimension statement at $D$ is the proposition $D = D$.
background
The module records the multi-axis stability theorem from the revised paper on three-dimensional space from recognition cost. Content is intentionally structural: coefficient-ring, tracked-invariant, and acyclicity axes are predicate-level interfaces. The axis that actually moves dimension is arithmetical: if the recognized-object dimension is $p$, the codimension formula reads $D = 2p + 1$.
Across the foundation stack the forced spatial dimension is the constant $D := 3$ (T8 in the forcing chain; T9 linking also requires $D = 3$). Sibling predicates package the codimension formula and the map $p \mapsto 2p+1$. The present definition is the bare conclusion slot those predicates fill: a named Prop asserting that the substrate dimension equals a supplied natural number.
proof idea
Pure definition. The body is propositional equality of $D$ with itself on $\mathbb{N}$, so the predicate is true for every input by rfl. No lemmas are applied. Downstream one-line wrappers (e.g. the axis-P selection theorem) introduce a codimension hypothesis and close by reflexivity after unfolding.
why it matters
Supplies the conclusion type for the dimension-selecting axis. The parent theorem axis_P_selects_D states that whenever the codimension formula holds at recognized-object dimension $p$ (with $p \ge 1$), the substrate-dimension statement holds at $2p+1$. The $p = 1$ case recovers the landmark $D = 3$ forced by T8 in the unified forcing chain.
In the paper architecture this is the arithmetical axis that can change $D$; the other axes are required only to preserve the $D = 3$ conclusion once $p = 1$ is fixed. The definition is a thin named interface so those stability statements can target a uniform Prop rather than raw equality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.