diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/CalibrationImplications.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/CalibrationImplications.lean
deleted file mode 100644
index fe2a7634..00000000
--- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/CalibrationImplications.lean
+++ /dev/null
@@ -1,119 +0,0 @@
--- CalibrationImplications.lean
---
--- What the Higgs/DESI calibration implies for the two core applications:
---   1. COMPRESSION: maximum achievable compression ratio from Menger voids
---   2. NAVIER-STOKES: Reynolds regime transition rate from boundary growth
---
--- Key result: Menger compression ALWAYS outpaces Koch boundary roughening
--- per iteration. Net ratio: (27/20) / (4/3) = 1.0125 > 1.
-
-namespace Semantics.Physics.CalibrationImplications
-
-def SCALE : Int := 65536
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §0  Calibrated constants
--- ═════════════════════════════════════════════════════════════════════════════
-
--- Menger void fraction per iteration: 20/27 = 0.7407
--- (20 of 27 subcubes survive each iteration)
-def mengerFrac : Int := 48549
-
--- Koch boundary growth per iteration: 4/3 = 1.3333
--- (each boundary segment becomes 4 shorter segments)
-def kochFrac : Int := 87381
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §1  Compression ratios
--- ═════════════════════════════════════════════════════════════════════════════
-
--- Compression ratio per Menger iteration: (27/20) = 1.35x
--- Q16_16: 1.35 * 65536 = 88474
-def compPerIter : Int := 88474
-
--- Compression ratio after n iterations: (27/20)^n
--- For n=3 (observable cosmic void iterations):
--- (27/20)^3 = 1.35^3 = 2.46x
--- Q16_16: 2.46 * 65536 = 161218
-def compN3 : Int := 161218
-
--- For n=4 (codebase-memory at N=64):
--- (27/20)^4 = 3.32x
--- Q16_16: 3.32 * 65536 = 217579
-def compN4 : Int := 217579
-
--- For n=6 (human scale 1m at 1mm):
--- (27/20)^6 = 6.05x
--- Q16_16: 6.05 * 65536 = 396493
-def compN6 : Int := 396493
-
--- Compression exceeds the benchmark zlib/gzip ratio (~3x) at n=4
-theorem comp_n4_exceeds_gzip : compN4 > 3 * SCALE := by native_decide
-
--- Compression improves with each iteration
-theorem compression_monotonic : compN3 < compN4 ∧ compN4 < compN6 := by native_decide
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §2  Navier-Stokes regime transition
--- ═════════════════════════════════════════════════════════════════════════════
-
--- Boundary growth coefficient: alpha = ln(4)/ln(3) * (4/3 - 1) = 0.00694
--- From Koch dimension D_K = 1.2619. Normalized: ~0.007.
--- Q16_16: 0.007 * 65536 = 459
-def boundaryGrowth : Int := 459
-
--- Torsion coupling coefficient: beta = lambda/32 = 0.129/32 = 0.00403
--- From Higgs self-coupling calibrated at CERN. Normalized: ~0.003.
--- Q16_16: 0.003 * 65536 = 197
-def torsionCoupl : Int := 197
-
--- Boundary growth at turbulent midpoint (Re=4000, A=1):
--- dA/dt = boundaryGrowth + torsionCoupl * ||tau||^2
--- The growth is always positive at turbulent Re
-theorem turbulent_growth_positive : boundaryGrowth + torsionCoupl > 0 := by
-  native_decide
-
--- Laminar regime (Re < 2300, A=0): no growth
-def laminarGrowth : Int := 0
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §3  Compression-boundary tradeoff (key result)
--- ═════════════════════════════════════════════════════════════════════════════
-
--- Menger compression per iteration: (27/20) = 1.35
--- Koch boundary growth per iteration: (4/3) = 1.333
--- Net per iteration: (27/20) / (4/3) = 1.0125 > 1
--- Q16_16: 1.0125 * 65536 = 66355
-def netPerIter : Int := 66355
-
--- Net > 1 means compression always outpaces boundary roughening
-theorem net_exceeds_one : netPerIter > SCALE := by
-  native_decide
-
--- Boundary complexity grows slower than volume compresses
--- This is guaranteed by the fractal dimensions:
---   d_H = ln(20)/ln(3) = 2.727  (Menger)
---   D_K = ln(4)/ln(3) = 1.262  (Koch)
---   d_H - D_K = 1.465 > 0, so compression always wins
--- The cumulative advantage grows with each iteration:
--- Net after n iterations: (1.0125)^n
-theorem cumulative_net_advantage_grows : netPerIter * netPerIter > netPerIter := by
-  native_decide  -- compound compression outpaces single-iteration growth
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §4  Executable receipts
--- ═════════════════════════════════════════════════════════════════════════════
-
--- Compression ratios
-#eval compPerIter    -- 1.35x per iteration
-#eval compN4         -- 3.32x at n=4 (codebase-memory N=64)
-#eval compN6         -- 6.05x at n=6
-
--- Navier-Stokes coefficients
-#eval boundaryGrowth  -- 0.007
-#eval torsionCoupl    -- 0.003
-
--- Tradeoff
-#eval netPerIter     -- 1.0125x net (compression > boundary)
-
-end Semantics.Physics.CalibrationImplications
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/CrossScaleTest.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/CrossScaleTest.lean
deleted file mode 100644
index 7da3d077..00000000
--- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/CrossScaleTest.lean
+++ /dev/null
@@ -1,156 +0,0 @@
--- CrossScaleTest.lean
---
--- Tests the 16D Menger/Koch model across three vastly different scales:
---   CERN (Higgs/Planck): 10^19 GeV   — 6-sigma precision
---   DESI (cosmic web):   10^2 Mpc     — 2-3 sigma precision
---   Human (materials):   1 m at 1 mm  — everyday scale
---
--- If the model is correct, the same void hierarchy geometry applies
--- at every scale. The number of Menger iterations changes with the
--- scale ratio, but the fractal dimension d_H = ln(20)/ln(3) is fixed.
-
-namespace Semantics.Physics.CrossScaleTest
-
-def SCALE : Int := 65536
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §0  Scale-invariant geometry (from Menger/Koch, not fitted)
--- ═════════════════════════════════════════════════════════════════════════════
-
--- Menger sponge: d_H = ln(20)/ln(3) = 2.7268
--- Q16_16: 2.7268 * 65536 = 178696
-def mengerDim : Int := 178696
-
--- Koch curve: D_K = ln(4)/ln(3) = 1.2619
--- Q16_16: 1.2619 * 65536 = 82706
-def kochDim : Int := 82706
-
--- Void fraction per iteration: 20/27 = 0.7407
--- Q16_16: 0.7407 * 65536 = 48549
-def voidFrac : Int := 48549
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §1  Scale 1: CERN (Higgs VEV / Planck mass)
---      Ratio = 246.22 GeV / 1.22e19 GeV = 2.02e-17
---      Menger iterations: n = ln(2.02e-17) / ln(20/27) = 128.1 -> 128
---      (20/27)^128 = 2.08e-17  (2.95% error from v/M_Pl)
---      This is the FUNDAMENTAL constraint: Higgs/Planck ratio determines
---      the deep void count with sub-percent precision from CERN.
--- ═════════════════════════════════════════════════════════════════════════════
-
--- Higgs VEV v = 246.22 GeV (CERN, 6+ sigma)
-def higgsVEV : Int := 24622
-
--- Planck mass M_Pl = 1.22e19 GeV
-def planckMass : Int := 12209
-
--- Menger iterations from Higgs/Planck: n = 128
-def n_cern : Int := 128
-
--- Predicted (20/27)^128 in Q16_16: would be ~0 (too small)
--- The key theorem: the void hierarchy naturally produces the observed
--- ratio between the electroweak and Planck scales.
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §2  Scale 2: DESI (cosmic web BAO scale / Menger cell)
---      BAO scale r_d = 147 Mpc, Menger cell at N=64: ~2.3 Mpc
---      Scale ratio: 147 / 2.3 = 63.9
---      Number of 3-merations: log_3(63.9) = 3.8 -> 4
---      After 4 iterations: void fraction = 1 - (20/27)^4 = 1 - 0.301 = 0.699
---      Observed cosmic void fraction at z=0: 60-80%
---      → Model predicts 70% void fraction, consistent with DESI
--- ═════════════════════════════════════════════════════════════════════════════
-
--- BAO sound horizon: 147 Mpc (raw Int)
-def baoScale : Int := 147
-
--- Menger cell size at N=64: 2.3 Mpc (×10: 23)
-def cellSize : Int := 23
-
--- Menger iterations at DESI scale: n = 4
-def n_cosmic : Int := 4
-
--- Void fraction after 4 iterations: 1 - (20/27)^4 = 1 - 0.301 = 0.699
--- Q16_16: 0.699 * 65536 = 45810
-def voidFrac4 : Int := 45810
-
--- Predicted void fraction is between 0.60 and 0.80 (DESI void catalogues)
-theorem void_fraction_consistent : voidFrac4 > 39322 ∧ voidFrac4 < 52429 := by
-  native_decide  -- 0.60*65536=39322, 0.80*65536=52429
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §3  Scale 3: Human (1 m object at 1 mm resolution)
---      Scale ratio: 1000
---      Menger iterations: log_3(1000) = 6.3 -> 6
---      After 6 iterations: void fraction = 1 - (20/27)^6 = 1 - 0.165 = 0.835
---      The void fraction at human scale is an abstract metric — it doesn't
---      correspond to physical voids in solid objects.
---      But the GEOMETRY is the same: the Menger void hierarchy applies
---      identically. The interpretation changes with the medium.
--- ═════════════════════════════════════════════════════════════════════════════
-
--- Scale ratio: 1000
-def humanScaleRatio : Int := 1000
-
--- Menger iterations: 6
-def n_human : Int := 6
-
--- Void fraction: 1 - (20/27)^6 = 0.835
--- Q16_16: 0.835 * 65536 = 54723
-def voidFracHuman : Int := 54723
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §4  Scale consistency claim
--- ═════════════════════════════════════════════════════════════════════════════
-
--- The model uses the SAME mengerDim and voidFrac at ALL scales.
--- Only n (the number of iterations) changes with the scale ratio.
---
--- The Higgs/Planck ratio gives n = 128 iterations for the COSMOLOGICAL
--- CONSTANT suppression. The BAO scale gives n = 4 iterations for the
--- OBSERVABLE cosmic void fraction. These are consistent:
---   n_CC + n_obs = 128 + 4 = 132 ≈ total e-folds from Planck to observable scale
---
--- Total e-folds from Planck to today: N_total = ln(a_today/a_Planck) ≈ 138
---   n_CC + n_obs = 132 matches N_total ≈ 138 within ~4%
---   This is additional cross-scale consistency: the sum of void iterations
---   across all scales equals the total expansion e-folds.
-
--- Total expansion e-folds: 138
-def totalEfolds : Int := 138
-
--- Sum of void iterations: n_CC + n_obs = 132
-def voidIterationsTotal : Int := 132
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §5  Menger geometry is scale-invariant (the fundamental theorem)
--- ═════════════════════════════════════════════════════════════════════════════
-
--- Menger dimension is strictly between 2 and 3 (fractal, not solid)
-theorem menger_is_fractal : 2 * SCALE < mengerDim ∧ mengerDim < 3 * SCALE := by
-  native_decide
-
--- Koch dimension is strictly between 1 and 2 (boundary is fractal)
-theorem koch_is_boundary_fractal : SCALE < kochDim ∧ kochDim < 2 * SCALE := by
-  native_decide
-
--- Menger dimension exceeds Koch (volume hierarchy dominates boundary roughness)
-theorem menger_exceeds_koch : kochDim < mengerDim := by
-  native_decide
-
--- Void fraction per iteration is less than 1 (suppression is real)
-theorem void_fraction_suppresses : voidFrac < SCALE := by
-  native_decide
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §6  Executable receipts
--- ═════════════════════════════════════════════════════════════════════════════
-
-#eval mengerDim
-#eval kochDim
-#eval voidFrac
-#eval n_cern
-#eval n_cosmic
-#eval voidFrac4
-
-end Semantics.Physics.CrossScaleTest
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIModelProjection.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIModelProjection.lean
index c0f7c16c..6d80ef57 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIModelProjection.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIModelProjection.lean
@@ -1,27 +1,14 @@
 /-
-DESIModelProjection.lean — 16D Horn-Fiber Projection onto DESI Observables
+DESIModelProjection.lean — Model Projection onto DESI Observables
 
-Projects the 16D Menger/Koch/Gabriel-Horn fiber model onto the DESI
-observational invariant set. Computes residuals and declares which
-predictions are within tolerance and which are not.
+Projects a cosmological parameter set (w0, wa, Om, s8) onto the DESI
+observational invariant set. Computes residuals against DESI DR1/DR2.
+
+NOTE: w0 is CALIBRATED to DESI DR1, not predicted.
+      wa, Om, s8 are structural projections that happen to be
+      consistent with DESI within 1s.
 
 Zero Float arithmetic. All values are hardcoded Q16_16 Int literals.
-
-Model components:
-  1. Menger/Koch divergence ratio: D_MK(n) ~ (9/5)^n → predicts w₀ > -1
-  2. Gabriel horn torsion widening: dA/dt > 0 while dV/dt ≈ 0 → predicts w_a < 0
-  3. Fractal void hierarchy: d_H = ln(20)/ln(3) → predicts Ω_m effective reduction
-
-Each projection:
-  model_prediction → compare with DESI observation → residual → verdict
-
-Conventions:
-  PascalCase types, camelCase functions.
-  Q16_16 for dimensionless; raw Int × 100 for dimensional.
-  structure for domain concepts.
-  theorem for residual bounds.
-  #eval! for executable receipts.
-  Namespace: Semantics.Physics.DESIModelProjection
 -/
 
 import Semantics.FixedPoint
@@ -78,9 +65,8 @@ def torsionCoupling : Int := 197
 -- ═══════════════════════════════════════════════════════════════════════════
 
 /--
-Prediction 1: w₀ > -1 (dark energy not cosmological constant).
-Menger/Koch divergence D_MK ~ (9/5)^n produces residual boundary pressure.
-Model calibrated to DESI DR1 w₀ = -0.827.
+Prediction 1: w₀ > -1 is an observational fact (DESI DR1/DR2).
+Model w₀ is CALIBRATED to DESI DR1 w₀ = -0.827.
 Q16_16: -0.827 × 65536 = -54198.
 -/
 def predictW0 : Int := -54198
@@ -89,14 +75,9 @@ def predictW0 : Int := -54198
 def predictW0_sigma : Int := 3277
 
 /--
-Prediction 2: w_a < 0 (dark energy was stronger in the past).
-Gabriel horn torsion: dA_boundary/dt = α·A + β·‖τ‖².
-At higher z, more compact → larger ‖τ‖² → more negative w_a.
-Model predicts w_a ≈ -0.55.
-
-Check: -0.55 × 65536 = -36044.8 ≈ -36045.
-DESI DR1: -0.75. Residual: 0.20 (within 1σ).
-DESI DR2: -0.59. Residual: 0.04 (within 1σ).
+Prediction 2: w_a < 0 is an observational fact (DESI DR1/DR2).
+Model w_a = -0.55 is consistent with DESI DR2 w_a = -0.59 +- 0.25
+at 0.16 sigma.
 -/
 def predictWa : Int := -36045
 
@@ -104,12 +85,10 @@ def predictWa : Int := -36045
 def predictWa_sigma : Int := 9830
 
 /--
-Prediction 3: Ω_m effective from Menger void correction.
-ΛCDM Ω_m ≈ 0.31, Menger (20/27)^3 × 0.31 ≈ 0.13 (too low).
-Real cosmic void fraction ~10% correction: Ω_m ≈ 0.29.
-Q16_16: 0.290 × 65536 = 19005.
+Prediction 3: Ω_m = 0.290 from Menger void correction.
+ΛCDM Ω_m ≈ 0.31. Menger (20/27)^3 × 0.31 ≈ 0.13 (over-correction).
+Real cosmic void fraction ~10%: Ω_m ≈ 0.29.
 DESI DR1: 0.295. Residual: -0.005 (within 1σ).
-DESI DR2: 0.2975. Residual: -0.0075 (within 1σ).
 -/
 def predictOmegaM : Int := 19005
 
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/HiggsCalibration.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/HiggsCalibration.lean
deleted file mode 100644
index 0a607559..00000000
--- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/HiggsCalibration.lean
+++ /dev/null
@@ -1,168 +0,0 @@
--- HiggsCalibration.lean
---
--- Calibrates the 16D Menger/Koch void hierarchy against the Higgs boson
--- parameters (PDG 2024: v = 246.22 GeV, m_H = 125.11 GeV).
---
--- Calibration principle:
---   The Higgs VEV sets the electroweak scale. The ratio v/M_Pl determines
---   the number of Menger void iterations needed to suppress the Higgs
---   vacuum energy to the observed dark-energy level.
---
---   Menger void fraction per iteration: f = 20/27 (20 of 27 subcubes survive)
---   Suppression after n iterations: f^n = (20/27)^n
---
---   Target: (20/27)^n = v/M_Pl = 246.22 / 1.22e19 = 2.02e-17
---   n = ln(v/M_Pl) / ln(20/27) = ln(2.02e-17) / ln(0.7407)
---     = (-38.4) / (-0.300) = 128.1
---
---   Void iterations n = 128 directly from Higgs VEV and Planck scale.
---   No free parameters. This is the calibration.
-
-namespace Semantics.Physics.HiggsCalibration
-
-def SCALE : Int := 65536
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §0  Higgs scale invariants
--- ═════════════════════════════════════════════════════════════════════════════
-
--- Higgs VEV v = 246.22 GeV  (×100: 24622)
-def hVEV : Int := 24622
-
--- Planck mass M_Pl = 1.220910e19 GeV
--- Stored as 1.2209 × 10^19 (×10^15 to fit in Int: 12209)
-def planckMass : Int := 12209
-
--- CERN PDG 2024 precision measurements (> 6 sigma):
---   Top mass: m_t = 172.76 +- 0.30 GeV
---   Higgs mass: m_H = 125.11 +- 0.11 GeV
---   W mass: m_W = 80.377 +- 0.012 GeV
---   Z mass: m_Z = 91.1876 +- 0.0021 GeV
--- Derived from CERN data:
---   lambda = m_H^2 / (2*v^2) = 0.129095  (Q16: 8460)
---   y_t = sqrt(2)*m_t / v = 0.9923     (Q16: 65030)
---   Top-driven running: d(lambda)/d(ln mu) = -6*y_t^4/(16*pi^2) = -0.0369 (Q16: -2418)
-
--- Top Yukawa from CERN m_t = 172.76 GeV
-def topYukawa : Int := 65030
-
--- One-loop Higgs running coefficient (dominated by top)
-def lambdaRunning : Int := -2418
-
--- Ratio v/M_Pl = 246.22 / 1.2209e19 = 2.017e-17
--- This is the natural suppression factor for the cosmological constant.
--- Q16.16: 2.017e-17 × 65536 ≈ 0 (too small for Q16.16)
--- The ratio is stored as raw integer: 2017 (×10^20)
-def vevPlanckRatio : Int := 2017
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §1  Calibration: void iterations from Higgs/Planck ratio
--- ═════════════════════════════════════════════════════════════════════════════
-
--- Menger void fraction per iteration: 20/27 = 0.7407
--- Q16.16: 0.7407 × 65536 = 48549
-def mengerFraction : Int := 48549
-
--- ln(20/27) = ln(0.7407) = -0.300
--- Q16.16: -0.300 × 65536 = -19661
--- Store as absolute value for division: 0.300 × 65536 = 19661
-def lnFraction : Int := 19661
-
--- ln(v/M_Pl) = ln(2.017e-17) = -38.42
--- Stored as ×1000: -38420 (too large for Q16)
--- Raw Int: -38
-def lnRatio : Int := -38
-
--- Menger void iterations n = ln(v/M_Pl) / ln(20/27) = 38.42 / 0.300 = 128.1
--- This is the FUNDAMENTAL calibration: Higgs/Planck ratio → void count.
--- n = 128 iterations directly from known particle physics constants.
-def voidIterations : Int := 128
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §2  Derived cosmological predictions
---
--- These come from the Menger void iteration count n = 128:
---
---     Omega_m = 0.31 * (20/27)^(128/3) * correction
---              = 0.31 * (5.8e-17)^(1/3)
---              = 0.31 * 0.00000387   ← too small, need 0.29
---
--- The issue: the void iterations that suppress vacuum energy (n = 128)
--- are NOT the same as the observable void iterations (n = 2-3 at cosmic scales).
--- The Higgs-to-Planck ratio gives the DEEP void count, but only the
--- TOP FEW iterations are cosmologically observable.
---
--- Observable void iterations ≈ 2-3 (from BAO scale / Menger cell size)
---   n_obs = ln(BAO_scale / Menger_cell) / ln(3)
---         = ln(147 Mpc / 2.3 Mpc) / ln(3)
---         = 4.15 / 1.10 = 3.8
---   So ~4 iterations are observable at DESI scales.
---
--- The Higgs-Planck ratio predicts DEEP iterations (n = 128), not
--- observable ones (n_obs ≈ 4). This is consistent — the vacuum
--- energy suppression happens at all scales, but only the top
--- few iterations affect the cosmic web structure.
---
--- The observable predictions:
---   Omega_m ≈ 0.31 - 0.31 * (1 - (20/27)^n_obs) * void_fraction
---            ≈ 0.31 - 0.31 * (1 - (20/27)^4) * 0.2
---            ≈ 0.31 - 0.31 * 0.699 * 0.2
---            ≈ 0.31 - 0.043 = 0.267 (too low)
---
--- Calibrated using BAO scale → n_obs ≈ 3:
---   Omega_m ≈ 0.31 - 0.31 * (1 - (20/27)^3) * 0.2
---            ≈ 0.31 - 0.31 * 0.594 * 0.2
---            ≈ 0.31 - 0.037 = 0.273 (still too low)
---
--- The void fraction per iteration needs calibration.
--- Observed cosmic void fraction ≈ 12% at z=0 (from DESI void catalogues).
--- This gives:
---   Omega_m ≈ 0.31 - 0.31 * (1 - (20/27)^3) * 0.12
---            ≈ 0.31 - 0.31 * 0.594 * 0.12
---            ≈ 0.31 - 0.022 = 0.288
--- This matches the model's Omega_m = 0.290.
---
--- So 3 observable void iterations at 12% void fraction gives Omega_m = 0.290.
--- The DEEP void iterations (n = 128 from Higgs) are at energies > GeV,
--- where quantum gravity resolves the void structure differently.
--- ═════════════════════════════════════════════════════════════════════════════
-
--- Observable void iterations (from BAO scale / cell size matching)
-def obsVoidIterations : Int := 3
-
--- Void fraction per iteration (from DESI void catalogues: ~12%)
-def voidFraction : Int := 7864  -- Q16.16: 0.12 × 65536
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §3  Higgs-calibrated theorems
--- ═════════════════════════════════════════════════════════════════════════════
-
--- Higgs VEV is positive (fundamental truth)
-theorem higgs_vev_positive : hVEV > 0 := by native_decide
-
--- Planck mass is much larger than Higgs VEV (> 10^16 times)
-theorem planck_above_higgs : planckMass > 1000 := by native_decide
-
--- Void iterations from Higgs/Planck ratio is positive
-theorem void_iterations_positive : voidIterations > 0 := by native_decide
-
--- Observable void iterations is much less than total
-theorem obs_less_than_total : obsVoidIterations < voidIterations := by native_decide
-
--- The deep void iterations (128) suppress vacuum energy by (20/27)^128
--- This factor matches the observed dark energy / Higgs vacuum ratio
--- Not directly provable in Lean without big-integer arithmetic for (20/27)^128
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §4  Executable receipts
--- ═════════════════════════════════════════════════════════════════════════════
-
--- CERN precision
-#eval hLambda         -- Higgs self-coupling from 1137s measurement
-#eval topYukawa       -- Top Yukawa from 576s measurement
-#eval lambdaRunning   -- One-loop running from CERN masses
-#eval hVEV
-#eval voidIterations
-#eval obsVoidIterations
-
-end Semantics.Physics.HiggsCalibration
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/ValveTestSuite.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/ValveTestSuite.lean
index 3c8cee40..a12ab08c 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/ValveTestSuite.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/ValveTestSuite.lean
@@ -1,13 +1,11 @@
 -- ValveTestSuite.lean
 --
--- Multi-valve cosmological test suite for the 16D horn-fiber model.
+-- Cosmological comparison suite for a parameter set (w0, wa, Om, s8).
+-- Computes residuals against DESI DR1, Planck, DES, KiDS.
 --
--- Valves tested:
---   1. S8 tension (matter fluctuation amplitude)
---   2. BAO distance-redshift consistency (DESI DR1)
---   3. Cosmic age vs known bounds
---
--- All model predictions from: w0 = -0.827, wa = -0.55, Om = 0.290, s8 = 0.812
+-- NOTE: these are COMPARISONS, not predictions. w0 is calibrated.
+-- S8 sits between CMB and weak-lensing values. This is a data point,
+-- not a tension resolution claim.
 
 namespace Semantics.Physics.ValveTestSuite