From f75384082e9a2129d58d0463996920d4c26e60c4 Mon Sep 17 00:00:00 2001 From: allaun Date: Tue, 16 Jun 2026 21:43:38 -0500 Subject: [PATCH] feat(lean): add applyViscosity_energy_le and AVMR ODE scaffolding MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Item 1 (BurgersPDE): Added Q16_16.mul_sq_le_sq lemma and applyViscosity_energy_le general theorem — the universal energy dissipation result that subsumes all 5 point-evaluation proofs. Item 7 (AVMRTheorems): Added Float-free vectorFieldℝ, Lipschitz proof, ε=0 base_dynamics, and ode_existence (with TODO) for the missingLinkODE continuum limit. Also fixed broken proofs: tipCoordinateMassResonance corrected to mass ≤ (k+1)² only; massResonanceMax → massMidpoint (correct: mass = k·(k+1)); replaced Nat.sqrt_eq_iff_sq_le (removed in Mathlib 4.30) with inline le_antisymm + Nat.le_sqrt proofs; fixed import paths; fixed omega/nlinarith failures in AVMRCore. Build: 3571 jobs, 0 errors (Semantics workspace), 8315 jobs, 1 sorry (ode_existence TODO) --- .../Semantics/AVMRClassification.lean | 2 +- .../lean/Semantics/Semantics/AVMRCore.lean | 20 +- .../Semantics/Semantics/AVMRTheorems.lean | 629 ++++++++---------- .../lean/Semantics/Semantics/BurgersPDE.lean | 113 +++- 4 files changed, 408 insertions(+), 356 deletions(-) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMRClassification.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMRClassification.lean index b3c28747..dca76b31 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/AVMRClassification.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/AVMRClassification.lean @@ -1,5 +1,5 @@ import Mathlib -import AVMRCore +import Semantics.AVMRCore /-! # AVMR Classification Event classification to DNA bases. diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMRCore.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMRCore.lean index 5587ed2d..17af2077 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/AVMRCore.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/AVMRCore.lean @@ -31,16 +31,22 @@ lemma squareShellIdentity (n : Nat) : let s := shellState n s.n = s.k * s.k + s.a := by dsimp [shellState] - let k := Nat.sqrt n - have hk : k*k ≤ n := Nat.sqrt_le n - omega + have hk : (Nat.sqrt n) * (Nat.sqrt n) ≤ n := Nat.sqrt_le n + calc + n = (n - (Nat.sqrt n)*(Nat.sqrt n)) + (Nat.sqrt n)*(Nat.sqrt n) := by + rw [Nat.sub_add_cancel hk] + _ = (Nat.sqrt n)*(Nat.sqrt n) + (n - (Nat.sqrt n)*(Nat.sqrt n)) := by rw [Nat.add_comm] /-- Verify: (k+1)² = n + b (complementary identity) -/ lemma complementaryIdentity (n : Nat) : let s := shellState n (s.k + 1) * (s.k + 1) = s.n + s.b := by dsimp [shellState] - let k := Nat.sqrt n - have hk1 : n < (k+1)*(k+1) := Nat.lt_succ_sqrt n - have hk2 : k*k ≤ n := Nat.sqrt_le n - omega + have hle : n ≤ (Nat.sqrt n + 1) * (Nat.sqrt n + 1) := by + have hlt : n < (Nat.sqrt n + 1) * (Nat.sqrt n + 1) := Nat.lt_succ_sqrt n + omega + calc + (Nat.sqrt n + 1) * (Nat.sqrt n + 1) + = ((Nat.sqrt n + 1) * (Nat.sqrt n + 1) - n) + n := by + rw [Nat.sub_add_cancel hle] + _ = n + ((Nat.sqrt n + 1) * (Nat.sqrt n + 1) - n) := by rw [Nat.add_comm] diff --git a/0-Core-Formalism/lean/Semantics/Semantics/AVMRTheorems.lean b/0-Core-Formalism/lean/Semantics/Semantics/AVMRTheorems.lean index e46e192c..97b3513c 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/AVMRTheorems.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/AVMRTheorems.lean @@ -1,6 +1,6 @@ import Mathlib -import AVMRCore -import AVMRClassification +import Semantics.AVMRCore +import Semantics.AVMRClassification /-! # AVMR Theorems The three main AVMR theorems: Tip Coordinate Mass Resonance, 45° Line Factor Revelation, and Missing Link ODE. @@ -9,380 +9,315 @@ Split from AVMRProofs.lean per swarm suggestion (USER AUTHORIZED). /-- The mass at a shell position equals the product a·b. This theorem proves that the mass (which maps to GC content - times H-bond energy) reaches its MAXIMUM at the shell's - midpoint — the "resonance point" where a ≈ b. - - Biochemical interpretation: Maximum stability occurs when - GC/AT ratio balances H-bond energy distribution. --/ + times H-bond energy) is bounded by (k+1)². -/ theorem tipCoordinateMassResonance (n : Nat) (hn : n > 0) : - let s := shellState n - let mass := s.a * s.b - -- Mass is maximized when a = b (the midpoint of the shell) - -- At the midpoint: a = b = k, so mass = k² - -- This is the point of maximum "resonance" - s.a ≤ s.k + 1 ∧ s.b ≤ s.k + 1 ∧ - -- The mass product a·b is bounded by k² - mass ≤ (s.k + 1) * (s.k + 1) := by + ((shellState n).a * (shellState n).b) ≤ ((shellState n).k + 1) * ((shellState n).k + 1) := by dsimp [shellState] let k := Nat.sqrt n have hk1 : k*k ≤ n := Nat.sqrt_le n have hk2 : n < (k+1)*(k+1) := Nat.lt_succ_sqrt n - have ha1 : n - k*k ≤ 2*k := by - have : n < k*k + 2*k + 1 := by - simp [Nat.pow_succ, Nat.mul_add] at hk2 ⊢ - linarith - have : n - k*k < 2*k + 1 := by - apply Nat.sub_lt_of_lt_add - · exact hk1 - · linarith - omega - have hb1 : (k+1)*(k+1) - n ≤ 2*k + 1 := by - have h1 : (k+1)*(k+1) ≤ n + 2*k + 1 := by linarith - have : (k+1)*(k+1) - n ≤ 2*k + 1 := by - rw [Nat.sub_le_iff_le_add] - · linarith - · exact hk1 - exact this - constructor - · -- Prove a ≤ k + 1 - have : n - k*k ≤ k + 1 := by - have : n - k*k ≤ 2*k := ha1 - have : 2*k ≤ k + 1 + k := by omega - -- Actually need tighter bound - have hmid : n - k*k ≤ k + k := ha1 - have : n - k*k ≤ k + 1 := by - by_cases hk0 : k = 0 - · simp [hk0] at * - have : n < 1 := by nlinarith - interval_cases n <;> omega - · have : k ≥ 1 := by omega - -- For k ≥ 1, the maximum a occurs near the midpoint - have ha_max : n - k*k ≤ 2*k := ha1 - have : n - k*k ≤ k + 1 := by - -- The midpoint a = k gives mass = k·k = k² - -- Maximum mass in terms of k is at a = b = k - nlinarith [Nat.sqrt_le n, Nat.lt_succ_sqrt n] - assumption - assumption - assumption - constructor - · -- Prove b ≤ k + 1 - have : (k+1)*(k+1) - n ≤ k + 1 := by - have h1 : n ≥ k*k := hk1 - have h2 : n < (k+1)*(k+1) := hk2 - -- b = (k+1)² - n, and since n ≥ k², b ≤ 2k+1 - -- But we need b ≤ k+1 for the bound - have hb : (k+1)*(k+1) - n ≤ k + 1 := by - rw [Nat.sub_le_iff_le_add] - · nlinarith - · exact hk1 - assumption - assumption - · -- Prove mass ≤ (k+1)² - have hmass : (n - k*k) * ((k+1)*(k+1) - n) ≤ (k+1)*(k+1) := by - have ha_le : n - k*k ≤ 2*k + 1 := by - have : n - k*k < 2*k + 1 := by - apply Nat.sub_lt_of_lt_add - · exact hk1 - · nlinarith + have hk1' : n ≥ k*k := hk1 + have hk2' : n ≤ (k+1)*(k+1) := by omega + -- Cast the ℕ subtraction to ℤ (requires proof that subtraction is proper) + have ha_cast : ((n - k*k : ℕ) : ℤ) = (n : ℤ) - (k : ℤ)*(k : ℤ) := by + calc + ((n - k*k : ℕ) : ℤ) = ((n : ℕ) : ℤ) - ((k*k : ℕ) : ℤ) := by rw [Nat.cast_sub hk1] + _ = (n : ℤ) - (k : ℤ)*(k : ℤ) := by simp + have hb_cast : (((k+1)*(k+1) - n : ℕ) : ℤ) = ((k+1 : ℤ)*(k+1 : ℤ)) - (n : ℤ) := by + calc + (((k+1)*(k+1) - n : ℕ) : ℤ) = (((k+1)*(k+1) : ℕ) : ℤ) - ((n : ℕ) : ℤ) := by rw [Nat.cast_sub hk2'] + _ = ((k+1 : ℤ)*(k+1 : ℤ)) - (n : ℤ) := by simp + -- ℤ proof of the inequality + have h_total_int : ((n - k*k : ℕ) : ℤ) * (((k+1)*(k+1) - n : ℕ) : ℤ) ≤ (((k+1)*(k+1) : ℕ) : ℤ) := by + rw [ha_cast, hb_cast] + have hsum_int : ((n : ℤ) - (k : ℤ)*(k : ℤ)) + (((k : ℤ)+1)*((k : ℤ)+1) - (n : ℤ)) = (2*(k : ℤ) + 1) := by ring + have h_sq_nonneg : (((n : ℤ) - (k : ℤ)*(k : ℤ)) - (((k : ℤ)+1)*((k : ℤ)+1) - (n : ℤ)))^2 ≥ 0 := + pow_two_nonneg _ + have hk_nonneg : (0 : ℤ) ≤ (k : ℤ) := by exact_mod_cast Nat.zero_le _ + have h_4ab_bound : 4 * ((n : ℤ) - (k : ℤ)*(k : ℤ)) * (((k : ℤ)+1)*((k : ℤ)+1) - (n : ℤ)) ≤ + (2*(k : ℤ)+1)^2 := by + set a := (n : ℤ) - (k : ℤ)*(k : ℤ) with ha + set b := ((k : ℤ)+1)*((k : ℤ)+1) - (n : ℤ) with hb + have hsum_ab : a + b = 2*(k : ℤ)+1 := by dsimp [a, b]; ring + have h_sq_nonneg' : (a - b)^2 ≥ 0 := pow_two_nonneg _ + calc + 4*a*b ≤ (a+b)^2 := by nlinarith + _ = (2*(k : ℤ)+1)^2 := by rw [hsum_ab] + by_contra! hgt + have h_lower_four : 4 * ((n : ℤ) - (k : ℤ)*(k : ℤ)) * (((k : ℤ)+1)*((k : ℤ)+1) - (n : ℤ)) ≥ + 4*((k : ℤ)+1)*((k : ℤ)+1) + 4 := by + have hgt_plus : ((n : ℤ) - (k : ℤ)*(k : ℤ)) * (((k : ℤ)+1)*((k : ℤ)+1) - (n : ℤ)) > + ((k+1 : ℤ)*((k+1 : ℤ))) := hgt + have hgt_val : ((n : ℤ) - (k : ℤ)*(k : ℤ)) * (((k : ℤ)+1)*((k : ℤ)+1) - (n : ℤ)) ≥ + ((k+1 : ℤ)*((k+1 : ℤ))) + 1 := by omega + nlinarith + have h_gt : 4*((k : ℤ)+1)*((k : ℤ)+1) + 4 > (2*(k : ℤ)+1)^2 := by + have h_expand : 4*((k : ℤ)+1)*((k : ℤ)+1) + 4 - (2*(k : ℤ)+1)^2 = 4*(k : ℤ) + 7 := by ring + have h_pos : 0 < 4*(k : ℤ) + 7 := by + have hk_nonneg' : (0 : ℤ) ≤ (k : ℤ) := by exact_mod_cast (show 0 ≤ k from Nat.zero_le _) omega - have hb_le : (k+1)*(k+1) - n ≤ 2*k + 1 := hb1 - -- Product of two numbers with fixed sum is maximized at equality - -- a + b = (n-k²) + ((k+1)²-n) = 2k+1, so max product is at a=b=k+0.5 - -- For integers: max at a=k, b=k+1 or a=k+1, b=k - have hprod : (n - k*k) * ((k+1)*(k+1) - n) ≤ k*(k+1) := by - -- Use the fact that for fixed sum S = 2k+1, product ≤ floor(S/2)·ceil(S/2) = k·(k+1) - have hsum : (n - k*k) + ((k+1)*(k+1) - n) = 2*k + 1 := by - rw [Nat.add_sub_assoc] - · simp [Nat.pow_succ] - ring_nf - omega - · exact hk1 - nlinarith [Nat.mul_le_mul (show k ≤ k by rfl) (show k ≤ k+1 by omega)] - have hk_k1 : k*(k+1) ≤ (k+1)*(k+1) := by - nlinarith - nlinarith - assumption + omega + have h_upper_four : 4 * ((n : ℤ) - (k : ℤ)*(k : ℤ)) * (((k : ℤ)+1)*((k : ℤ)+1) - (n : ℤ)) ≤ + (2*(k : ℤ)+1)^2 := h_4ab_bound + have h_gt_val : 4*((k : ℤ)+1)*((k : ℤ)+1) + 4 > (2*(k : ℤ)+1)^2 := h_gt + -- Chain: (2k+1)² ≥ X (h_upper_four) ≥ 4(k+1)² + 4 (h_lower_four) > (2k+1)² (h_gt_val) + -- So (2k+1)² > (2k+1)², contradiction. + have h_chain : 4*((k : ℤ)+1)*((k : ℤ)+1) + 4 ≤ (2*(k : ℤ)+1)^2 := + le_trans h_lower_four h_upper_four + have h_gt_rev : (2*(k : ℤ)+1)^2 < 4*((k : ℤ)+1)*((k : ℤ)+1) + 4 := h_gt_val + linarith + exact_mod_cast h_total_int -/-- Corollary: At the exact midpoint a = b = k, mass = k². - This is the maximum possible mass for shell k. -/ -corollary massResonanceMax (k : Nat) : - let n := k*k + k -- midpoint position - let s := shellState n - s.a * s.b = k * k := by - dsimp [shellState] - have : Nat.sqrt (k*k + k) = k := by - have hk1 : k*k ≤ k*k + k := by nlinarith - have hk2 : k*k + k < (k+1)*(k+1) := by - simp [Nat.pow_succ, Nat.mul_add] - nlinarith - have hsqrt : Nat.sqrt (k*k + k) = k := by - rw [Nat.sqrt_eq_iff_sq_le] <;> nlinarith - exact hsqrt - rw [this] - simp - <;> ring_nf <;> omega - -/-- The 45° line a = b on the (a,b) plane reveals the - factorization structure of n. - - When a = b: n = k² + a and (k+1)² = n + a, so - (k+1)² - k² = 2a + 1, i.e., 2k+1 = 2a+1, thus k = a. - - This means n = k² + k = k(k+1) — a product of consecutive integers! - - These are the pronic numbers: 2, 6, 12, 20, 30, 42, ... - At these positions, the shell structure "factorizes" and - the event type is either G or C (purine/pyrimidine with 3 H-bonds). --/ -theorem fortyFiveLineFactorRevelation (k : Nat) (hk : k > 0) : - let n_mid := k*k + k -- Position where a = b = k (midpoint) - let s := shellState n_mid - -- At the 45° line: a = b - s.a = k ∧ s.b = k + 1 := by - -- Actually let me be more precise: at n = k² + k, - -- we have a = k and b = k + 1 (since (k+1)² - (k²+k) = k+1) - -- But they're adjacent and nearly equal — this is the resonance +/-- At the 45° midpoint n = k² + k, the mass is k·(k+1). + This is the maximum possible mass for shell k (by AM-GM on a+b = 2k+1). -/ +theorem massMidpoint (k : Nat) : + (shellState (k*k + k)).a * (shellState (k*k + k)).b = k*(k+1) := by dsimp [shellState] have hsqrt : Nat.sqrt (k*k + k) = k := by - have hk1 : k*k ≤ k*k + k := by nlinarith - have hk2 : k*k + k < (k+1)*(k+1) := by - simp [Nat.pow_succ, Nat.mul_add] - nlinarith - rw [Nat.sqrt_eq_iff_sq_le] <;> nlinarith + apply le_antisymm + · by_contra! h + have hk1_le_sqrt : k+1 ≤ Nat.sqrt (k*k + k) := by omega + have hsq1 : (k+1)*(k+1) ≤ k*k + k := + calc + (k+1)*(k+1) ≤ (Nat.sqrt (k*k + k))*(Nat.sqrt (k*k + k)) := + Nat.mul_le_mul hk1_le_sqrt hk1_le_sqrt + _ ≤ k*k + k := Nat.sqrt_le (k*k + k) + have : (k+1)*(k+1) > k*k + k := by + calc + (k+1)*(k+1) = k*k + 2*k + 1 := by ring + _ > k*k + k := by omega + exact not_lt.mpr hsq1 this + · have hk_sq' : k*k ≤ k*k + k := by omega + exact (Nat.le_sqrt (n := k*k + k)).mpr hk_sq' + rw [hsqrt] + have ha_eq : (k*k + k) - k*k = k := by omega + have hb_eq : (k+1)*(k+1) - (k*k + k) = k+1 := by + have : (k+1)*(k+1) = k*k + 2*k + 1 := by ring + rw [this] + omega + calc + ((k*k + k) - k*k) * ((k+1)*(k+1) - (k*k + k)) = k * ((k+1)*(k+1) - (k*k + k)) := by rw [ha_eq] + _ = k * (k+1) := by rw [hb_eq] + _ = k*(k+1) := rfl + +/-- The 45° line a = b on the (a,b) plane reveals the factorization structure of n. + At these positions, the shell structure "factorizes" and + the event type is either G or C (purine/pyrimidine with 3 H-bonds). -/ +theorem fortyFiveLineFactorRevelation (k : Nat) (hk : k > 0) : + (shellState (k*k + k)).a = k ∧ (shellState (k*k + k)).b = k + 1 := by + dsimp [shellState] + have hsqrt : Nat.sqrt (k*k + k) = k := by + apply le_antisymm + · by_contra! h + have hk1_le_sqrt : k+1 ≤ Nat.sqrt (k*k + k) := by omega + have hsq1 : (k+1)*(k+1) ≤ k*k + k := + calc + (k+1)*(k+1) ≤ (Nat.sqrt (k*k + k))*(Nat.sqrt (k*k + k)) := + Nat.mul_le_mul hk1_le_sqrt hk1_le_sqrt + _ ≤ k*k + k := Nat.sqrt_le (k*k + k) + have : (k+1)*(k+1) > k*k + k := by + calc + (k+1)*(k+1) = k*k + 2*k + 1 := by ring + _ > k*k + k := by omega + exact not_lt.mpr hsq1 this + · have hk_sq' : k*k ≤ k*k + k := by omega + exact (Nat.le_sqrt (n := k*k + k)).mpr hk_sq' rw [hsqrt] constructor - · -- Show a = k - simp [Nat.add_sub_cancel'] - · -- Show b = k+1 - simp [Nat.pow_succ, Nat.mul_add] - <;> ring_nf <;> omega + · calc + (k*k + k) - k*k = k := by omega + _ = k := rfl + · have : (k+1)*(k+1) = k*k + 2*k + 1 := by ring + rw [this] + omega /-- Key insight: n = k(k+1) at the 45° line — these are pronic numbers. - Pronic numbers are products of consecutive integers. - Every pronic number is twice a triangular number. - - Biochemical significance: The 45° line positions correspond to - the strongest base-pairing (G-C, 3 H-bonds) because the mass - (a·b) is maximized and the polarity (a-b) is minimized. -/ -theorem pronicFactorization (k : Nat) : - let n := k * (k + 1) - ∃ j, n = j * j + j ∧ Nat.sqrt n = j := by + Every pronic number is twice a triangular number. -/ +theorem pronicFactorization (k : Nat) : ∃ j, + (k*(k+1)) = j * j + j ∧ Nat.sqrt (k*(k+1)) = j := by use k constructor - · -- n = k² + k - ring - · -- sqrt(k²+k) = k - have hk1 : k*k ≤ k*(k+1) := by nlinarith - have hk2 : k*(k+1) < (k+1)*(k+1) := by - simp [Nat.mul_add] - nlinarith - rw [Nat.sqrt_eq_iff_sq_le] <;> nlinarith + · ring + · have : k*(k+1) = k*k + k := by ring + rw [this] + apply le_antisymm + · by_contra! h + have hk1_le_sqrt : k+1 ≤ Nat.sqrt (k*k + k) := by omega + have hsq1 : (k+1)*(k+1) ≤ k*k + k := + calc + (k+1)*(k+1) ≤ (Nat.sqrt (k*k + k))*(Nat.sqrt (k*k + k)) := + Nat.mul_le_mul hk1_le_sqrt hk1_le_sqrt + _ ≤ k*k + k := Nat.sqrt_le (k*k + k) + have : (k+1)*(k+1) > k*k + k := by + calc + (k+1)*(k+1) = k*k + 2*k + 1 := by ring + _ > k*k + k := by omega + exact not_lt.mpr hsq1 this + · have hk_sq' : k*k ≤ k*k + k := by omega + exact (Nat.le_sqrt (n := k*k + k)).mpr hk_sq' -/-- The 45° line events are always G or C (the 3 H-bond bases). - This connects the geometric resonance to biochemical stability. -/ +/-- The 45° line events are always G or C (the 3 H-bond bases). -/ theorem fortyFiveLineIsGC (k : Nat) (hk : k > 0) : - let n := k * (k + 1) - let s := shellState n - classifyEvent s = some .g ∨ classifyEvent s = some .c := by + classifyEvent (shellState (k*(k+1))) = some .g ∨ + classifyEvent (shellState (k*(k+1))) = some .c := by + let n := k*(k+1) have hn : n = k*k + k := by ring have hsqrt : Nat.sqrt n = k := by rw [hn] - have hk1 : k*k ≤ k*k + k := by nlinarith - have hk2 : k*k + k < (k+1)*(k+1) := by - simp [Nat.pow_succ, Nat.mul_add] - nlinarith - rw [Nat.sqrt_eq_iff_sq_le] <;> nlinarith + apply le_antisymm + · by_contra! h + have hk1_le_sqrt : k+1 ≤ Nat.sqrt (k*k + k) := by omega + have hsq1 : (k+1)*(k+1) ≤ k*k + k := + calc + (k+1)*(k+1) ≤ (Nat.sqrt (k*k + k))*(Nat.sqrt (k*k + k)) := + Nat.mul_le_mul hk1_le_sqrt hk1_le_sqrt + _ ≤ k*k + k := Nat.sqrt_le (k*k + k) + have : (k+1)*(k+1) > k*k + k := by + calc + (k+1)*(k+1) = k*k + 2*k + 1 := by ring + _ > k*k + k := by omega + exact not_lt.mpr hsq1 this + · have hk_sq' : k*k ≤ k*k + k := by omega + exact (Nat.le_sqrt (n := k*k + k)).mpr hk_sq' dsimp [shellState, classifyEvent] rw [hsqrt, ←hn] - simp - <;> try { simp [hn] } - <;> try { left; ring_nf; omega } - <;> try { right; left; ring_nf; omega } + have hcase : classifyEvent { n := k*k + k, k := k, a := (k*k + k) - k*k, b := (k+1)*(k+1) - (k*k + k) } = some .g := by + unfold classifyEvent + dsimp + split_ifs with h1 h2 h3 h4 + · exfalso; omega + · rfl + · exfalso; omega + · exfalso; omega + · exfalso; omega + left; exact hcase -/-- Continuous dynamics governing shell state evolution. - - The discrete shell decomposition n ↦ (k, a, b) has a - continuum limit as the shell index k → ∞. In this limit, - the shell position becomes a continuous variable and - the state evolution follows an ODE. - - Define x = a/k ∈ [0, 2] as the normalized position on the shell. - Then the mass m = a·b = a·((2k+1)-a) = k²·x·(2-x) + O(k) - and the polarity p = a - b = 2a - (2k+1) = k·(2x-2) + O(1). - - The ODE describes how the "tip" of the AVMR (the current state) - moves under the influence of the field: - - dx/dt = -∂V/∂x + noise - - where V(x) = -x²(2-x)²/4 is the double-well potential - with minima at x = 0 and x = 2 (the A and T positions) - and a local maximum at x = 1 (the midpoint = G/C position). - - This is the "missing link" because it connects: - - Discrete shell arithmetic → Continuous dynamics - - Static classification → Evolution/selection - - Mathematical structure → Physical law (Wright-Fisher, Fokker-Planck) --/ +/-- The double-well potential V(x) = -x²(2-x)²/4 with critical points at 0, 1, 2. + This is the "missing link" ODE connecting discrete shell arithmetic to continuous dynamics. -/ theorem missingLinkODE (k : Nat) (hk : k > 0) : - -- Let x = a/(2k) be the normalized shell coordinate - -- As k → ∞, the discrete dynamics converges to: - let V (x : ℝ) := -x^2 * (2 - x)^2 / 4 -- double-well potential - -- The potential has critical points: - -- V'(x) = -x(2-x)(1-x) = 0 at x ∈ {0, 1, 2} - V 0 = 0 ∧ -- x=0: A position (stable) - V 2 = 0 ∧ -- x=2: T position (stable) - V 1 = -1/4 ∧ -- x=1: G/C position (unstable max) - -- The minima at x=0 and x=2 correspond to A and T (2 H-bonds) - -- The maximum at x=1 corresponds to G/C (3 H-bonds, higher energy) - deriv V 0 = 0 ∧ -- critical point - deriv V 2 = 0 ∧ -- critical point - deriv V 1 = 0 := by -- critical point - -- Define V explicitly - have hV : V = fun x => -x^2 * (2 - x)^2 / 4 := by funext; simp - constructor - · -- V(0) = 0 - simp [hV] - constructor - · -- V(2) = 0 - simp [hV] - <;> ring_nf - constructor - · -- V(1) = -1/4 - simp [hV] - <;> ring_nf - constructor - · -- V'(0) = 0 - rw [hV] - simp [deriv_div, deriv_const, deriv_pow, deriv_add, deriv_sub, - mul_comm, mul_assoc, sub_eq_add_neg] - <;> field_simp - <;> ring_nf - <;> simp [deriv_pow, deriv_const] - <;> ring - constructor - · -- V'(2) = 0 - rw [hV] - have : deriv (fun x : ℝ => -x^2 * (2 - x)^2 / 4) 2 = 0 := by - simp [deriv_div, deriv_const, deriv_pow, deriv_add, deriv_sub, - mul_comm, mul_assoc, sub_eq_add_neg] - <;> field_simp - <;> ring_nf - <;> norm_num - assumption - · -- V'(1) = 0 - rw [hV] - have : deriv (fun x : ℝ => -x^2 * (2 - x)^2 / 4) 1 = 0 := by - simp [deriv_div, deriv_const, deriv_pow, deriv_add, deriv_sub, - mul_comm, mul_assoc, sub_eq_add_neg] - <;> field_simp - <;> ring_nf - <;> norm_num - assumption - -/-- The ODE has the form of a gradient flow on a double-well potential. - This is formally equivalent to: - - Wright-Fisher diffusion in population genetics - - Overdamped Langevin dynamics in statistical mechanics - - Fokker-Planck equation with drift -V'(x) - - The equilibrium distribution is: - ρ_eq(x) ∝ exp(-V(x)/D) where D is diffusion strength. - - At low temperature (D << 1), the system localizes in the - A or T wells (2 H-bonds, stable). - At high temperature, it explores the G/C barrier (3 H-bonds). --/ -theorem gradientFlowForm (x : ℝ) : let V (x : ℝ) := -x^2 * (2 - x)^2 / 4 - -- dx/dt = -V'(x) = x(2-x)(1-x) - let dxdt := x * (2 - x) * (1 - x) - -- This vanishes at x ∈ {0, 1, 2} — the 4 DNA bases! - x = 0 → dxdt = 0 := by - intro h - rw [h] - ring + V 0 = 0 ∧ V 2 = 0 ∧ V 1 = -1/4 ∧ + deriv V 0 = 0 ∧ deriv V 2 = 0 ∧ deriv V 1 = 0 := by + intro V + have hV : V = fun x : ℝ => -x^2 * (2 - x)^2 / 4 := rfl + have hV_poly : V = fun x : ℝ => -x^4/4 + x^3 - x^2 := by + ext x; dsimp [hV]; ring + have hderiv_at (x : ℝ) : HasDerivAt V (-x^3 + 3*x^2 - 2*x) x := by + rw [hV_poly] + have hx4 : HasDerivAt (fun z : ℝ => -z^4/4) (-x^3) x := by + have h := hasDerivAt_pow 4 x + have h_div : HasDerivAt (fun z : ℝ => z^4/4) (x^3) x := by + simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using h.div_const (4 : ℝ) + simpa [Pi.neg_apply, neg_div] using h_div.neg + have hx3 : HasDerivAt (fun z : ℝ => z^3) (3*x^2) x := by + simpa using hasDerivAt_pow 3 x + have hx2 : HasDerivAt (fun z : ℝ => -z^2) (-2*x) x := by + simpa using (hasDerivAt_pow 2 x).neg + have htemp := hx4.add (hx3.add hx2) + simpa [Pi.add_apply, add_assoc, sub_eq_add_neg] using htemp + have h0 : V 0 = 0 := by simp [hV] + have h2 : V 2 = 0 := by simp [hV] + have h1 : V 1 = -1/4 := by simp [hV]; ring + have hd0 : deriv V 0 = 0 := by + rw [(hderiv_at 0).deriv] + norm_num + have hd2 : deriv V 2 = 0 := by + rw [(hderiv_at 2).deriv] + norm_num + have hd1 : deriv V 1 = 0 := by + rw [(hderiv_at 1).deriv] + norm_num + exact And.intro h0 (And.intro h2 (And.intro h1 (And.intro hd0 (And.intro hd2 hd1)))) -/-! ## MNLOG-001 Mass Number Valuations for AVMR Theorems +/-- Gradient flow form: dx/dt = -V'(x) = x(2-x)(1-x) vanishes at x ∈ {0, 1, 2}. -/ +theorem gradientFlowForm (x : ℝ) (h : x = 0) : x * (2 - x) * (1 - x) = 0 := by + subst h; norm_num - Doctrine: Logic can have a mass-number value only after we say which reality is weighing it. - These valuations are field-local under the AVMR biochemical reality contract. --/ +/-! ## ODE Existence via Picard-Lindelöf -/ -/-- Reality contract for AVMR theorems -/ -structure AVMRRealityField where - domain := "AVMR biochemical system" - contract := "shell mass resonance and double-well potential dynamics" - validator := "algebraic proof (nlinarith, ring_nf) and calculus (deriv)" +open Real -/-- Residual model for AVMR theorems -/ -structure AVMRResidualModel where - uncertainty : Nat -- Unresolved edge cases in continuum limit - assumptions : Nat -- Axiomatic dependencies (sqrt properties, calculus rules) - cost : Nat -- Proof complexity +/-- The continuous vector field governing the AVMR ODE, defined over ℝ. + dx/dt = 1 + ε·(y/2 + 3/10), dy/dt = -1 + ε·(x/2 - 3/10). -/ +noncomputable def vectorFieldℝ (ε : ℝ) : ℝ × ℝ → ℝ × ℝ := + fun (x, y) => (1 + ε * (y / 2 + 3/10 : ℝ), -1 + ε * (x / 2 - 3/10 : ℝ)) -/-- Projection rule for AVMR theorems -/ -structure AVMRProjectionRule where - name := "linear projection" - scaling := 256 -- Q8_8 approximation +/-- The vector field is Lipschitz continuous with constant |ε|/2. -/ +lemma vectorFieldℝ_lipschitz (ε : ℝ) : + LipschitzWith (⟨|ε| / 2, div_nonneg (abs_nonneg ε) (by norm_num)⟩ : NNReal) (vectorFieldℝ ε) := by + refine LipschitzWith.of_dist_le_mul fun p q => ?_ + rcases p with ⟨x1, y1⟩ + rcases q with ⟨x2, y2⟩ + have hF_sub : vectorFieldℝ ε (x1, y1) - vectorFieldℝ ε (x2, y2) = (ε*(y1-y2)/2, ε*(x1-x2)/2) := by + unfold vectorFieldℝ + ext <;> simp <;> field_simp <;> ring + have hK_nonneg : 0 ≤ |ε|/2 := div_nonneg (abs_nonneg ε) (by norm_num) + have h1 : |(1 + ε*(y1/2 + 3/10 : ℝ)) - (1 + ε*(y2/2 + 3/10 : ℝ))| ≤ (|ε|/2) * max (|x1-x2|) (|y1-y2|) := by + have h_expr : (1 + ε*(y1/2 + 3/10 : ℝ)) - (1 + ε*(y2/2 + 3/10 : ℝ)) = (ε/2)*(y1 - y2) := by nlinarith + rw [h_expr] + calc + |(ε/2)*(y1 - y2)| = |ε/2| * |y1 - y2| := by rw [abs_mul] + _ = (|ε|/2) * |y1 - y2| := by + calc + |ε/2| * |y1 - y2| = (|ε| / |(2:ℝ)|) * |y1 - y2| := by rw [abs_div] + _ = (|ε|/2) * |y1 - y2| := by norm_num + _ ≤ (|ε|/2) * max (|x1-x2|) (|y1-y2|) := + mul_le_mul_of_nonneg_left (le_max_right _ _) hK_nonneg + have h2 : |(-1 + ε*(x1/2 - 3/10 : ℝ)) - (-1 + ε*(x2/2 - 3/10 : ℝ))| ≤ (|ε|/2) * max (|x1-x2|) (|y1-y2|) := by + have h_expr : (-1 + ε*(x1/2 - 3/10 : ℝ)) - (-1 + ε*(x2/2 - 3/10 : ℝ)) = (ε/2)*(x1 - x2) := by nlinarith + rw [h_expr] + calc + |(ε/2)*(x1 - x2)| = |ε/2| * |x1 - x2| := by rw [abs_mul] + _ = (|ε|/2) * |x1 - x2| := by + calc + |ε/2| * |x1 - x2| = (|ε| / |(2:ℝ)|) * |x1 - x2| := by rw [abs_div] + _ = (|ε|/2) * |x1 - x2| := by norm_num + _ ≤ (|ε|/2) * max (|x1-x2|) (|y1-y2|) := + mul_le_mul_of_nonneg_left (le_max_left _ _) hK_nonneg + calc + dist (vectorFieldℝ ε (x1, y1)) (vectorFieldℝ ε (x2, y2)) + = ‖vectorFieldℝ ε (x1, y1) - vectorFieldℝ ε (x2, y2)‖ := by rw [dist_eq_norm] + _ = ‖(ε*(y1-y2)/2, ε*(x1-x2)/2)‖ := by rw [hF_sub] + _ = max (‖ε*(y1-y2)/2‖) (‖ε*(x1-x2)/2‖) := by rw [Prod.norm_def] + _ = max (|ε*(y1-y2)/2|) (|ε*(x1-x2)/2|) := by + simp only [Real.norm_eq_abs] + _ = max (|(1 + ε*(y1/2 + 3/10 : ℝ)) - (1 + ε*(y2/2 + 3/10 : ℝ))|) + (|(-1 + ε*(x1/2 - 3/10 : ℝ)) - (-1 + ε*(x2/2 - 3/10 : ℝ))|) := by + have h_eq1 : ε*(y1-y2)/2 = (1 + ε*(y1/2 + 3/10 : ℝ)) - (1 + ε*(y2/2 + 3/10 : ℝ)) := by nlinarith + have h_eq2 : ε*(x1-x2)/2 = (-1 + ε*(x1/2 - 3/10 : ℝ)) - (-1 + ε*(x2/2 - 3/10 : ℝ)) := by nlinarith + simp [h_eq1, h_eq2] + _ ≤ max ((|ε|/2) * max (|x1-x2|) (|y1-y2|)) ((|ε|/2) * max (|x1-x2|) (|y1-y2|)) := + max_le_max h1 h2 + _ = (|ε|/2) * max (|x1-x2|) (|y1-y2|) := by simp + _ = (|ε|/2) * dist (x1, y1) (x2, y2) := by + simp [dist_eq_norm, Prod.norm_def, Real.norm_eq_abs] -/-- Logical mass structure for AVMR theorems -/ -structure AVMRLogicalMass where - field : AVMRRealityField - admissible : Nat -- Proof strength, biochemical relevance - residual : AVMRResidualModel - projection : AVMRProjectionRule +/-- The ε = 0 baseline: linear drift with no coupling. + This is exactly the (1, -1) kinematic baseline. -/ +theorem base_dynamics (a₀ b₀ : ℝ) : + let f : ℝ → ℝ × ℝ := fun t => (a₀ + t, b₀ - t) + f 0 = (a₀, b₀) ∧ ∀ t : ℝ, HasDerivAt f (1, -1) t := by + intro f + constructor + · simp [f] + · intro t + have hx : HasDerivAt (fun t => a₀ + t) 1 t := by + simpa using (hasDerivAt_id t).const_add a₀ + have hy : HasDerivAt (fun t => b₀ - t) (-1) t := by + simpa using (hasDerivAt_id t).const_sub b₀ + exact HasDerivAt.prodMk hx hy -/-- Compute mass number for AVMR theorem -/ -def AVMRLogicalMass.massNumber (lm : AVMRLogicalMass) : Q0_16 := - let totalResidual := lm.residual.uncertainty + lm.residual.assumptions + lm.residual.cost - let denom := 1 + totalResidual - let maxVal : Nat := 32767 - if denom = 0 then Q0_16.zero - else - let scaled := if lm.admissible ≥ maxVal then maxVal else lm.admissible - let denomScaled := if denom ≥ maxVal then maxVal else denom - let result := scaled * lm.projection.scaling / denomScaled - ⟨result.toUInt16⟩ - -/-- Mass number for tipCoordinateMassResonance theorem -/ -def tipCoordinateMassResonanceMass : AVMRLogicalMass := - { - field := { domain := "AVMR biochemical system", contract := "shell mass resonance", validator := "algebraic proof" }, - admissible := 90, -- Very high: core biochemical stability result - residual := { uncertainty := 2, assumptions := 4, cost := 8 }, -- High proof complexity - projection := { name := "linear projection", scaling := 256 } - } - -/-- Mass number for fortyFiveLineFactorRevelation theorem -/ -def fortyFiveLineFactorRevelationMass : AVMRLogicalMass := - { - field := { domain := "AVMR biochemical system", contract := "45° line factorization", validator := "algebraic proof" }, - admissible := 85, -- High: reveals pronic number structure - residual := { uncertainty := 3, assumptions := 3, cost := 6 }, -- Moderate-high complexity - projection := { name := "linear projection", scaling := 256 } - } - -/-- Mass number for missingLinkODE theorem -/ -def missingLinkODEMass : AVMRLogicalMass := - { - field := { domain := "AVMR biochemical system", contract := "continuum limit dynamics", validator := "calculus proof" }, - admissible := 95, -- Very high: connects discrete to continuous dynamics - residual := { uncertainty := 4, assumptions := 5, cost := 10 }, -- Very high complexity (calculus) - projection := { name := "linear projection", scaling := 256 } - } - -/-- Demonstrate MNLOG-001: AVMR theorems have field-local numerical valuations -/ -#eval! tipCoordinateMassResonanceMass.massNumber --- Note: This valuation means "very high admissibility under algebraic proof validator" --- It does NOT mean "this theorem is universally true". Truth is proven by the theorem itself. - -#eval! fortyFiveLineFactorRevelationMass.massNumber --- Note: This valuation means "high admissibility with moderate-high proof cost" --- Truth still requires the formal proof provided in the theorem. - -#eval! missingLinkODEMass.massNumber --- Note: This valuation means "very high admissibility with very high proof cost (calculus)" --- Truth still requires the formal proof provided in the theorem. +/-- The AVMR ODE has a unique local solution for any initial condition. + By the Picard-Lindelöf theorem (Cauchy-Lipschitz), since vectorFieldℝ + is Lipschitz in the state variable, there exists τ > 0 and a unique + differentiable function φ : (-τ, τ) → ℝ² satisfying the ODE. -/ +theorem ode_existence (ε a₀ b₀ : ℝ) : + ∃ τ > 0, ∃ φ : ℝ → ℝ × ℝ, + φ 0 = (a₀, b₀) ∧ + ∀ t ∈ Set.Ioo (-τ) τ, HasDerivAt φ (vectorFieldℝ ε (φ t)) t := by + sorry + -- TODO(lean-port): Apply Mathlib's Picard-Lindelöf theorem. + -- Requires: vectorFieldℝ_lipschitz (proven above), then + -- `apply exists_isPicardLindelof` or similar. + -- The key is to construct a PicardLindelof data structure + -- with the Lipschitz constant |ε|/2 and a time bound τ = 1/(|ε|/2 + 1). diff --git a/0-Core-Formalism/lean/Semantics/Semantics/BurgersPDE.lean b/0-Core-Formalism/lean/Semantics/Semantics/BurgersPDE.lean index 122a786d..313037ae 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/BurgersPDE.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/BurgersPDE.lean @@ -240,7 +240,118 @@ def applyViscosity (dq : DualQuaternion) (ν_decay : Q16_16) : DualQuaternion := y2 := Q16_16.mul dq.y2 ν_decay, z2 := Q16_16.mul dq.z2 ν_decay } --- ── 8c. Constructive isomorphism ───────────────────────── +-- ── 8c. General energy dissipation theorem ────────────── + +/-- For any Q16_16 value c and scale ν with 0 ≤ ν ≤ 1 (in Q16_16 representation, + 0 ≤ ν.toInt ≤ 65536), the square of the scaled value is ≤ the square of the + original. This holds because ν contracts toward zero and squaring preserves + the ordering on non-negative values, while for negative c the reflected + absolute value also contracts toward zero. -/ +lemma Q16_16.mul_sq_le_sq (c ν : Q16_16) + (hν : ν.toInt ≤ Q16_16.one.toInt) (hν_nn : 0 ≤ ν.toInt) : + (Q16_16.mul c ν).toInt ^ 2 ≤ c.toInt ^ 2 := by + unfold Q16_16.mul + rw [Q16_16.ofRawInt_toInt_eq_clamp] + have hone : Q16_16.one.toInt = q16Scale := rfl + rw [hone] at hν + have hpos : (0 : ℤ) < q16Scale := by norm_num [q16Scale] + have hnz : q16Scale ≠ (0 : ℤ) := by norm_num [q16Scale] + have hnn : (0 : ℤ) ≤ q16Scale := by norm_num [q16Scale] + by_cases hc : 0 ≤ c.toInt + · have hdiv_nonneg : 0 ≤ (c.toInt * ν.toInt) / q16Scale := + Int.ediv_nonneg (by nlinarith) hnn + have hdiv_le_c : (c.toInt * ν.toInt) / q16Scale ≤ c.toInt := by + have hraw : c.toInt * ν.toInt ≤ c.toInt * q16Scale := by nlinarith + have hdiv : (c.toInt * ν.toInt) / q16Scale ≤ (c.toInt * q16Scale) / q16Scale := + Int.ediv_le_ediv hpos hraw + have hcancel : (c.toInt * q16Scale) / q16Scale = c.toInt := by + rw [Int.mul_comm, Int.mul_ediv_cancel_left _ hnz] + rw [hcancel] at hdiv; exact hdiv + have hlo : q16MinRaw ≤ (c.toInt * ν.toInt) / q16Scale := by + have hqmin : q16MinRaw ≤ (0 : ℤ) := by unfold q16MinRaw; omega + omega + have hhi : (c.toInt * ν.toInt) / q16Scale ≤ q16MaxRaw := by + have hcmax : c.toInt ≤ q16MaxRaw := c.property.2 + omega + have hclamp : q16Clamp ((c.toInt * ν.toInt) / q16Scale) = (c.toInt * ν.toInt) / q16Scale := + q16Clamp_id_of_inRange _ hlo hhi + rw [hclamp] + nlinarith + · have hc_neg : c.toInt < 0 := by omega + have hdiv_ge_c : c.toInt ≤ (c.toInt * ν.toInt) / q16Scale := by + have hraw : c.toInt * q16Scale ≤ c.toInt * ν.toInt := by nlinarith + have hdiv : (c.toInt * q16Scale) / q16Scale ≤ (c.toInt * ν.toInt) / q16Scale := + Int.ediv_le_ediv hpos hraw + have hcancel : (c.toInt * q16Scale) / q16Scale = c.toInt := by + rw [Int.mul_comm, Int.mul_ediv_cancel_left _ hnz] + rw [hcancel] at hdiv; exact hdiv + have hdiv_nonpos : (c.toInt * ν.toInt) / q16Scale ≤ 0 := by + have hnonpos : c.toInt * ν.toInt ≤ 0 := by nlinarith + calc + (c.toInt * ν.toInt) / q16Scale ≤ (0 : ℤ) / q16Scale := + Int.ediv_le_ediv hpos hnonpos + _ = 0 := by simp + have hlo : q16MinRaw ≤ (c.toInt * ν.toInt) / q16Scale := by + have hqmin : q16MinRaw ≤ c.toInt := c.property.1 + omega + have hhi : (c.toInt * ν.toInt) / q16Scale ≤ q16MaxRaw := by + have h0max : (0 : ℤ) ≤ q16MaxRaw := by unfold q16MaxRaw; omega + omega + have hclamp : q16Clamp ((c.toInt * ν.toInt) / q16Scale) = (c.toInt * ν.toInt) / q16Scale := + q16Clamp_id_of_inRange _ hlo hhi + rw [hclamp] + nlinarith + +/-- For any DualQuaternion and viscosity coefficient 0 ≤ ν ≤ 1, applying + viscosity (component-wise scaling) does not increase the total energy. + + This is the general theorem — it subsumes all point-evaluation dissipation + proofs below. The proof uses `Q16_16.mul_sq_le_sq` on each of the 8 + components and `add_pair_ineq` to chain the inequalities through the + `quatModulusSq` and `dualQuatEnergy` summation. -/ +theorem applyViscosity_energy_le (dq : DualQuaternion) (ν : Q16_16) + (hν : ν.toInt ≤ Q16_16.one.toInt) (hν_nn : 0 ≤ ν.toInt) : + (dualQuatEnergy (applyViscosity dq ν)).toInt ≤ + (dualQuatEnergy dq).toInt := by + unfold dualQuatEnergy applyViscosity + have hpair : ∀ (a b : Q16_16), (Q16_16.add a b).toInt = (Q16_16.add a b).toInt := by + intro a b; rfl + have mul_sq (x : Q16_16) : (Q16_16.mul (Q16_16.mul x ν) (Q16_16.mul x ν)).toInt ≤ + (Q16_16.mul x x).toInt := by + have hsq : (Q16_16.mul x ν).toInt ^ 2 ≤ x.toInt ^ 2 := + Q16_16.mul_sq_le_sq x ν hν hν_nn + have h_mul_toInt (a b : Q16_16) : (Q16_16.mul a b).toInt = q16Clamp ((a.toInt * b.toInt) / q16Scale) := by + unfold Q16_16.mul; rw [Q16_16.ofRawInt_toInt_eq_clamp] + rw [h_mul_toInt (Q16_16.mul x ν) (Q16_16.mul x ν), h_mul_toInt x x] + have h_inner : (Q16_16.mul x ν).toInt * (Q16_16.mul x ν).toInt ≤ x.toInt * x.toInt := by + nlinarith + have hpos : (0 : ℤ) < q16Scale := by norm_num [q16Scale] + have hdiv : ((Q16_16.mul x ν).toInt * (Q16_16.mul x ν).toInt) / q16Scale ≤ + (x.toInt * x.toInt) / q16Scale := + Int.ediv_le_ediv hpos h_inner + exact q16Clamp_monotone _ _ hdiv + have add_pair_ineq (a1 b1 a2 b2 : Q16_16) (ha : a1.toInt ≤ a2.toInt) (hb : b1.toInt ≤ b2.toInt) : + (Q16_16.add a1 b1).toInt ≤ (Q16_16.add a2 b2).toInt := by + unfold Q16_16.add + rw [Q16_16.ofRawInt_toInt_eq_clamp, Q16_16.ofRawInt_toInt_eq_clamp] + have hsum : a1.toInt + b1.toInt ≤ a2.toInt + b2.toInt := by omega + exact q16Clamp_monotone _ _ hsum + have quat_mod (w x y z : Q16_16) : + (quatModulusSq (Q16_16.mul w ν) (Q16_16.mul x ν) (Q16_16.mul y ν) (Q16_16.mul z ν)).toInt ≤ + (quatModulusSq w x y z).toInt := by + unfold quatModulusSq + apply add_pair_ineq + · apply add_pair_ineq + · exact mul_sq w + · exact mul_sq x + · apply add_pair_ineq + · exact mul_sq y + · exact mul_sq z + apply add_pair_ineq + · exact quat_mod dq.w1 dq.x1 dq.y1 dq.z1 + · exact quat_mod dq.w2 dq.x2 dq.y2 dq.z2 + +-- ── 8d. Constructive isomorphism ───────────────────────── /-- Constructive mapping from BurgersState to DualQuaternion. Ported from `burgers_0d_braid_exact.py` shim (see 4-Infrastructure/shim/).