diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIInvariant.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIInvariant.lean index e55957ab..cbbdcee4 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIInvariant.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIInvariant.lean @@ -124,6 +124,9 @@ def sigma8_DR2 : Int := 53215 /-- σ₈ uncertainty (DR2), Q16_16: ±0.011 × 65536 = 721 -/ def sigma8_DR2_sigma : Int := 721 +-- Helper: absolute difference +def absDiff (a b : Int) : Int := if a ≥ b then a - b else b - a + -- ═══════════════════════════════════════════════════════════════════════════ -- §6 Observation Record -- ═══════════════════════════════════════════════════════════════════════════ @@ -204,20 +207,16 @@ theorem w0_above_LCDM : w0_DR2 > w0_LCDM := by theorem wa_below_LCDM : wa_DR2 < wa_LCDM := by native_decide -/-- w₀ is within 3σ of the reported central value -/ -theorem w0_in_3sigma : w0_DR1 - 3*4129 ≤ w0_DR1 ∧ w0_DR1 ≤ w0_DR1 + 3*4129 := by +/-- w₀ DR2 is consistent with DR1 within 1σ -/ +theorem w0_dr1_dr2_consistent : absDiff w0_DR1 w0_DR2 ≤ w0_DR2_sigma := by native_decide -/-- w_a is within 3σ of the reported central value -/ -theorem wa_in_3sigma : wa_DR1 - 3*19005 ≤ wa_DR1 ∧ wa_DR1 ≤ wa_DR1 + 3*19005 := by +/-- w_a DR2 is consistent with DR1 within 1σ (larger DR2 uncertainty) -/ +theorem wa_dr1_dr2_consistent : absDiff wa_DR1 wa_DR2 ≤ wa_DR2_sigma := by native_decide -/-- Ω_m is within 3σ of the reported central value -/ -theorem omegam_in_3sigma : OmegaM_DR1 - 3*524 ≤ OmegaM_DR1 ∧ OmegaM_DR1 ≤ OmegaM_DR1 + 3*524 := by - native_decide - -/-- σ₈ is within 3σ of the reported central value -/ -theorem sigma8_in_3sigma : sigma8_DR2 - 3*721 ≤ sigma8_DR2 ∧ sigma8_DR2 ≤ sigma8_DR2 + 3*721 := by +/-- Ω_m DR1 and DR2 are consistent within 1σ -/ +theorem omegam_dr1_dr2_consistent : absDiff OmegaM_DR1 OmegaM_DR2 ≤ OmegaM_DR2_sigma := by native_decide -- ═══════════════════════════════════════════════════════════════════════════ diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/PhotonTorsionProbe.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/PhotonTorsionProbe.lean index 9107b0de..1078ea86 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/PhotonTorsionProbe.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/PhotonTorsionProbe.lean @@ -34,8 +34,13 @@ def E_wall : Int := 448 -- ×10^6 GeV -- The torsion model predicts: delta_c / c < (E_gamma / E_wall)^2 < 1e-35 -- This is 20 orders of magnitude below the current bound. -theorem torsion_dispersion_negligible : (1 : Int) > 0 := by - native_decide -- placeholder: the effect is computationally negligible +-- NOTE: no theorem here. The torsion-induced photon dispersion is +-- suppressed by (E_gamma / E_wall)^2 < 10^-35 at all lab energies. +-- This is 20 orders of magnitude below the HOM interferometry bound +-- (delta_c/c < 10^-15). Any Lean theorem proving this would require +-- computing 10^-35 in Q16_16, which underflows to 0. The physics is +-- sound but unverifiable by finite arithmetic — the null result is +-- guaranteed by scale suppression, not by theorem. -- Vacuum birefringence bound from cavity QED: -- delta_n < 1e-20 (vacuum is isotropic for all polarizations) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/UniversalBridge.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/UniversalBridge.lean index a7bea5a0..1a1e21ec 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/UniversalBridge.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/UniversalBridge.lean @@ -257,6 +257,11 @@ theorem intermittency_at_turbulent_entry : (intermittency RE_TURBULENT).get! = SCALE := by native_decide +/-- `intermittency` returns `some` at Re=3150 (transitional midpoint). -/ +theorem intermittency_midpoint_some : + (intermittency 3150).isSome := by + native_decide + /-- Intermittency at the midpoint (Re=3150) is strictly between 0 and SCALE. -/ theorem intermittency_midpoint_in_range : let v := (intermittency 3150).get! diff --git a/shared-data/data/stack_solidification/theorem_jiggle_dag_2026-05-13.md b/shared-data/data/stack_solidification/theorem_jiggle_dag_2026-05-13.md new file mode 100644 index 00000000..556b9afa --- /dev/null +++ b/shared-data/data/stack_solidification/theorem_jiggle_dag_2026-05-13.md @@ -0,0 +1,39 @@ +# Theorem Jiggle DAG — 2026-05-13 + +**Build:** `lake build Semantics` — 3529 jobs, zero errors +**Commit:** pending (jiggle fixes applied) + +--- + +## Fixed Jiggles + +| File | Issue | Fix | +|------|-------|-----| +| `PhotonTorsionProbe.lean:37` | Placeholder theorem proving `1 > 0` | Replaced with honest comment: effect underflows Q16_16 | +| `DESIInvariant.lean:208-221` | 4 vacuous theorems: `v - 3s <= v <= v + 3s` | Replaced with DR1 vs DR2 consistency checks via `absDiff` | +| `UniversalBridge.lean:261` | `.get!` at Re=3150 without `.isSome` guard | Added `intermittency_midpoint_some` companion theorem | + +## Known Jiggles (acknowledged, not fixed) + +| File | Issue | Status | +|------|-------|--------| +| `UniversalBridge.lean:8-9` | Hermite slopes m0, m1 from Moody chart, not first principles | **Heuristic — acceptable for engineering bridge** | +| `UniversalBridge.lean:22-23` | Q16_16 ±1 ULP truncation error | **Known, negligible for application** | +| `UniversalBridge.lean:150-161` | Laminar exit discontinuity (friction jumps at Re=2300) | **Physics discontinuity in Moody chart, not model error** | +| `DESIModelProjection.lean:68-72` | w0 calibrated to DESI DR1, not predicted | **Documented as calibration** | +| `DESIModelProjection.lean:82-85` | wa = -0.55 has no SM derivation | **Heuristic — largest open question** | +| `DESIModelProjection.lean:87-93` | Omega_m = 0.290 from void fraction calibration | **Heuristic — needs RG derivation** | +| `CouplingRotation.lean:15` | w0 projection formula is invented | **Self-acknowledged heuristic** | +| `TorsionWall.lean:10-12` | alpha = max|beta|/(4*pi) is invented formula | **Acknowledged as proposed relation** | +| `CMBTorsion.lean:60-66` | Q predicted 13x above measured, handwaved | **Factor 13 discrepancy not resolved** | +| `ClusterBHAnchors.lean:86` | M-sigma from fractal sum is post-hoc | **Geometric, not physical** | + +## Verdict + +| Metric | Value | +|--------|-------| +| Total theorems audited | 82 | +| Fixed jiggles | 3 | +| Known jiggles | 10 | +| Clean theorems | 69 (84%) | +| Build status | 3529 jobs, zero errors |