E_coh_gap_eq
plain-language theorem explainer
The coherence-energy scale forced by the configuration dimension of a recognition event equals φ to the minus fifth. Anyone deriving the RS-native action quantum ħ = φ^{-5}, or closing boundary item B-22, cites this identity. The proof unfolds E_coh_gap := φ^{-configDim(D)} and reduces by the forced values D = 3 and configDim(D) = D + 2.
Claim. The gap coherence energy equals $\varphi^{-5}$, where that energy is defined as $\varphi$ raised to minus the configuration dimension of a recognition event at spatial dimension $D=3$ (so the exponent is $-(D+2)=-5$).
background
Recognition Science assigns a coherence energy by counting independent degrees of freedom of one recognition event. Module GapDerivation closes boundary item B-22: that count is the configuration dimension $\mathrm{configDim}(D)=D+2$, namely $D$ spatial directions (T8), one temporal tick advance (T2), and one ledger-balance degree from $J(x)=J(x^{-1})$ (T3).
Locally the gap energy is defined as $\varphi$ to the minus that count. Spatial dimension is the constant $D:=3$. With one factor $\varphi^{-1}$ per configuration degree of freedom this yields $\varphi^{-5}$ at $D=3$, matching the runtime constant used to build $\hbar=E_{\mathrm{coh}}\cdot\tau_0$.
Upstream, $D$ is fixed in AlphaDerivation as the spatial dimension forced by linking. The native action quantum is defined by $\hbar=E_{\mathrm{coh}}\cdot\tau_0$; the present identity is the part of that story that is a forced count rather than a free unit choice.
proof idea
Short term-mode proof by unfolding. Substitute the definition of the gap energy ($\varphi$ to the minus configuration dimension of $D$), then unfold $\mathrm{configDim}$ and the constant $D$. With $D=3$ and $\mathrm{configDim}(D)=D+2$ the exponent is $-5$; norm_num discharges the resulting real equality.
why it matters
This is the machine-checked half of the $\hbar=\varphi^{-5}$ story that is not pure unit convention. The module states the forced content is the count $\mathrm{configDim}(D)=D+2=5$ ($D=3$ from T8, $+1$ tick from T2, $+1$ balance from T3); the modeling input is $\varphi^{-1}$ per degree of freedom.
Downstream it feeds gap45_cert, the certificate packaging configuration dimension, parity counts, and the gap-45 identity $D^2(D+2)=45$ at $D=3$. It is also used from the $\tau_0$ positivity infrastructure in Constants, adjacent to the C-004 Planck-constant derivation block.
Together with gap_at_D3 and the coprimality lemmas in the same module, it completes B-22 and locks the exponent that makes native $E_{\mathrm{coh}}$ and $\hbar$ consistent with the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.