v3.3.30: L5 computed spectrum + L6 spectral democracy + PDG 2025

[gift-framework]

L5 (v3.3.29): Formalize headline Spectral Physics paper results:

• ComputedSpectrum.lean: Q22 signature (3,19), SD/ASD gap >2000x, gauge coupling B-test at 0.24%, sin²θ_W and α_s deviation bounds
• Certificate/Spectral: 23 → 26 conjuncts

L6 (v3.3.30): Spectral democracy + experimental update:

• SpectralDemocracy.lean: SD eigenvalue near-degeneracy (spread <2%), coupling ratio <1.02, generation universality (8-conjunct cert)
• sin²θ_W updated PDG 2024 → PDG 2025 (0.23122 → 0.23129)
• Certificate/Spectral: 26 → 29 conjuncts, total 161

Zero new axioms. 124 published files, 2659 build jobs.

---

Note

Low Risk
Mostly additive Lean formalization and documentation updates, with minor risk of breaking builds via import/re-export or certificate conjunct changes rather than behavioral/runtime impact.

Overview
Adds two new Spectral modules to formalize numerically-verified results from the Spectral Physics paper: ComputedSpectrum (Q22 signature/SD=N_gen, SD/ASD eigenvalue gap, gauge-coupling B-test, coupling deviation checks) and SpectralDemocracy (SD eigenvalue near-degeneracy and coupling universality), both proved via native_decide and introducing no new axioms.

Extends Certificate/Spectral.lean and Spectral.lean to import/re-export these results and to include the new checks in the master spectral certificate (conjunct count increases), and updates the sin²θ_W experimental constant/bound to PDG 2025; documentation/versioning (CHANGELOG, docs/USAGE.md, README, gift_core/_version.py) is updated accordingly.

^{Written by Cursor Bugbot for commit 5b95bb8. This will update automatically on new commits. Configure here.}

[cursor]

Cursor Bugbot has reviewed your changes and found 1 potential issue.

Bugbot Free Tier Details

You are on the Bugbot Free tier. On this plan, Bugbot will review limited PRs each billing cycle.

To receive Bugbot reviews on all of your PRs, visit the Cursor dashboard to activate Pro and start your 14-day free trial.

^{Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

[cursor]

min_SD_num holds max eigenvalue, not minimum

Medium Severity

min_SD_num is defined as 4863 and documented as "Smallest SD eigenvalue lower bound," but SpectralDemocracy.lean (same PR) reveals the three SD eigenvalues are λ₁=4.863, λ₂=4.821, λ₃=4.779 — making the actual minimum 4779 (sd_ev_3_num), not 4863. The value 4863 is the maximum. The sd_asd_gap_large theorem thus proves the gap for the largest SD eigenvalue, not the smallest as claimed. The physical claim still holds (4779 also satisfies the bound), but the formal certificate doesn't prove what its documentation states.

Additional Locations (1)

• Lean/GIFT/Spectral/SpectralDemocracy.lean#L39-L52