configDim_at_D3
plain-language theorem explainer
At spatial dimension three, a recognition event has configuration dimension five (three spatial plus one temporal plus one balance degree of freedom). Anyone pinning the coherence-energy or ħ exponent to φ^{-5} from D alone cites this evaluation. The proof is a one-line native decision of the arithmetic 3+2=5.
Claim. Let the spatial dimension be $D=3$. The configuration dimension of a recognition event, defined by $d \mapsto d+2$, satisfies $D+2=5$.
background
The module derives the gap-45 identity from spatial dimension alone, closing boundary item B-22. A recognition event is assigned $D+2$ independent degrees of freedom: $D$ spatial (forced by T8), one temporal tick advance (T2), and one ledger-balance mode from $J(x)=J(x^{-1})$ (T3). Coherence energy is then one factor of $\varphi^{-1}$ per degree of freedom, so $E_{\mathrm{coh}}=\varphi^{-(D+2)}$.
Here the spatial dimension is the constant $D:=3$, and the configuration dimension is the linear map $\mathrm{configDim}(d):=d+2$. The same integer five appears elsewhere in the stack as a fixed configuration count (for example in the CMB rung product), but in this module it is derived rather than postulated.
Upstream, T8 forces three spatial dimensions; the present fact simply evaluates the configuration formula at that forced value.
proof idea
Unfold the two definitions: spatial dimension is the natural number 3, and configuration dimension is addition of two. The goal reduces to $3+2=5$, which native_decide discharges by kernel computation. No lemmas are required beyond definitional reduction.
why it matters
This evaluation is the arithmetic hinge that turns the structural claim "exponent equals $D+2$" into the concrete RS-native powers $\varphi^{-5}$. Downstream, Constants_E_coh_eq_configDim rewrites $E_{\mathrm{coh}}=\varphi^{-(\mathrm{configDim},D)}$ by substituting the value five; hbar_exponent_eq_configDim does the same for $\hbar$, stating that the exponent five is forced $D+2$, not a free parameter. The certificate bundle gap45_cert records this fact as its config_dim field, feeding the gap identity $D^2(D+2)=45$ at $D=3$.
In the forcing chain this sits after T8 ($D=3$) and before the coherence and action quanta. Combined with the parity-count side ($D^2=9$ at $D=3$) it yields gap-45 from dimension alone, with no extra fitting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.