three_D_eq_D_sq
plain-language theorem explainer
At spatial dimension D=3 the elementary identity 3D=D² holds, so the squared lattice factor equals nine. Gap-derivation arguments cite it when rewriting D²(D+2) as 9·5=45 (the gap-45 exponent). The proof is a one-step native evaluation of the closed natural-number definition D:=3.
Claim. With spatial dimension fixed at $D=3$, one has $3D=D^{2}$. (As a Diophantine identity this holds only for $D\in\{0,3\}$.)
background
The module derives the coherence-energy gap exponent 45 from spatial dimension alone, closing boundary item B-22. A recognition event carries configuration dimension $D+2$: $D$ spatial axes (forced by T8), one temporal tick advance (T2), and one ledger-balance degree of freedom from $J(x)=J(x^{-1})$ (T3). Coherence energy is one factor of $\varphi^{-1}$ per degree of freedom, so $E_{\mathrm{coh}}=\varphi^{-(D+2)}$; at $D=3$ this recovers the constant $\varphi^{-5}$.
In-module, $D:\mathbb{N}:=3$ is the spatial dimension. The squared factor $D^{2}$ appears in the parity-count and gap formulae (configuration space of the $D$-cube and related ledger enumerations). The present identity simply records that this square equals the linear factor $3D$ once $D$ is specialized to three.
proof idea
Term-mode proof by native_decide. Because $D$ is definitionally the natural number 3, both sides reduce to concrete numerals ($3\cdot 3$ and $3^{2}$) and the kernel decides equality. No lemmas are invoked.
why it matters
Gap-45 is the product $D^{2}(D+2)$. At $D=3$ one needs $D^{2}=9$ to obtain $9\cdot 5=45$, matching the main theorem gap_at_D3 and the subsequent factorizations gap_factors / gap_is_lcm. The identity is the trivial arithmetic step that converts the geometric square into the integer 9 used throughout the B-22 resolution.
Framework landmarks: T8 forces $D=3$; the configuration count $D+2$ then forces $E_{\mathrm{coh}}=\varphi^{-5}$. Coprimality results in the same module further require $D$ odd, and Alexander duality selects $D=3$ among odd candidates, so gap-45 follows from dimension alone. No open sorry remains in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.