IndisputableMonolith.Constants.AlphaGenesis
IndisputableMonolith/Constants/AlphaGenesis.lean · 63 lines · 0 declarations
show as:
view math explainer →
1import IndisputableMonolith.Constants.AlphaGenesis.ResummationForcing
2import IndisputableMonolith.Constants.AlphaGenesis.PatternForcing
3import IndisputableMonolith.Constants.AlphaGenesis.LoopCertificate
4import IndisputableMonolith.Constants.AlphaGenesis.ResidualTarget
5import IndisputableMonolith.Constants.AlphaGenesis.CalibrationForcing
6import IndisputableMonolith.Constants.AlphaGenesis.SpectralForcing
7import IndisputableMonolith.Constants.AlphaGenesis.MeasurementVerdict
8import IndisputableMonolith.Constants.AlphaGenesis.KappaGammaIrreducibility
9
10/-!
11# Alpha Genesis (aggregator)
12
13The forward derivation of the fine-structure constant, replacing the
14backwards (display-first) assembly. Mirror of the mass-derivation program.
15
16* `ResummationForcing` (M1): the exponential dressing is forced by the same
17 factorization premise that forces the T9 measure; the additive form (A) is
18 excluded. `alphaInv = seed · contWeight(w₈/seed)`: the α dressing IS the
19 forced measure.
20* `PatternForcing` (M2): the φ-pattern is forced by T6 self-similarity on
21 the T7 carrier; the spectral decay envelope IS the forced measure; pattern
22 and measure are reciprocal displays.
23* `LoopCertificate` (M3): the EM recognition loop (channel budget = Gauss-
24 Bonnet × passive edges), the forward definition `alphaInvGenesis`, the
25 identity with the certified pipeline, the proved band, and
26 `AlphaGenesisCert`. One named BRIDGE input: the channel-budget reading.
27* `ResidualTarget` (M4, quarantine): the only module that sees CODATA.
28 Residual bounds, the unique `closingLoad`, and the seam-derivation
29 falsifier with the binding anti-epicycle rule.
30* `CalibrationForcing` (M5): the calibration is NOT an input. A
31 factorizing, antitone response whose step satisfies the self-similar
32 balance is forced to `φ⁻ᵗ` with zero normalization choices; the M1
33 calibrated response is its natural-units display.
34* `SpectralForcing` (M6): the `sin²(kπ/8)` oscillation factor IS one
35 quarter of the difference-operator spectrum on the DFT-8 eigenbasis
36 (trig closure `|ω₈ᵏ−1|² = 4sin²(kπ/8)`); every nonzero mode weight
37 factors as spectrum × forced measure.
38
39* `MeasurementVerdict` (M7): the measurement verdict on the first-order
40 construction. `alphaInvGenesis > alpha_inv_CODATA + 0.0007`, i.e. the
41 first-order value is excluded at more than 30,000σ. Any build that carries
42 the construction also carries its measured exclusion.
43* `KappaGammaIrreducibility` (M8): the structural reason the miss cannot be
44 repaired by more forced kinematics. Every listed forced-closure fact on Q₃
45 is κ_γ-independent, `α⁻¹ = κ_γ × (forced stiffness)` sweeps every positive
46 value with the closure intact (`alphaInv_irreducible_under_closure`), and no
47 normalization-blind condition whatever can pin the coupling
48 (`kappa_blind_closure_cannot_pin`). Within RS the exact value of `α⁻¹(0)` is
49 the free U(1) kinetic normalization: a boundary datum, not a derived
50 constant.
51
52M1–M3 and M5–M6 are blind to measurement by construction. M7 is the
53quarantined CODATA contact; importing it HERE (at the aggregator, downstream
54of the whole forward chain) preserves the quarantine while making the verdict
55reachable from every build target that carries the construction.
56
57CANONICAL POSITION (post-retraction): the forced content of the photon sector
58is kinematic (channel, 4π closure, cycle rank b₁ = 5); the coupling's value is
59the free normalization κ_γ (M8); the first-order construction value is excluded
60by measurement (M7); the unique second-order closing load δ₂ (M4) is OPEN and
61may not be reverse-engineered from proximity to CODATA.
62-/
63