diff --git a/0-Core-Formalism/lean/Semantics/Semantics.lean b/0-Core-Formalism/lean/Semantics/Semantics.lean
index ccab7684..5eca59e1 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics.lean
@@ -55,7 +55,8 @@ import Semantics.VecState
 import Semantics.PrimeLut
 import PIST
 import PistBridge
-import PistSimulation
+-- PistSimulation imported via Semantics.TreeDIATKruskal; bare import removed
+-- to avoid double-import collision with Semantics.PistSimulation in the glob build.
 
 import Semantics.Tape
 import Semantics.DynamicCanal
@@ -162,41 +163,43 @@ import Semantics.CrossDomainOneOverN
 import Semantics.BaselineComparison
 import Semantics.ParameterSensitivity
 import Semantics.DimensionalConsistency
-import Semantics.AtomicTimescaleProbe
-import Semantics.CosmologicalTimescaleProbe
-import Semantics.SpacetimeStretchingProbe
-import Semantics.BigBangTemporalAnchor
-import Semantics.EinsteinFrameDragProbe
-import Semantics.GeminiThreePathsProbe
-import Semantics.ProtonDecayAnchor
-import Semantics.ShortestObservableTime
-import Semantics.LandauerShannonProbe
-import Semantics.ImaginarySemanticTime
-import Semantics.AdiabaticInvariantProbe
-import Semantics.CalculusIntegralProbe
-import Semantics.AdiabaticCalculusProbe
-import Semantics.PadicCalculusProbe
-import Semantics.GapSpaceProbe
-import Semantics.ArakelovAdeleProbe
-import Semantics.AdelicStringProbe
-import Semantics.MengerUniversalProbe
-import Semantics.Genus1MengerEmbedding
-import Semantics.GeneticFieldEquation
-import Semantics.CivilizationalPulseProbe
-import Semantics.SingularityPulseProbe
-import Semantics.MediaTransferProbe
-import Semantics.LanguageTransferProbe
-import Semantics.LanguageZoologyProbe
-import Semantics.EcologicalPeriodDataProbe
-import Semantics.ThermodynamicLanguageProbe
-import Semantics.GeneticThermodynamicLimitProbe
-import Semantics.ExpandedGeneticAlphabetProbe
-import Semantics.GeneticSignalTransformProbe
-import Semantics.SemanticBasinOverflowProbe
-import Semantics.GeneticErrorMinimizationProbe
-import Semantics.InformationBottleneckLanguageProbe
-import Semantics.CrossModalGeneticLanguageProbe
-import Semantics.LandauerGeneticClockProbe
+-- QUARANTINE: Probe stubs (files not yet written). Removed from root to keep
+-- lake build non-crashing. TODO(lean-port): implement and re-enable.
+-- import Semantics.AtomicTimescaleProbe
+-- import Semantics.CosmologicalTimescaleProbe
+-- import Semantics.SpacetimeStretchingProbe
+-- import Semantics.BigBangTemporalAnchor
+-- import Semantics.EinsteinFrameDragProbe
+-- import Semantics.GeminiThreePathsProbe
+-- import Semantics.ProtonDecayAnchor
+-- import Semantics.ShortestObservableTime
+-- import Semantics.LandauerShannonProbe
+-- import Semantics.ImaginarySemanticTime
+-- import Semantics.AdiabaticInvariantProbe
+-- import Semantics.CalculusIntegralProbe
+-- import Semantics.AdiabaticCalculusProbe
+-- import Semantics.PadicCalculusProbe
+-- import Semantics.GapSpaceProbe
+-- import Semantics.ArakelovAdeleProbe
+-- import Semantics.AdelicStringProbe
+-- import Semantics.MengerUniversalProbe
+-- import Semantics.Genus1MengerEmbedding
+-- import Semantics.GeneticFieldEquation
+-- import Semantics.CivilizationalPulseProbe
+-- import Semantics.SingularityPulseProbe
+-- import Semantics.MediaTransferProbe
+-- import Semantics.LanguageTransferProbe
+-- import Semantics.LanguageZoologyProbe
+-- import Semantics.EcologicalPeriodDataProbe
+-- import Semantics.ThermodynamicLanguageProbe
+-- import Semantics.GeneticThermodynamicLimitProbe
+-- import Semantics.ExpandedGeneticAlphabetProbe
+-- import Semantics.GeneticSignalTransformProbe
+-- import Semantics.SemanticBasinOverflowProbe
+-- import Semantics.GeneticErrorMinimizationProbe
+-- import Semantics.InformationBottleneckLanguageProbe
+-- import Semantics.CrossModalGeneticLanguageProbe
+-- import Semantics.LandauerGeneticClockProbe
 import Semantics.FAMM
 import Semantics.HCMMR.Core
 import Semantics.HCMMR.Kernels.FAMMScarMemory
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/PistSimulation.lean b/0-Core-Formalism/lean/Semantics/Semantics/PistSimulation.lean
index fa78e18b..0cf18757 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/PistSimulation.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/PistSimulation.lean
@@ -626,8 +626,8 @@ def spectralWindowToRegimeChaos (window : List Q16_16) : MagneticRegime :=
 -- ════════════════════════════════════════════════════════════
 
 def fixtureSpectralWindow : List Q16_16 := [
-  ⟨655360⟩, ⟨1310720⟩, ⟨6553600⟩, ⟨2621440⟩,
-  ⟨1310720⟩, ⟨655360⟩, ⟨327680⟩, ⟨327680⟩
+  Q16_16.ofRawInt 655360, Q16_16.ofRawInt 1310720, Q16_16.ofRawInt 6553600, Q16_16.ofRawInt 2621440,
+  Q16_16.ofRawInt 1310720, Q16_16.ofRawInt 655360,  Q16_16.ofRawInt 327680,  Q16_16.ofRawInt 327680
 ]
 
 #eval! quadraticFitCoeffs fixtureSpectralWindow
@@ -1266,17 +1266,17 @@ def burgersPhiDissipationStep (N : Nat) (u : Array Q16_16) (_ν _dx _dt : Q16_16
     theorem for the viscous Burgers equation.
     TODO(lean-port): complete the proof; currently verified by
     computational witness on all test fixtures. -/
-theorem goldenContractionEnergyDecrease {N : Nat} (u : Array Q16_16)
-    (hN : N ≥ 3)
-    (h_size : u.size = N)
-    (ν dx dt : Q16_16) :
-    Q16_16.le
-      (arrayKineticEnergy (burgersPhiDissipationStep N u ν dx dt))
-      (arrayKineticEnergy u) := by
-  -- Computational witness: the theorem holds for all test fixtures.
-  -- General proof requires Jensen's inequality for discrete convex
-  -- combinations and a monotonicity argument on the squared sum.
-  sorry
+-- TODO(lean-port): goldenContractionEnergyDecrease forward-references
+-- arrayKineticEnergy (defined below at §9f). Move this theorem after
+-- arrayKineticEnergy's definition or introduce a mutual block.
+-- theorem goldenContractionEnergyDecrease {N : Nat} (u : Array Q16_16)
+--     (hN : N ≥ 3)
+--     (h_size : u.size = N)
+--     (ν dx dt : Q16_16) :
+--     Q16_16.le
+--       (arrayKineticEnergy (burgersPhiDissipationStep N u ν dx dt))
+--       (arrayKineticEnergy u) := by
+--   sorry
 
 -- ── 9e. Verification witnesses ───────────────────────────
 
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/TreeDIATKruskal.lean b/0-Core-Formalism/lean/Semantics/Semantics/TreeDIATKruskal.lean
index 186f9a2c..c1f9ffb1 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/TreeDIATKruskal.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/TreeDIATKruskal.lean
@@ -53,17 +53,13 @@ def treeLabelCountExact (t : TreeNode) : Nat := treeMaxLabelExact t + 1
 theorem treeNodeCountExact_pos (t : TreeNode) : 0 < treeNodeCountExact t := by
   induction t with
   | leaf label => simp [treeNodeCountExact]
-  | node label l r ihL ihR =>
-      simp [treeNodeCountExact]
-      omega
+  | node label l r ihL ihR => simp [treeNodeCountExact, ihL, ihR]
 
 /-- Leaf count is always positive. -/
 theorem treeLeafCountExact_pos (t : TreeNode) : 0 < treeLeafCountExact t := by
   induction t with
   | leaf label => simp [treeLeafCountExact]
-  | node label l r ihL ihR =>
-      simp [treeLeafCountExact]
-      omega
+  | node label l r ihL ihR => simp [treeLeafCountExact, ihL, ihR]
 
 /-- A tree cannot have more leaves than nodes. -/
 theorem treeLeafCountExact_le_nodeCountExact (t : TreeNode) :