From bf22d432b47a3a6eca79648ae96841ea6289af40 Mon Sep 17 00:00:00 2001
From: Brandon Schneider <ceo@sovereign-stack.local>
Date: Thu, 28 May 2026 17:19:12 -0500
Subject: [PATCH] fix: eliminate 2 sorries (BraidBitwiseODE + MeshRouting)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

BraidBitwiseODE.lean:
- bitwise_ode_correct: Q16_16.toInt_eq_zero_iff + subst + native_decide
- No more sorry

MeshRouting.lean:
- goxelFieldEnergyConservation: added upper bound hypothesis
- Proof: ofRawInt_val_eq_q16Clamp + q16Clamp_id_of_inRange + omega
- No more sorry

Remaining: AdjugateMatrix det_self_inverse (hard — 8×8 adjugate identity)
---
 .../Semantics/Semantics/BraidBitwiseODE.lean  |  9 ++++---
 .../lean/Semantics/Semantics/MeshRouting.lean | 27 +++++++++----------
 2 files changed, 19 insertions(+), 17 deletions(-)

diff --git a/0-Core-Formalism/lean/Semantics/Semantics/BraidBitwiseODE.lean b/0-Core-Formalism/lean/Semantics/Semantics/BraidBitwiseODE.lean
index 1d46f22b..40f13c89 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/BraidBitwiseODE.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/BraidBitwiseODE.lean
@@ -140,9 +140,12 @@ theorem cross_step_preserves_slot (a b : BraidStrand) :
     32 steps (the bit width of Q16.16). -/
 theorem bitwise_ode_correct (state : Q16_16) (h : state.toInt = 0) :
     bitwiseODEIntegrate state state = state := by
-  unfold bitwiseODEIntegrate
-  simp [h, Q16_16.ofBits, Q16_16.toBits, Q16_16.ofNat]
-  sorry  -- TODO(lean-port): requires Q16.16 bit-level identity proof
+  -- state.toInt = 0 means state is the zero Q16.16 value
+  rw [Q16_16.toInt_eq_zero_iff] at h
+  subst h
+  -- Goal: bitwiseODEIntegrate zero zero = zero
+  -- All intermediate values (toBits 0, ofNat 0, ofBits 0, XOR 0 0) reduce to zero
+  native_decide
 
 
 -- ════════════════════════════════════════════════════════════
diff --git a/0-Core-Formalism/lean/Semantics/Semantics/MeshRouting.lean b/0-Core-Formalism/lean/Semantics/Semantics/MeshRouting.lean
index a14d1ec2..875d64fe 100644
--- a/0-Core-Formalism/lean/Semantics/Semantics/MeshRouting.lean
+++ b/0-Core-Formalism/lean/Semantics/Semantics/MeshRouting.lean
@@ -331,23 +331,22 @@ def projectGoxelFieldToFrame (field : GoxelFieldFrame) (spec : VCNFrameSpec) : A
 
 /-- 16D field energy conservation theorem during VCN transform.
     The hardware transform should preserve high-dimensional field energy.
-    TODO(lean-port): This theorem requires additional hypotheses to be provable.
-    Needed premises:
-    - `fieldEnergyBound : field.fieldEnergy ≤ encoded.compressionRatio + ⟨32768, ...⟩`
-      (or equivalently, the Q16_16 energy difference is bounded by 0.5 in fixed-point)
-    - Or: `field.fieldEnergy ≤ ⟨32768, ...⟩` and `encoded.compressionRatio ≥ 0`
-    Without these, the subtraction `fieldEnergy - compressionRatio` can saturate
-    to q16MaxRaw, violating the bound. -/
+    When field energy exceeds compression ratio (so subtraction doesn't
+    underflow) and the difference is bounded by 0x8000 (0.5 in Q16_16),
+    the saturated subtraction result stays within the bound. -/
 theorem goxelFieldEnergyConservation (field : GoxelFieldFrame) (encoded : VCNComputationReceipt) :
     field.fieldEnergy.val ≥ encoded.compressionRatio.val →
+    field.fieldEnergy.val ≤ encoded.compressionRatio.val + 32768 →
     (field.fieldEnergy - encoded.compressionRatio).val ≤ 32768 := by
-  -- TODO(lean-port): Requires Q16_16.sub_val_of_ge lemma (subtraction preserves
-  -- non-negative values without saturation). The bound 32768 = 0x8000 is half the
-  -- Q16_16 scale, representing 0.5 in fixed-point. Proof sketch:
-  -- 1. Show (a - b).val = a.val - b.val when a.val ≥ b.val (no saturation)
-  -- 2. Show result ≤ 32768 from field energy constraints
-  intro _h
-  sorry
+  intro h_ge h_le
+  -- Unfold subtraction to ofRawInt and then to q16Clamp
+  change (Q16_16.ofRawInt (field.fieldEnergy.val - encoded.compressionRatio.val)).val ≤ 32768
+  rw [FixedPoint.Q16_16.ofRawInt_val_eq_q16Clamp]
+  -- The raw difference is in-range, so q16Clamp is the identity
+  rw [FixedPoint.q16Clamp_id_of_inRange]
+  · omega
+  · dsimp [FixedPoint.q16MinRaw]; omega
+  · dsimp [FixedPoint.q16MaxRaw]; omega
 
 /-- 16D topology preservation theorem.
     The compression hierarchy should preserve topological relationships in 16D space.