gap45_cert
plain-language theorem explainer
Packages every proved identity of the gap-45 derivation at spatial dimension three into one certificate structure: configuration dimension five, nine parities, gap forty-five, coprimality with the eight-tick power of two, coherence energy φ^{-5}, and the matter-coherence balance. Anyone citing the B-22 closure or the D=3 origin of E_coh points here. The body is a pure field assembly of already-proved lemmas; no new reasoning.
Claim. There is a certificate recording that, at spatial dimension $D=3$: the configuration dimension equals $5$, the parity count equals $9$ and matches the enumerated nine-parity index set, the dimension gap $D^2(D+2)$ equals $45$, $\gcd(2^D,45)=1$, the coherence energy is $\varphi^{-5}$, the balance identity $\varphi^{A-\mathrm{gap}}\cdot\varphi^{\mathrm{gap}}=\varphi$ holds, every odd dimension is coprime to its gap, and every even dimension $D\ge 2$ fails that coprimality.
background
Module Foundation.GapDerivation closes boundary item B-22: a recognition event carries $D+2$ independent degrees of freedom ($D$ spatial from the lattice/T8, one temporal tick, one ledger-balance degree from $J(x)=J(x^{-1})$). Coherence energy is charged at $\varphi^{-1}$ per degree, so $E_{\mathrm{coh}}=\varphi^{-(D+2)}$. At $D=3$ this is $\varphi^{-5}$, matching the runtime constant.
The dimension gap is defined as $\mathrm{parityCount}(d)\times\mathrm{configDim}(d)$. At $D=3$ one has $\mathrm{configDim}=D+2=5$ and $\mathrm{parityCount}=D^2=9$, hence gap $45$. Coprimality of $2^D$ with the gap holds precisely when $D$ is odd, supplying an independent parity argument that $D$ cannot be even.
Gap45Cert is the structure that freezes all of these equalities (plus the global odd/even coprimality families and the $\varphi$-balance $\eta_B\cdot\Theta_{\mathrm{crit}}=\varphi$) into a single record.
proof idea
One-line structure construction. Each field of Gap45Cert is filled by a named upstream theorem already proved in the same module: configDim_at_D3, parityCount_at_D3, parityCount_matches_enumeration, gap_at_D3, coprime_at_D3, E_coh_gap_eq, gap_balance, coprimality_odd, and coprimality_even_fails. No tactics beyond the structure instance; the certificate inherits the native_decide and algebraic proofs of those lemmas.
why it matters
This is the single exportable witness that gap-45 and $E_{\mathrm{coh}}=\varphi^{-5}$ follow from $D=3$ alone (T8), closing B-22 with zero sorry and zero axioms. The coprimality fields give a fourth independent reason $D$ must be odd, which, combined with Alexander duality selecting $D=3$, pins the octave gap that appears in the mass ladder and in the RS-native constants ($\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$). Downstream consumers that need a bundled hypothesis-free package of the gap identities take this certificate rather than re-importing the nine separate lemmas. No used-by edges are recorded yet; the object is the terminal packaging step of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.