AlphaGenesisCert
plain-language theorem explainer
Empty certificate type whose verified predicate packages the full forward α⁻¹ derivation: channel budget 4π·11, forced φ-ladder, forced spectral envelope, forced exp(−ε) dressing (additive excluded), genesis identity with the certified pipeline, and the band (137.030, 137.039). Cite it for the no-fit Alpha Genesis claim. verified_any is a one-line refine that conjoins existing lemmas.
Claim. A genesis certificate is verified precisely when all of the following hold: the EM channel budget equals $4\pi\cdot 11$; every admissible eight-tick ladder satisfies $u_n=\varphi^n$; for each nonzero mode $k\in\{1,\ldots,7\}$ the gap weight equals $\sin^2(k\pi/8)$ times the forced lattice measure; every dressing response is $g(\varepsilon)=e^{-\varepsilon}$ and none equals the additive map $1-\varepsilon$; the forward inverse fine-structure equals the certified pipeline value; and that value lies in the open interval $(137.030,137.039)$.
background
Alpha Genesis defines $\alpha^{-1}$ forward as a property of the EM recognition loop, before any measurement comparison. The channel budget is the voxel-boundary angular total times the passive dressing edges: $\Omega(\partial Q_3)\times E_{\mathrm{passive}}=4\pi\times 11$, both factors cube theorems on the $D=3$ voxel ($D=3$ forced by T8). Spectral load is the Parseval-normalized DFT-8 gap weight of the forced $\varphi$-pattern, distributed over that budget. Dressing is the unique factorizing recognition weight (T9 forced measure) at that load.
The forward object is $\mathrm{alphaInvGenesis}:=\mathrm{channelBudget}\cdot\mathrm{contWeight}(\mathrm{spectralLoad})$. Upstream, alphaInvGenesis_eq_alphaInv identifies it with the certified pipeline alphaInv (canonical exponential resummation of the seed), and alphaInvGenesis_band transfers the proved numerical window. Calibration forcing supplies $g(t)=e^{-t}$ on nonnegative loads with the additive display excluded. Pattern forcing supplies $u_n=\varphi^n$ on every eight-tick ladder (T6 self-similarity on the T7 carrier).
proof idea
The structure itself is empty (unit-like, Inhabited). The verified predicate is the six-way conjunction written in the body. The companion theorem verified_any is a single refine that discharges each conjunct by an existing lemma: channelBudget_eq for the seed; EightTickLadder.pattern_forced for the $\varphi$-ladder; geometricWeight_eq_sin_mul_forced_measure for the envelope; DressingResponse.response_forced and no_additive_response for the dressing clauses; alphaInvGenesis_eq_alphaInv for the genesis identity; alphaInvGenesis_band for the numerical window. No new arithmetic is performed here.
why it matters
This is the Alpha Genesis certificate: the single place that bundles the forward EM-loop derivation of $\alpha^{-1}$ with no measurement clause. It records the status table of the four discrete choices: resummation form forced (M1), canonical $\varphi$-pattern forced (M2), cube reading of the seed structural (Gauss-Bonnet + passive edges), and $D=3$ forced upstream (T8). The honest remaining input is named once as the channel-budget bridge (inverse coupling = angular budget × passive channels), a physical identification with no continuous freedom.
Framework landmarks hit directly: T6 ($\varphi$ fixed point), T7 (eight-tick octave), T8 ($D=3$), the forced measure, and the RS alpha band $(137.030,137.039)$. The IR boundary $\alpha^{-1}(0)=137.035999$ remains OPEN; this certificate does not close it. No downstream consumers are wired yet; the object is the terminal packaging of the M3 loop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.