Pith. sign in

IndisputableMonolith.Constants.AlphaGenesis

IndisputableMonolith/Constants/AlphaGenesis.lean · 63 lines · 0 declarations

show as:
view math explainer →

open module explainer GitHub source

Explainer status: pending

   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

source mirrored from github.com/jonwashburn/shape-of-logic