#!/usr/bin/env python3
r"""
The alpha construction, honestly: the CANONICAL certified pipeline.

This script mirrors, step for step, the Lean 4 modules that carry the
Recognition Science fine-structure construction:

    IndisputableMonolith/Constants/GapWeight/Formula.lean      (phi-pattern, DFT-8, weights)
    IndisputableMonolith/Constants/GapWeight/Projection.lean   (Parseval + 64-cell projection)
    IndisputableMonolith/Constants/GapWeight.lean              (closed form w8, THEOREM-equal)
    IndisputableMonolith/Constants/Alpha.lean                  (alphaInv = 44pi * exp(-f_gap/44pi))
    IndisputableMonolith/Numerics/Interval/AlphaBounds.lean    (certified band 137.030..137.039)
    IndisputableMonolith/Constants/AlphaGenesis/*.lean         (the verdict modules)

What it verifies:
  1. The gap weight w8 computed as the Parseval-normalized 64-cell projection of
     the DFT-8 of the phi-pattern equals the parameter-free closed form
     (348 + 210*sqrt(2) - (204 + 130*sqrt(2))*phi) / 7  to machine precision.
     (Lean theorem: GapWeight.ProjectionEquality.w8_projection_equality, 0 sorry.)
  2. The assembled alpha^-1 = 44pi * exp(-w8*ln(phi)/(44pi)) lies in the certified
     band (137.030, 137.039).  (Lean theorems alphaInv_gt, alphaInv_lt.)
  3. The MEASUREMENT VERDICT: the assembled value EXCEEDS CODATA by ~0.00077,
     i.e. ~5.6 ppm, more than 30,000 sigma. The Lean proves this miss
     (MeasurementVerdict.alphaInvGenesis_exceeds_CODATA_by_0007,
      margin_0007_gt_30000_sigma). The construction is NOT the exact alpha.
  4. The seed audit: 44pi = 4pi*11 is an IDENTIFICATION, not a derived coupling.
     The gauge-invariant photon count on the cube is the cycle rank E-V+1 = 5,
     not 11 (U1Normalization.cube_cycle_rank_eq_5); the genuine quadratic J-cost
     of the cube curvature is pi^2, not 4pi*11 (CurvatureJCostVerdict).

Appendix: the RETIRED legacy pipeline (numeric-certificate w8 = 2.488254397846,
additive assembly with delta_kappa) that landed 0.6 ppb from CODATA, and why it
was retired: that w8 was a stored number, not a derivation, and backward-solving
shows it simply encodes CODATA. The derived w8 gives an honest, proved miss.

Dependencies: numpy only. Runtime: well under a second. No files written.
"""

import numpy as np

PHI = (1 + np.sqrt(5)) / 2
LN_PHI = np.log(PHI)

# External anchor exactly as IndisputableMonolith/Constants/ExternalAnchors.lean
ALPHA_INV_CODATA = 137.035999177
ALPHA_INV_CODATA_SIGMA = 0.000000021


def section(title):
    print()
    print("=" * 64)
    print(title)
    print("=" * 64)


# ---------------------------------------------------------------------------
# Part 1: w8 from first principles (mirrors GapWeight/Formula.lean + Projection.lean)
# ---------------------------------------------------------------------------
section("PART 1: THE GAP WEIGHT w8, DERIVED (mirrors the Lean projection)")

t = np.arange(8)
pattern = PHI ** t  # phiPattern: forced by the 8-tick (T7) and the phi-ladder (T6)

# dft8_entry t k = omega^(t*k)/sqrt(8);  phiDFTCoeff k = sum_t conj(entry)*pattern
omega = np.exp(2j * np.pi / 8)
coeff = np.array([np.sum(np.conj(omega ** (t * k) / np.sqrt(8)) * pattern) for k in range(8)])
amp = np.abs(coeff) ** 2  # phiDFTAmplitude

print("phi-pattern phi^t, t = 0..7:")
print(" ", np.array2string(pattern, precision=6))
print("DFT-8 mode energies |c_k|^2:")
for k in range(8):
    print(f"  k={k}: {amp[k]:.10f}")

# Parseval: total DFT energy must equal the closed form (phi^16 - 1)/phi
E_total = np.sum(amp)
E_closed = (PHI ** 16 - 1) / PHI
print(f"\nParseval total:   {E_total:.10f}")
print(f"(phi^16-1)/phi:   {E_closed:.10f}")
print(f"match:            {np.isclose(E_total, E_closed, rtol=0, atol=1e-9)}")

# geometricWeight k = sin^2(k*pi/8) * phi^(-k) for k != 0 (spectral weight of the
# discrete 8-tick derivative x conjugate ladder envelope; forced, see Projection.lean)
gweight = np.array([0.0] + [np.sin(k * np.pi / 8) ** 2 * PHI ** (-k) for k in range(1, 8)])

# w8_projected = 64 * (sum_k |c_k|^2 * gweight_k) / (sum_k |c_k|^2)
# 64 = 8 ticks x 8 vertices of the Q3 cell: the fundamental RS interface cell.
w8_candidate_sum = np.sum(amp * gweight)
w8_projected = 64 * (w8_candidate_sum / E_total)

# Closed form (GapWeight.lean): integers forced by the algebra, not chosen
w8_closed = (348 + 210 * np.sqrt(2) - (204 + 130 * np.sqrt(2)) * PHI) / 7

print("\nPer-mode contribution to w8 (64 * |c_k|^2 * gweight_k / E_total):")
for k in range(1, 8):
    print(f"  k={k}: {64 * amp[k] * gweight[k] / E_total:.6f}")

print(f"\nw8 (projection):  {w8_projected:.13f}")
print(f"w8 (closed form): {w8_closed:.13f}")
print(f"difference:       {abs(w8_projected - w8_closed):.2e}")
print("This equality is a Lean THEOREM (w8_projection_equality, 0 sorry):")
print("the projection and the closed form are the same number, derived, not fitted.")

# ---------------------------------------------------------------------------
# Part 2: the assembly (mirrors Constants/Alpha.lean)
# ---------------------------------------------------------------------------
section("PART 2: THE ASSEMBLY alpha^-1 = 44pi * exp(-w8*ln(phi)/(44pi))")

seed = 44 * np.pi          # alpha_seed: 4pi (Gauss-Bonnet on the cube boundary) x 11
f_gap = w8_closed * LN_PHI  # f_gap = w8 * ln(phi), forced with zero alpha-input
alpha_inv = seed * np.exp(-f_gap / seed)

print(f"seed 44*pi:       {seed:.10f}   (IDENTIFICATION, see Part 4)")
print(f"f_gap = w8*ln(phi): {f_gap:.10f}   (forced, zero alpha-input)")
print(f"alpha^-1 assembled: {alpha_inv:.9f}")

in_band = 137.030 < alpha_inv < 137.039
print(f"\ncertified band (137.030, 137.039): {'INSIDE' if in_band else 'OUTSIDE'}")
print("(Lean theorems alphaInv_gt / alphaInv_lt certify the band.)")

# ---------------------------------------------------------------------------
# Part 3: the measurement verdict (mirrors AlphaGenesis/MeasurementVerdict.lean)
# ---------------------------------------------------------------------------
section("PART 3: THE MEASUREMENT VERDICT (the construction MISSES, provably)")

overshoot = alpha_inv - ALPHA_INV_CODATA
ppm = overshoot / ALPHA_INV_CODATA * 1e6
n_sigma = overshoot / ALPHA_INV_CODATA_SIGMA

print(f"CODATA alpha^-1:  {ALPHA_INV_CODATA} +/- {ALPHA_INV_CODATA_SIGMA}")
print(f"assembled value:  {alpha_inv:.9f}")
print(f"overshoot:        +{overshoot:.9f}")
print(f"relative:         +{ppm:.2f} ppm")
print(f"in CODATA sigma:  {n_sigma:,.0f} sigma")
print()
print("Lean proves: overshoot > 0.0007 (alphaInvGenesis_exceeds_CODATA_by_0007)")
print(f"  check: {overshoot:.9f} > 0.0007  ->  {overshoot > 0.0007}")
print("Lean proves: 0.0007 > 30000 * sigma (margin_0007_gt_30000_sigma)")
print(f"  check: 0.0007 > {30000 * ALPHA_INV_CODATA_SIGMA:.6f}  ->  {0.0007 > 30000 * ALPHA_INV_CODATA_SIGMA}")
print()
print("VERDICT: the parameter-free construction lands 5.6 ppm ABOVE the measured")
print("alpha^-1 and is excluded as the exact value at >30,000 sigma, by our own")
print("Lean theorems. The exact infrared alpha^-1 is OPEN: a boundary condition")
print("the present formalization does not derive.")

# ---------------------------------------------------------------------------
# Part 4: the seed audit (mirrors the AlphaGenesis quarantine verdict modules)
# ---------------------------------------------------------------------------
section("PART 4: WHY THE SEED 44pi IS AN IDENTIFICATION, NOT A DERIVATION")

E, V = 12, 8  # edges and vertices of the cube Q3
cycle_rank = E - V + 1
print(f"U1Normalization: gauge-invariant photon count on Q3 = cycle rank E-V+1 = {cycle_rank}")
print(f"  The '11' in 44pi is the passive-edge LEDGER count (12 - 1), not the gauge count.")
print(f"  A genuine gauge seed would be 4pi*{cycle_rank} = {4 * np.pi * cycle_rank:.2f}, excluded by measurement.")
print(f"CurvatureJCostVerdict: the genuine quadratic J-cost of the cube curvature")
print(f"  is pi^2 = {np.pi ** 2:.4f}; 4pi = {4 * np.pi:.4f} is a linear Gauss-Bonnet invariant, not a cost.")
print(f"  So reading 4pi*11 = {seed:.2f} as a recognition cost is a category error.")
print(f"ScaleIdentification: the assembled {alpha_inv:.6f} exceeds the Thomson ceiling")
print(f"  alpha^-1(0) = {ALPHA_INV_CODATA}, so it is off the physical running curve at EVERY scale.")

# ---------------------------------------------------------------------------
# Appendix: the retired legacy pipeline, and why it had to go
# ---------------------------------------------------------------------------
section("APPENDIX: THE RETIRED LEGACY PIPELINE (a cautionary tale)")

w8_legacy = 2.488254397846                    # the old stored numeric certificate
delta_kappa = -103 / (102 * np.pi ** 5)       # legacy curvature correction (Alpha.lean: retired)
alpha_inv_legacy = seed - w8_legacy * LN_PHI - delta_kappa
legacy_ppb = (alpha_inv_legacy - ALPHA_INV_CODATA) / ALPHA_INV_CODATA * 1e9

# Backward-solve: the w8 the additive assembly NEEDS to hit CODATA exactly
w8_required = (seed - delta_kappa - ALPHA_INV_CODATA) / LN_PHI

print("The repository once carried w8 as a stored NUMBER (2.488254397846) and an")
print("additive assembly  alpha^-1 = 44pi - w8*ln(phi) - delta_kappa :")
print(f"  legacy assembly:  {alpha_inv_legacy:.9f}   ({legacy_ppb:+.2f} ppb from CODATA)")
print(f"  w8 required to hit CODATA exactly: {w8_required:.12f}")
print(f"  stored legacy w8:                  {w8_legacy:.12f}")
print(f"  difference: {abs(w8_required - w8_legacy):.2e}  <- the stored number just encoded CODATA")
print()
print("That ppb 'agreement' was retired (GapWeight.lean: a numeric certificate is")
print("'no longer acceptable for the no-free-parameters claim'). The derived w8 is")
print(f"{w8_closed:.10f}, the certified assembly is exponential, and the honest")
print("result is the proved 5.6 ppm miss above. A construction that cannot miss")
print("is not evidence; this one can, and does, and the Lean says exactly where.")

# ---------------------------------------------------------------------------
# Chart data (consumed by the lab page)
# ---------------------------------------------------------------------------
section("CHART DATA")
print(f"band_lo 137.030")
print(f"band_hi 137.039")
print(f"alpha_inv {alpha_inv:.9f}")
print(f"codata {ALPHA_INV_CODATA}")
print(f"codata_sigma {ALPHA_INV_CODATA_SIGMA}")
print(f"legacy {alpha_inv_legacy:.9f}")
for k in range(1, 8):
    print(f"mode {k} {64 * amp[k] * gweight[k] / E_total:.6f}")