Gap45Cert
plain-language theorem explainer
Master certificate type packaging the gap-45 facts forced by spatial dimension D=3: configuration dimension 5, nine ledger parities, dimension gap 45, coprimality of 2^D with the gap, E_coh=φ^{-5}, and the matter-coherence balance φ^{1-45}·φ^{45}=φ. Anyone citing B-22 or the φ-ladder mass/coherence link uses this bundle. It is a pure structure definition; proofs live in the field constructors of gap45_cert.
Claim. A certificate recording that at spatial dimension $D=3$: the recognition-event configuration dimension equals $5$; the independent ledger parity count equals $9$ and matches the enumerated parity index; the dimension gap $D^2(D+2)$ equals $45$; $\gcd(2^D,45)=1$; the coherence energy is $E_{\mathrm{coh}}=\varphi^{-5}$; the balance identity $\varphi^{A-\mathrm{gap}}\cdot\varphi^{\mathrm{gap}}=\varphi$ holds with active-edge count $A=1$; and coprimality of $2^d$ with $d^2(d+2)$ holds for every odd $d$ and fails for every even $d\ge 2$.
background
Module GapDerivation closes boundary item B-22: a recognition event has $D+2$ independent degrees of freedom ($D$ spatial from the lattice/T8, one temporal tick advance/T2, one ledger-balance neutrality $J(x)=J(x^{-1})$/T3). Coherence energy is one factor $\varphi^{-1}$ per degree of freedom, so $E_{\mathrm{coh}}=\varphi^{-(D+2)}$. At the forced $D=3$ this is $\varphi^{-5}$, matching the constant used elsewhere in RS.
Configuration dimension is $\mathrm{configDim}(d)=d+2$. Parity count is $d^2$ (at $D=3$ the linear formula $3D$ coincides with $D^2$). Dimension gap is their product: $\mathrm{dimensionGap}(d)=d^2(d+2)$. Active edge count per tick is the integer $A=1$. The balance identity packages the matter-coherence link $\eta_B\cdot\Theta_{\mathrm{crit}}=\varphi^A=\varphi$ with $\eta_B=\varphi^{A-\mathrm{gap}}$ and $\Theta_{\mathrm{crit}}=\varphi^{\mathrm{gap}}$.
Upstream facts already proved in-module include $\mathrm{configDim},3=5$, $\mathrm{parityCount},3=9$, gap $=45$, and the odd/even coprimality dichotomy that supplies a fourth argument that $D$ must be odd.
proof idea
No proof body: Gap45Cert is a structure (certificate type). Each field is a Prop naming one of the gap-45 claims. The inhabited instance gap45_cert fills the fields by applying the already-proved lemmas configDim_at_D3, parityCount_at_D3, parityCount_matches_enumeration, gap_at_D3, coprime_at_D3, and the corresponding ecoh/balance/odd-even coprimality results. Consumers only need to pattern-match on a Gap45Cert value.
why it matters
This is the master certificate for the gap-45 derivation. Combined with Alexander duality selecting $D=3$, gap 45 follows from spatial dimension alone, closing B-22 and locking $E_{\mathrm{coh}}=\varphi^{-5}$ (the RS-native $\hbar\sim\varphi^{-5}$ scale). The balance field is the matter-coherence link $\varphi^{1-45}\cdot\varphi^{45}=\varphi$ used on the $\varphi$-ladder. Coprimality of $2^D$ with the gap is a fourth odd-$D$ constraint alongside the forcing chain (T8 forces $D=3$). Downstream, gap45_cert builds the concrete witness; Constants.tau0_pos sits in the same constants layer that consumes the coherence scale. Status of the module: 0 sorry, 0 axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.