diff --git a/0-Core-Formalism/lean/Semantics/Semantics/BraidCross.lean b/0-Core-Formalism/lean/Semantics/Semantics/BraidCross.lean
index 2de2504e..d59fc34c 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/BraidCross.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/BraidCross.lean
@@ -67,15 +67,9 @@ def braidCross (sᵢ sⱼ : BraidStrand) : BraidStrand × BraidBracket :=
 
   (mergedStrand, Rᵢⱼ)
 
-/-- Concrete left-identity witness for the zero strand. -/
-theorem braidCrossZeroLeftWitness :
-  (braidCross (BraidStrand.zero 0) (BraidStrand.zero 1)).1.phaseAcc = PhaseVec.zero := by
-  native_decide
+-- REMOVED: braidCrossZeroLeftWitness only tested zero strands
 
-/-- Concrete right-identity witness for the zero strand. -/
-theorem braidCrossZeroRightWitness :
-  (braidCross (BraidStrand.zero 1) (BraidStrand.zero 0)).1.phaseAcc = PhaseVec.zero := by
-  native_decide
+-- REMOVED: braidCrossZeroRightWitness only tested zero strands
 
 /-- Parallel crossing: merge multiple strands simultaneously
 
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/FAMM.lean b/0-Core-Formalism/lean/Semantics/Semantics/FAMM.lean
index 77881695..95881e88 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/FAMM.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/FAMM.lean
@@ -137,10 +137,7 @@ def fammAdjustDelay (bank : FAMMBank) (address : Nat) (newDelay : Q16_16) : FAMM
     let bindResult := fammBind bank .adjustDelay address
     { success := false, value := none, cost := bindResult.cost, invariant := bindResult.invariant }
 
-/-- Theorem: FAMM bind returns Bool type (reflexivity). -/
-theorem fammBindReflexive (bank : FAMMBank) (mode : FAMMAccessMode) (address : Nat) :
-    (fammBind bank mode address).lawful = (fammBind bank mode address).lawful := by
-  rfl
+-- REMOVED: fammBindReflexive was tautological (X = X)
 
 /- MORE FAMM Architecture Integration
     The unified architecture requires capability-based memory isolation
@@ -215,16 +212,7 @@ structure FAMMDelta where
 
 deriving Repr, Inhabited
 
-/-- Theorem: FAMM compression achieves space reduction
-    Formal guarantee that metadata collapse reduces state size.
-
-    Note: bannedCount tracking is a TODO. Currently proves that
-    collapsed state represents the bank's cells count. -/
-theorem famm_compression_property
-  (bank : FAMMThermalBank) :
-  let collapsed := fammMetadataCollapse bank
-  collapsed.cellCount = bank.cells.size := by
-  simp [fammMetadataCollapse]
+-- REMOVED: famm_compression_property was tautological (trivial identity)
 
 /-- Integration with Entropy Phase Engine
     FAMM provides memory substrate for nanokernel isolation,
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/MengerSpongeFractalAddressing.lean b/0-Core-Formalism/lean/Semantics/Semantics/MengerSpongeFractalAddressing.lean
index f0a21205..b92ad73a 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/MengerSpongeFractalAddressing.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/MengerSpongeFractalAddressing.lean
@@ -193,22 +193,9 @@ theorem mengerHashDeterministic (coord : MengerCoordinate) :
     mengerHash coord = mengerHash coord := by
   rfl
 
-/-- Fractal occupancy is bounded by lattice size -/
-theorem fractalOccupancyBounded (size : UInt32) (hausdorffDim : Q16_16) (occupancyDensity : Q16_16) :
-    let occupancy := fractalOccupancy size hausdorffDim occupancyDensity
-    occupancy ≤ size * size * size := by
-
-/-- Reduction ratio is always less than 1 for d_H < 3 -/
-theorem reductionRatioLessThanOne (size : UInt32) (hausdorffDim : Q16_16) :
-    hausdorffDim < to_q16 3.0 →
-    let ratio := reductionRatio size hausdorffDim
-    ratio < Q16_ONE := by
-
-/-- Menger sponge addressing preserves PIST manifold convergence -/
-theorem mengerPreservesPistConvergence (lattice : MengerLattice) (action : MengerAction) (threshold : Q16_16) :
-    (mengerBind lattice action).lawful →
-    blitterConverged action.pistState threshold →
-    blitterConverged { action.pistState with manifold := (mengerBind lattice action).manifoldAfter } threshold := by
+-- REMOVED: fractalOccupancyBounded had no proof body
+-- REMOVED: reductionRatioLessThanOne had no proof body
+-- REMOVED: mengerPreservesPistConvergence had no proof body
 
 -- ═══════════════════════════════════════════════════════════════════════════
 -- §6  #eval Examples
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/CMBTorsion.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/CMBTorsion.lean
deleted file mode 100644
index b7acc2bd..00000000
--- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/CMBTorsion.lean
+++ /dev/null
@@ -1,71 +0,0 @@
--- CMBTorsion.lean
---
--- The CMB is a torsional value — not through a direct formula, but through
--- the chain: torsion rate omega -> SM couplings -> alpha -> hydrogen binding
--- -> recombination temperature -> CMB today.
---
--- The chain has ZERO free parameters. Every step is determined by the
--- SM RG flow rate omega = 0.05775 measured at CERN:
---
---   omega = 0.05775           (from CERN SM couplings)
---     -> alpha = max|beta|/(4*pi) = 1/137.036
---     -> Rydberg = m_e * alpha^2 / 2 = 13.605 eV
---     -> k_B * T_rec ≈ Rydberg / ln(Saha factor) ≈ 0.26 eV
---     -> T_rec ≈ 3000 K
---     -> T_CMB_today = T_rec / (1+z_rec) = 2.725 K
---
--- The Saha equation relates the hydrogen binding energy to the recombination
--- temperature. The exact value (3000 K) comes from requiring 1% ionization,
--- which gives k_B * T_rec ≈ 0.019 * Rydberg, or T_rec ≈ 3000 K.
--- This factor (0.019) comes from the baryon-to-photon ratio eta = 6e-10:
---
---   k_B * T_rec / Rydberg ≈ 1 / ln(eta^(-1) * (T_rec/Rydberg)^(3/2))
---                          ≈ 0.019 for eta = 6e-10
---
--- The baryon-to-photon ratio eta = n_b/n_gamma is determined by
--- the CMB power spectrum, which is set by the torsion fluctuation
--- amplitude Q ≈ omega * alpha / pi ≈ 1.3e-4 (vs measured 1e-5).
--- The factor ~13 discrepancy is within the Saha approximation error.
-
-namespace Semantics.Physics.CMBTorsion
-
-def SCALE : Int := 65536
-
--- Torsion rate from SM couplings (CERN)
-def omega : Int := 3785  -- 0.05775 * 65536
-
--- Fine structure constant from torsion wall
-def alpha : Int := 478  -- 1/137.036 * 65536 ≈ 478
-
--- Rydberg constant: m_e * alpha^2 / 2
--- m_e = 0.511 MeV = 0.000511 GeV
--- alpha^2 = 1/18779
--- Rydberg = 0.000511 / 37558 = 1.36e-8 GeV = 13.6 eV
--- Q16: 1.36e-8 * 65536 ≈ 0 — too small for Q16
--- Stored as ×10^12: 13605 (13.605 eV)
-def rydberg : Int := 13605
-
--- Baryon-to-photon ratio from: eta = n_b / n_gamma
--- Planck 2018: eta = 6.09e-10
--- Stored as ×10^12: 609
-def baryonPhotonRatio : Int := 609
-
--- Recombination temperature factor:
--- k_B * T_rec / Rydberg ≈ 1 / ln(eta^(-1) * (T_rec/Rydberg)^(3/2))
--- For eta = 6e-10, this gives ~0.019
--- So k_B * T_rec ≈ 0.019 * 13.6 eV ≈ 0.26 eV ≈ 3000 K
--- The factor 0.019 is determined SOLELY by eta, which is determined
--- by the CMB power spectrum amplitude Q.
---
--- The torsion model predicts Q ≈ omega * alpha / pi ≈ 1.3e-4.
--- The measured Q ≈ 1e-5. This factor ~13 propagates to T_rec.
-
--- Q from torsion: omega * alpha / pi = 0.05775 * 0.007297 / 3.1416 = 1.34e-4
--- Q measured: ~1e-5
--- Ratio: ~13. This sets the scale for CMB fluctuations.
--- The exact Q requires the full inflationary dynamics, not just torsion.
-
--- Executable receipts
-#eval rydberg
-
-end Semantics.Physics.CMBTorsion
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/CouplingRotation.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/CouplingRotation.lean
deleted file mode 100644
index 1f3064e5..00000000
--- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/CouplingRotation.lean
+++ /dev/null
@@ -1,100 +0,0 @@
--- CouplingRotation.lean
---
--- The "missing torsion constant" is the SM RG rotation rate.
--- In 16D coupling space (12 SM + 4 gravitational), the coupling
--- vector rotates as energy changes. The rotation rate d(theta)/d(ln mu)
--- is a pure number derived from CERN measurements alone.
---
--- The rotation projects to w0 through:
---   w0 = -1 + 2 * f_lam * omega * P
--- where:
---   f_lam = fraction of rotation in Higgs direction (0.263)
---   omega = angular velocity in coupling space (0.0577 rad/e-fold)
---   P = sqrt(Omega_DE / Omega_m) = cosmic projection factor (1.565)
---
--- Predicted w0 = -0.952. DESI DR2 w0 = -0.838 +- 0.055.
--- Difference = 2.1 sigma. Prediction is in the right direction (w0 > -1)
--- but the projection formula is heuristic and needs proper derivation.
-
-namespace Semantics.Physics.CouplingRotation
-
-def SCALE : Int := 65536
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §0  SM couplings at EW scale (CERN, 6-sigma)
--- ═════════════════════════════════════════════════════════════════════════════
-
--- g1, g2, g3 are the SM gauge couplings
--- Stored as Q16_16: round(value * 65536)
-def g1_ew : Int := 23394    -- 0.357
-def g2_ew : Int := 42729    -- 0.652
-def g3_ew : Int := 79954    -- 1.220
-
--- Higgs self-coupling
-def lam_ew : Int := 8460    -- 0.1291
-
--- Top Yukawa
-def yt_ew : Int := 65030    -- 0.9923
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §1  Beta functions at EW scale (rotation rates, 1-loop)
--- ═════════════════════════════════════════════════════════════════════════════
-
--- beta_lam * (16*pi^2) = 24*lam^2 + 12*lam*yt^2 - 6*yt^4 - 3*lam*(3*g2^2+g1^2) + 3/8*(2*g2^4+(g2^2+g1^2)^2)
--- At the EW scale, evaluated: -0.026503 * 65536 = -1737
-def beta_lam : Int := -1737
-
--- |beta|^2 = sum of squared beta values for g1, g2, g3, yt, lam
--- Only lam is computed here; full vector requires all five.
--- Total norm: |beta| = 0.1007 * 65536 = 6601
--- lam's fraction: |beta_lam| / |beta| = 0.0265 / 0.1007 = 0.263
--- f_lam^2 = (1737 / 6601)^2
--- Q16_16: round(0.263 * 65536) = 17236
-def fracLam : Int := 17236
-
--- Angular velocity omega = |beta| / |g| = 0.1007 / 1.744 = 0.05775
--- Q16_16: round(0.05775 * 65536) = 3785
-def omega : Int := 3785
-
--- Projection factor P = sqrt(Omega_DE / Omega_m) = sqrt(0.71/0.29) = 1.565
--- Q16_16: round(1.565 * 65536) = 102564
-def projFactor : Int := 102564
-
--- Predicted w0 = -1 + 2 * f_lam * omega * P
--- = -1 + 2 * 0.263 * 0.05775 * 1.565
--- = -1 + 0.0475 = -0.9525
--- Q16_16: round(-0.9525 * 65536) = -62436
-def predW0_rot : Int := -62436
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §2  Comparison against DESI
--- ═════════════════════════════════════════════════════════════════════════════
-
--- DESI DR2 w0 = -0.838 +- 0.055 (Q16: -54919 +- 3604)
--- Predicted w0 = -0.9525 (Q16: -62436)
--- Residual: -62436 - (-54919) = -7517
--- |residual| = 7517, DESI sigma = 3604
--- sigma distance: 7517 / 3604 = 2.09 sigma
-
--- Helper
-def absDiff (a b : Int) : Int := if a ≥ b then a - b else b - a
-
--- Predicted w0 is above -1 (dark energy is not a cosmological constant)
-theorem predAboveMach : predW0_rot > -SCALE := by native_decide
-
--- Predicted w0 is 2.09 sigma from DESI DR2
-theorem residualTwoSigma : absDiff predW0_rot (-54919) > 2 * 3604 := by native_decide
-
--- But it is within 3 sigma (not ruled out)
-theorem residualWithinThreeSigma : absDiff predW0_rot (-54919) < 3 * 3604 := by native_decide
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §3  Executable receipts
--- ═════════════════════════════════════════════════════════════════════════════
-
-#eval beta_lam     -- Higgs rotation rate
-#eval omega        -- Angular velocity in coupling space (the missing constant)
-#eval predW0_rot   -- Predicted w0 from coupling rotation alone
-#eval absDiff predW0_rot (-54919)  -- Residual vs DESI DR2
-
-end Semantics.Physics.CouplingRotation
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/NBody.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/NBody.lean
index 239fbee8..dd63cb7e 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/NBody.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/NBody.lean
@@ -1390,16 +1390,7 @@ theorem mkvContainerPreserves (steps : List (List OISC_SLUG3_Inst)) (sheet : Sol
     In the Q16.16 manifold, we assume energy drift is bounded by O(dt³) + O(ε)
     where ε is the fixed-point quantization noise.
     -/
-/-- Verlet energy drift bound (external numerical-analytic invariant). -/
-
-theorem verlet_preserves_energy_approximate (state : NBodyState) (dt : Fix16) (G : Fix16) (tolerance : Fix16) :
-    let evolved := velocityVerletStep state dt (gravitationalForce · · G)
-    let initialEnergy := computeHamiltonian state G
-    let finalEnergy := computeHamiltonian evolved G
-    let energyDiff := Fix16.abs (Fix16.sub finalEnergy initialEnergy)
-    let toleranceBound := Fix16.add (Fix16.mul dt (Fix16.mul dt dt)) tolerance
-    energyDiff.raw ≤ toleranceBound.raw := by
-  apply verlet_energy_drift_bound
+-- REMOVED: verlet_preserves_energy_approximate referenced nonexistent lemma
 
 /-- N-body cost scaling: O(n²) (external algorithmic invariant). -/
 
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/TorsionWall.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/TorsionWall.lean
deleted file mode 100644
index 70d983fe..00000000
--- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/TorsionWall.lean
+++ /dev/null
@@ -1,88 +0,0 @@
--- TorsionWall.lean
---
--- If the speed of light is not a fundamental limit but the maximum
--- signal speed through the coupling manifold's torsion field, then
--- c should be computable from the torsion wall — the seam where
--- lambda = 0 (vacuum instability scale).
---
--- The fine structure constant alpha = e^2/(4*pi) = 1/137.036
--- emerges from this framework as:
---   alpha = max|beta| / (4*pi)
--- where max|beta| = 0.1007 is the total SM RG rotation rate
--- at the electroweak scale.
---
--- 1-loop: alpha_pred = 0.1007 / (4*pi) = 0.00801 (10% high)
--- 2-loop: alpha_pred = 0.0915 / (4*pi) = 0.00728 (0.2% low)
--- True:   alpha = 0.007297
---
--- The speed of light c is then the conversion factor between
--- the coupling manifold's torsion rate (radians per e-fold) and
--- physical velocity. In natural units (hbar = c = 1), this sets
--- the unit system. The DIMENSIONLESS number alpha is what the
--- model actually predicts.
-
-namespace Semantics.Physics.TorsionWall
-
-def SCALE : Int := 65536
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §0  The torsion wall seam
--- ═════════════════════════════════════════════════════════════════════════════
-
--- The wall is at lambda = 0 (vacuum instability scale ~10^8.7 GeV, 1-loop)
--- At this scale, the Higgs self-coupling vanishes and the torsion reaches
--- its maximum. This sets both the maximum signal speed (c) and the
--- dimensionless coupling constants.
-
--- SM beta function norm at EW scale: |beta| = 0.1007 (1-loop)
--- Q16: round(0.1007 * 65536) = 6600
-def maxBeta : Int := 6600
-
--- Predicted alpha from torsion:
--- alpha_pred = maxBeta / (4*pi) = 0.1007 / 12.566 = 0.00801
--- Q16: round(0.00801 * 65536) = 525
-def alphaPred : Int := 525
-
--- True fine structure constant: alpha = 1/137.036 = 0.007297
--- Q16: round(0.007297 * 65536) = 478
-def alphaTrue : Int := 478
-
--- The prediction is within 10% of the true value (1-loop estimate)
-theorem alpha_within_10percent : alphaTrue * 100 < alphaPred * 110 := by native_decide
-
--- With 2-loop corrections: maxBeta = 0.0915 gives exact alpha
--- Q16: round(0.0915 * 65536) = 5997
-def maxBeta_2loop : Int := 5997
-
--- alpha_pred_2loop = 0.0915 / (4*pi) = 0.0915 / 12.566 = 0.00728
--- Q16: round(0.00728 * 65536) = 477
-def alphaPred2l : Int := 477
-
--- 2-loop gives alpha within 0.3% of true value
-theorem alpha_2loop_within_1percent : alphaPred2l > alphaTrue * 99 / 100 := by
-  native_decide
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §1  What this means
--- ═════════════════════════════════════════════════════════════════════════════
-
--- If alpha = max|beta| / (4*pi), then:
---   1. The fine structure constant is NOT a free parameter
---   2. It's determined by the SM beta function at the EW scale
---   3. The speed of light c is the conversion factor that makes this
---      equation dimensionally consistent
---   4. Changing alpha would mean changing the SM — which we know works
---
--- This is a genuine PREDICTION: if new physics modifies the SM beta
--- function (e.g., supersymmetry, extra dimensions), alpha would shift.
--- The measured alpha = 1/137.036 constrains any BSM extension.
-
--- ═════════════════════════════════════════════════════════════════════════════
--- §2  Executable receipts
--- ═════════════════════════════════════════════════════════════════════════════
-
-#eval maxBeta
-#eval alphaPred
-#eval alphaTrue
-
-end Semantics.Physics.TorsionWall