dag: fix 3 critical jiggles, document 10 known

FIXED:
  PhotonTorsionProbe.lean:37 — placeholder theorem (proved 1>0)
  DESIInvariant.lean:208-221 — 4 vacuous sigma-range theorems
  UniversalBridge.lean:261 — missing .isSome for intermittency(3150)

DOCUMENTED (known jiggles):
  Moody chart slopes (heuristic but acceptable)
  wa has no SM derivation (largest open question)
  w0 projection formula (self-acknowledged heuristic)
  alpha = max|beta|/(4*pi) (invented relation)
  CMB Q factor 13 discrepancy (unresolved)
  10 known jiggles total, 69/82 theorems clean (84%)

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
 
 -- ═══════════════════════════════════════════════════════════════════════════

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)

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!

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 |