E_coh_gap
plain-language theorem explainer
Coherence energy is defined as φ to the minus configuration dimension of a recognition event. With spatial dimension fixed at 3, that exponent is −5, recovering the RS-native E_coh scale. Cited by anyone closing B-22 or linking the φ-ladder yardstick to gap-45. Pure one-line definitional composition of φ-power with configDim D.
Claim. Define the coherence-energy scale by $E_{\mathrm{coh}}:=\varphi^{-(D+2)}$, where $D=3$ is the forced spatial dimension and $D+2$ is the configuration dimension of a recognition event (D spatial + one temporal tick + one ledger-balance degree of freedom).
background
Module GapDerivation closes boundary item B-22: the coherence-energy exponent equals the configuration dimension of a recognition event, so $E_{\mathrm{coh}}=\varphi^{-5}$ once spatial dimension is three.
Spatial dimension $D$ is the constant 3 forced by T8 in the unified forcing chain. Configuration dimension is the sibling configDim d := d + 2: D lattice directions, one temporal tick advance (T2), and one balance degree of freedom from ledger neutrality $J(x)=J(x^{-1})$ (T3). Coherence energy is charged at $\varphi^{-1}$ per independent degree of freedom, hence the pure power $\varphi^{-(D+2)}$.
The same $D=3$ appears in sibling Alpha and FermionDOF modules; cosmology reuses the numeric value 5 as a fixed configDim for multipole scaffolding. Downstream, gap-45 is $D^2(D+2)=9\times 5=45$.
proof idea
Definitional, not a proof. The body is the single term $\varphi$ raised to the integer power $-({\mathrm{configDim}}, D)$. Unfolding configDim and D immediately yields $\varphi^{-5}$; that numerical identity is discharged next door by E_coh_gap_eq via unfold and norm_num.
why it matters
Pins the B-22 claim that $E_{\mathrm{coh}}=\varphi^{-(D+2)}$ and, at the T8 value $D=3$, matches Constants.E_coh ($\hbar=\varphi^{-5}$ in RS-native units). Feeds E_coh_gap_eq, which upgrades the prose match to a proved equality, and sits inside Gap45Cert (config_dim field: configDim D = 5) alongside parity count 9, gap 45, and coprimality of $2^D$ with the gap.
Together with gap_at_D3 and the odd-D coprimality lemmas, this makes gap-45 a consequence of $D=3$ alone (Alexander duality selecting three-space). It is the energy-side half of the matter-coherence link gap_balance: $\varphi^{1-{\mathrm{gap}}}\cdot\varphi^{\mathrm{gap}}=\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.