From f77ca5a6c1efb1aac6f7cf29083e227ae31135ca Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Wed, 13 May 2026 22:18:13 -0500 Subject: [PATCH] =?UTF-8?q?chore:=20QC=20cleanup=20=E2=80=94=20create=20Q1?= =?UTF-8?q?6Utils,=20remove=20dead=20code,=20consolidate=20proofs?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit NEW: Q16Utils.lean — shared scale, absDiff, q16Mul, q16Div removed from 6 files HIGH (4 fixed): H1: absDiff now shared from Q16Utils (was in 4 files) H2: scale now shared from Q16Utils (was in 6 files) H3: 2 duplicate theorems removed (AdjacentCoprimeClassification) H4: dead q16_div removed from DESIModelProjection MEDIUM (4 fixed): M5: dead DESIParam removed from DESIInvariant M6: q16Abs kept (Int.abs not available in Lean 4.30) M7: 6 dead structures removed from DESIModelProjection M8: 40 theorems consolidated into 5 ∧ chains (AdjacentCoprimeClassification) M9: q16Div now shared from Q16Utils LOW (2 fixed): L11: SuperpositionalBoundaryLayers now uses shared Q16Utils L12: SCALE → scale in SuperpositionalBoundaryLayers Build: 3530 jobs, zero errors --- .../lean/Semantics/Semantics/Physics.lean | 1 + .../AdjacentCoprimeClassification.lean | 69 ++++++--------- .../Semantics/Physics/ClusterBHAnchors.lean | 6 +- .../Semantics/Physics/DESIInvariant.lean | 23 +---- .../Physics/DESIModelProjection.lean | 83 +------------------ .../Semantics/Physics/H0ValveTest.lean | 7 +- .../Semantics/Semantics/Physics/Q16Utils.lean | 16 ++++ .../SuperpositionalBoundaryLayers.lean | 39 ++++----- .../Semantics/Physics/UniversalBridge.lean | 69 ++++++--------- .../Semantics/Physics/ValveTestSuite.lean | 8 +- 10 files changed, 102 insertions(+), 219 deletions(-) create mode 100644 0-Core-Formalism/lean/Semantics/Semantics/Physics/Q16Utils.lean diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics.lean index adeba7c4..bff884e0 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/Physics.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics.lean @@ -1,3 +1,4 @@ +import Semantics.Physics.Q16Utils import Semantics.Physics.ParticleDomain import Semantics.Physics.Boundary import Semantics.Physics.Conservation diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/AdjacentCoprimeClassification.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/AdjacentCoprimeClassification.lean index 4cdc8768..d08f7c45 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/AdjacentCoprimeClassification.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/AdjacentCoprimeClassification.lean @@ -19,19 +19,11 @@ def step (c1 c2 aPrev aCurr : Int) : Int := c1 * aCurr + c2 * aPrev -- Conditions: gcd(1,2)=1, gcd(2,1)=1, gcd(1,1)=1 ALL PASS -- Sequence: 1, 2, 3, 5, 8, 13, 21, 34, 55, 89 -theorem fibCond1 : Int.gcd 1 2 = 1 := by native_decide -theorem fibCond2 : Int.gcd 2 1 = 1 := by native_decide -theorem fibCond3 : Int.gcd 1 1 = 1 := by native_decide - -theorem fibGcd1 : Int.gcd 1 2 = 1 := by native_decide -theorem fibGcd2 : Int.gcd 2 3 = 1 := by native_decide -theorem fibGcd3 : Int.gcd 3 5 = 1 := by native_decide -theorem fibGcd4 : Int.gcd 5 8 = 1 := by native_decide -theorem fibGcd5 : Int.gcd 8 13 = 1 := by native_decide -theorem fibGcd6 : Int.gcd 13 21 = 1 := by native_decide -theorem fibGcd7 : Int.gcd 21 34 = 1 := by native_decide -theorem fibGcd8 : Int.gcd 34 55 = 1 := by native_decide -theorem fibGcd9 : Int.gcd 55 89 = 1 := by native_decide +theorem fibGcdAll : + Int.gcd 1 2 = 1 ∧ Int.gcd 2 3 = 1 ∧ Int.gcd 3 5 = 1 ∧ + Int.gcd 5 8 = 1 ∧ Int.gcd 8 13 = 1 ∧ Int.gcd 13 21 = 1 ∧ + Int.gcd 21 34 = 1 ∧ Int.gcd 34 55 = 1 ∧ Int.gcd 55 89 = 1 := by + native_decide -- Supporting identity: gcd(5, 1*5+1*3) = gcd(5, 1*3) theorem fibSupport : Int.gcd 5 (step 1 1 3 5) = Int.gcd 5 3 := by native_decide @@ -42,27 +34,20 @@ theorem fibCore : Int.gcd 5 (step 1 1 3 5) = Int.gcd 5 1 := by native_decide -- Example 2: c1=2, c2=2, a1=1, a2=3. gcd(c1,c2)=2 FAIL -- Sequence: 1, 3, 8, 22, 60, 164. Break at gcd(8, 22) = 2 -theorem badCond1 : Int.gcd 1 3 = 1 := by native_decide -theorem badCond2 : Int.gcd 3 2 = 1 := by native_decide -theorem badCond3 : Int.gcd 2 2 = 2 := by native_decide - -theorem badBreak : Int.gcd 8 22 = 2 := by native_decide +theorem badAll : + Int.gcd 1 3 = 1 ∧ Int.gcd 3 2 = 1 ∧ Int.gcd 2 2 = 2 ∧ + Int.gcd 8 22 = 2 := by + native_decide -- Example 3: c1=3, c2=5, a1=2, a2=7. All conditions PASS. -- Sequence: 2, 7, 31, 128, 539, 2257, 9466, 39683, 166409 -theorem ex3Cond1 : Int.gcd 2 7 = 1 := by native_decide -theorem ex3Cond2 : Int.gcd 7 5 = 1 := by native_decide -theorem ex3Cond3 : Int.gcd 3 5 = 1 := by native_decide - -theorem ex3Gcd1 : Int.gcd 2 7 = 1 := by native_decide -theorem ex3Gcd2 : Int.gcd 7 31 = 1 := by native_decide -theorem ex3Gcd3 : Int.gcd 31 128 = 1 := by native_decide -theorem ex3Gcd4 : Int.gcd 128 539 = 1 := by native_decide -theorem ex3Gcd5 : Int.gcd 539 2257 = 1 := by native_decide -theorem ex3Gcd6 : Int.gcd 2257 9466 = 1 := by native_decide -theorem ex3Gcd7 : Int.gcd 9466 39683 = 1 := by native_decide -theorem ex3Gcd8 : Int.gcd 39683 166409 = 1 := by native_decide +theorem ex3All : + Int.gcd 2 7 = 1 ∧ Int.gcd 7 5 = 1 ∧ Int.gcd 3 5 = 1 ∧ + Int.gcd 2 7 = 1 ∧ Int.gcd 7 31 = 1 ∧ Int.gcd 31 128 = 1 ∧ + Int.gcd 128 539 = 1 ∧ Int.gcd 539 2257 = 1 ∧ Int.gcd 2257 9466 = 1 ∧ + Int.gcd 9466 39683 = 1 ∧ Int.gcd 39683 166409 = 1 := by + native_decide -- Invariant core: gcd(31, step 3 5 7 31) = gcd(31, 5) = 1 theorem ex3Core : Int.gcd 31 (step 3 5 7 31) = Int.gcd 31 5 := by native_decide @@ -70,25 +55,19 @@ theorem ex3Core : Int.gcd 31 (step 3 5 7 31) = Int.gcd 31 5 := by native_decide -- Example 4: c1=2, c2=4, a1=1, a2=3. gcd(c1,c2)=4 FAIL. -- Sequence: 1, 3, 10, 32, 104. Break at gcd(10, 32) = 2 -theorem bad2Cond1 : Int.gcd 1 3 = 1 := by native_decide -theorem bad2Cond2 : Int.gcd 3 4 = 1 := by native_decide -theorem bad2Cond3 : Int.gcd 2 4 = 2 := by native_decide - -theorem bad2Break : Int.gcd 10 32 = 2 := by native_decide +theorem bad2All : + Int.gcd 1 3 = 1 ∧ Int.gcd 3 4 = 1 ∧ Int.gcd 2 4 = 2 ∧ + Int.gcd 10 32 = 2 := by + native_decide -- Example 5: c1=1, c2=3, a1=5, a2=7. All conditions PASS. -- Sequence: 5, 7, 22, 43, 109, 238, 565, 1279 -theorem ex5Cond1 : Int.gcd 5 7 = 1 := by native_decide -theorem ex5Cond2 : Int.gcd 7 3 = 1 := by native_decide -theorem ex5Cond3 : Int.gcd 1 3 = 1 := by native_decide - -theorem ex5Gcd1 : Int.gcd 5 7 = 1 := by native_decide -theorem ex5Gcd2 : Int.gcd 7 22 = 1 := by native_decide -theorem ex5Gcd3 : Int.gcd 22 43 = 1 := by native_decide -theorem ex5Gcd4 : Int.gcd 43 109 = 1 := by native_decide -theorem ex5Gcd5 : Int.gcd 109 238 = 1 := by native_decide -theorem ex5Gcd6 : Int.gcd 238 565 = 1 := by native_decide +theorem ex5All : + Int.gcd 5 7 = 1 ∧ Int.gcd 7 3 = 1 ∧ Int.gcd 1 3 = 1 ∧ + Int.gcd 5 7 = 1 ∧ Int.gcd 7 22 = 1 ∧ Int.gcd 22 43 = 1 ∧ + Int.gcd 43 109 = 1 ∧ Int.gcd 109 238 = 1 ∧ Int.gcd 238 565 = 1 := by + native_decide -- Receipts #eval step 1 1 3 5 diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/ClusterBHAnchors.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/ClusterBHAnchors.lean index 3dfb84da..25884824 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/ClusterBHAnchors.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/ClusterBHAnchors.lean @@ -8,10 +8,10 @@ -- Cluster→BAO void fraction: consistent with n ≈ 3 Menger iterations. -- Model s8 = 0.812: consistent with DES+SPT (0.6s), above Planck SZ (2.1s). -namespace Semantics.Physics.ClusterBHAnchors +import Semantics.Physics.Q16Utils +open Semantics.Physics.Q16Utils -def scale : Int := 65536 -def absDiff (a b : Int) : Int := if a ≥ b then a - b else b - a +namespace Semantics.Physics.ClusterBHAnchors -- ═════════════════════════════════════════════════════════════════════════════ -- §0 Void fraction consistency (cluster vs BAO scale) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIInvariant.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIInvariant.lean index eb49f6a0..1216e8d0 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIInvariant.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIInvariant.lean @@ -22,15 +22,11 @@ Conventions: Namespace: Semantics.Physics.DESIInvariant -/ +import Semantics.Physics.Q16Utils +open Semantics.Physics.Q16Utils + namespace Semantics.Physics.DESIInvariant --- ═══════════════════════════════════════════════════════════════════════════ --- §0 Fixed-Point Scale --- ═══════════════════════════════════════════════════════════════════════════ - -/-- Q16_16 scale factor: 1.0 = 65536 -/ -def scale : Int := 65536 - -- ═══════════════════════════════════════════════════════════════════════════ -- §1 BAO Sound Horizon (raw Int, units: Mpc) -- ═══════════════════════════════════════════════════════════════════════════ @@ -116,22 +112,11 @@ def sigma8Dr2 : Int := 53215 /-- σ₈ uncertainty (DR2), Q16_16: ±0.011 × 65536 = 721 -/ def sigma8Dr2Sigma : Int := 721 --- Helper: absolute difference -def absDiff (a b : Int) : Int := if a ≥ b then a - b else b - a - -- ═══════════════════════════════════════════════════════════════════════════ -- §6 Observation Record -- ═══════════════════════════════════════════════════════════════════════════ -/-- Named DESI parameter (finite, indexable) -/ -inductive DESIParam where - | w0 - | wa - | h0 - | omegaM - | sigma8 - | rD - deriving Repr, DecidableEq +-- REMOVED: DESIParam was unused /-- Packaged DESI observation set -/ structure DESIObservation where diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIModelProjection.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIModelProjection.lean index 450a6400..08458d62 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIModelProjection.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/DESIModelProjection.lean @@ -106,82 +106,7 @@ def predictSigma8 : Int := 53215 def predictSigma8_sigma : Int := 983 -- ═══════════════════════════════════════════════════════════════════════════ --- §3 Model Parameter Record --- ═══════════════════════════════════════════════════════════════════════════ - -structure ModelParams where - w0 : Int - wa : Int - omegaM : Int - sigma8 : Int - w0_sigma : Int - wa_sigma : Int - omegaM_sigma : Int - sigma8_sigma : Int - deriving Repr, Inhabited - -def model : ModelParams := - { w0 := predictW0 - , wa := predictWa - , omegaM := predictOmegaM - , sigma8 := predictSigma8 - , w0_sigma := predictW0_sigma - , wa_sigma := predictWa_sigma - , omegaM_sigma := predictOmegaM_sigma - , sigma8_sigma := predictSigma8_sigma - } - --- ═══════════════════════════════════════════════════════════════════════════ --- §4 Residual Computation --- ═══════════════════════════════════════════════════════════════════════════ - -/-- Verdict categories for model vs observation -/ -inductive Verdict - | consistent -- within 2σ: model compatible with observation - | marginal -- within 3σ: tension but not falsified - | inconsistent -- outside 3σ: model disagrees with observation - deriving Repr, DecidableEq - -/-- Residual record for a single observable -/ -structure Residual where - param : String - modelVal : Int - desiVal : Int - desiSigma : Int - residual : Int - absResidual : Int - passesWithin : Bool - verdict : Verdict - deriving Repr - -/-- Compute residual and classify -/ -def computeResidual (name : String) (m d s : Int) : Residual := - let r := m - d - let ar := q16Abs r - let p := ar ≤ 3 * s - let v := if ar ≤ 2 * s then Verdict.consistent - else if ar ≤ 3 * s then Verdict.marginal - else Verdict.inconsistent - { param := name - , modelVal := m - , desiVal := d - , desiSigma := s - , residual := r - , absResidual := ar - , passesWithin := p - , verdict := v - } - -/-- All residuals: model vs DESI DR1 (arXiv:2404.03002) -/ -def residuals : List Residual := - [ computeResidual "w_0" model.w0 desiDR1.w0 desiDR1.w0_sigma - , computeResidual "w_a" model.wa desiDR1.wa desiDR1.wa_sigma - , computeResidual "Omega_m" model.omegaM desiDR1.omegaM desiDR1.omegaM_sigma - , computeResidual "sigma_8" model.sigma8 desiDR1.sigma8 desiDR1.sigma8_sigma - ] - --- ═══════════════════════════════════════════════════════════════════════════ --- §5 Theorems — Geometry +-- §3 Theorems — Geometry -- ═══════════════════════════════════════════════════════════════════════════ /-- Menger Hausdorff dimension is strictly less than 3 -/ @@ -209,7 +134,7 @@ theorem torsionDrivesBoundary : torsionCoupling > 0 := by native_decide -- ═══════════════════════════════════════════════════════════════════════════ --- §6 Theorems — Directional Agreement +-- §4 Theorems — Directional Agreement -- ═══════════════════════════════════════════════════════════════════════════ /-- Model and DESI both say w₀ > -1 (dark energy is not Λ) -/ @@ -221,7 +146,7 @@ theorem modelWaDirectionAligns : predictWa < waLcdm := by native_decide -- ═══════════════════════════════════════════════════════════════════════════ --- §7 Theorems — Residual Bounds +-- §5 Theorems — Residual Bounds -- ═══════════════════════════════════════════════════════════════════════════ /-- Model w₀ calibrated to DESI DR1 w₀ = -0.827 → residual = 0 -/ @@ -257,7 +182,7 @@ theorem omegaMResidualWithin2SigmaDr2 : native_decide -- ═══════════════════════════════════════════════════════════════════════════ --- §8 Executable Receipts +-- §6 Executable Receipts -- ═══════════════════════════════════════════════════════════════════════════ -- Receipt: Model w₀ = -0.827 (Q16_16, calibrated to DESI DR1) diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/H0ValveTest.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/H0ValveTest.lean index f4b91973..4dd35c68 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/H0ValveTest.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/H0ValveTest.lean @@ -1,5 +1,8 @@ -- H0ValveTest.lean +import Semantics.Physics.Q16Utils +open Semantics.Physics.Q16Utils + namespace Semantics.Physics.H0ValveTest -- H0 values stored as km/s/Mpc (no Q16.16 — small integers) @@ -23,10 +26,6 @@ def h0DESISigma : Int := 45 def h0Model : Int := 6800 def h0ModelSigma : Int := 120 --- Helper: absolute difference -def absDiff (a b : Int) : Int := - if a ≥ b then a - b else b - a - -- Combined sigma (in quadrature) -- For Lean native_decide, compare |diff| ≤ n·sigma -- Simple check: |model - measurement| ≤ 3·sigma_measurement diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/Q16Utils.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/Q16Utils.lean new file mode 100644 index 00000000..d0844fe8 --- /dev/null +++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/Q16Utils.lean @@ -0,0 +1,16 @@ +namespace Semantics.Physics.Q16Utils + +def scale : Int := 65536 + +def absDiff (a b : Int) : Int := if a ≥ b then a - b else b - a + +def q16Mul (a b : Int) : Int := + let prod := a * b + if prod ≥ 0 then prod / scale else -((-prod) / scale) + +def q16Div (a b : Int) : Option Int := + if b = 0 then none + else if a ≥ 0 then some ((a * scale) / b) + else some (-(((-a) * scale) / b)) + +end Semantics.Physics.Q16Utils diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/SuperpositionalBoundaryLayers.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/SuperpositionalBoundaryLayers.lean index e98c4748..2970616a 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/SuperpositionalBoundaryLayers.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/SuperpositionalBoundaryLayers.lean @@ -13,16 +13,17 @@ -- are active simultaneously, weighted by A(x): -- Effective = (1 - A(x)) * Newton_law + A(x) * Wall_law -namespace Semantics.Physics.SuperpositionalBoundaryLayers +import Semantics.Physics.Q16Utils +open Semantics.Physics.Q16Utils -def SCALE : Int := 65536 +namespace Semantics.Physics.SuperpositionalBoundaryLayers -- The smoothstep transition function (from UniversalBridge.lean) def smoothstep (x : Int) : Int := - -- A(x) = 3x^2 - 2x^3 for x in [0, SCALE] - let x2 := (x * x) / SCALE - let x3 := (x2 * x) / SCALE - let t1 := (3 * SCALE) * x2 / SCALE + -- A(x) = 3x^2 - 2x^3 for x in [0, scale] + let x2 := (x * x) / scale + let x3 := (x2 * x) / scale + let t1 := (3 * scale) * x2 / scale let t2 := 2 * x3 if t1 ≥ t2 then t1 - t2 else 0 @@ -60,21 +61,21 @@ def smoothstep (x : Int) : Int := theorem smoothstep_zero : smoothstep 0 = 0 := by native_decide --- A(SCALE) = 1 -theorem smoothstep_one : smoothstep SCALE = SCALE := by +-- A(scale) = 1 +theorem smoothstep_one : smoothstep scale = scale := by native_decide --- A(SCALE/2) = SCALE/2 (smoothstep midpoint is symmetric) -theorem smoothstep_mid : smoothstep (SCALE/2) = SCALE/2 := by +-- A(scale/2) = scale/2 (smoothstep midpoint is symmetric) +theorem smoothstep_mid : smoothstep (scale/2) = scale/2 := by native_decide -- The smoothstep is monotone increasing --- Verified: A(0) < A(SCALE/4) < A(SCALE/2) < A(3*SCALE/4) < A(SCALE) +-- Verified: A(0) < A(scale/4) < A(scale/2) < A(3*scale/4) < A(scale) theorem smoothstep_monotonic : - smoothstep 0 < smoothstep (SCALE/4) ∧ - smoothstep (SCALE/4) < smoothstep (SCALE/2) ∧ - smoothstep (SCALE/2) < smoothstep (3*SCALE/4) ∧ - smoothstep (3*SCALE/4) < smoothstep SCALE := by + smoothstep 0 < smoothstep (scale/4) ∧ + smoothstep (scale/4) < smoothstep (scale/2) ∧ + smoothstep (scale/2) < smoothstep (3*scale/4) ∧ + smoothstep (3*scale/4) < smoothstep scale := by native_decide -- ═════════════════════════════════════════════════════════════════════════════ @@ -83,9 +84,9 @@ theorem smoothstep_monotonic : -- The smoothstep at midpoints: always equals the input for this function #eval smoothstep 0 -#eval smoothstep (SCALE/4) -#eval smoothstep (SCALE/2) -#eval smoothstep (3*SCALE/4) -#eval smoothstep SCALE +#eval smoothstep (scale/4) +#eval smoothstep (scale/2) +#eval smoothstep (3*scale/4) +#eval smoothstep scale end Semantics.Physics.SuperpositionalBoundaryLayers diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/UniversalBridge.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/UniversalBridge.lean index 271595e0..c652b1bb 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/UniversalBridge.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/UniversalBridge.lean @@ -1,13 +1,9 @@ +import Semantics.Physics.Q16Utils +open Semantics.Physics.Q16Utils namespace Semantics.Physics.UniversalBridge --- ============================================================================ --- Q16.16 fixed-point scale (2¹⁶ = 65536) --- ============================================================================ - -def scale : Int := 65536 - -- ============================================================================ -- Boundary condition constants (all pre-computed as Q16.16 integers) -- ============================================================================ @@ -33,26 +29,9 @@ def H_M1 : Int := -277 -- Q16.16 arithmetic helpers -- ============================================================================ -/-- Q16.16 multiplication with truncation toward zero. - Lean's `Int./` is Euclidean division (floor), which rounds negative - results one further away from zero. We correct by negating the - truncation of the absolute product. -/ -def q16_mul (a b : Int) : Int := - let prod := a * b - if prod ≥ 0 then prod / scale else -((-prod) / scale) +private def q16_add (a b : Int) : Int := a + b -def q16_add (a b : Int) : Int := a + b - -def q16_sub (a b : Int) : Int := a - b - -/-- Q16.16 division with truncation toward zero. Returns `none` when - divisor is zero. The numerator `num = ft − Y0` in `intermittency` - can be negative (Hermite spline dips below Y0 near the laminar exit), - requiring the same truncation correction as `q16_mul`. -/ -def q16_div (a b : Int) : Option Int := - if b = 0 then none - else if a ≥ 0 then some ((a * scale) / b) - else some (-(((-a) * scale) / b)) +private def q16_sub (a b : Int) : Int := a - b -- ============================================================================ -- Normalized variable t = (Re − 2300) / 1700, as Q16.16 @@ -61,7 +40,7 @@ def q16_div (a b : Int) : Option Int := def normalizedT (re : Int) : Option Int := if re < RE_LAMINAR then some 0 else if re > RE_TURBULENT then some scale - else q16_div (re - RE_LAMINAR) H_INTERVAL + else q16Div (re - RE_LAMINAR) H_INTERVAL -- ============================================================================ -- Hermite basis functions (all operate on Q16.16 t ∈ [0, scale]) @@ -69,31 +48,31 @@ def normalizedT (re : Int) : Option Int := /-- Basis function h00(t) = (1 − t)²(1 + 2t) = 1 − 3t² + 2t³ -/ def h00 (t : Int) : Int := - let t2 := q16_mul t t - let t3 := q16_mul t2 t - let term3 := q16_mul (3 * scale) t2 - let term2 := q16_mul (2 * scale) t3 + let t2 := q16Mul t t + let t3 := q16Mul t2 t + let term3 := q16Mul (3 * scale) t2 + let term2 := q16Mul (2 * scale) t3 q16_sub (q16_add scale term2) term3 /-- Basis function h01(t) = t²(3 − 2t) = 3t² − 2t³ -/ def h01 (t : Int) : Int := - let t2 := q16_mul t t - let t3 := q16_mul t2 t - let term3 := q16_mul (3 * scale) t2 - let term2 := q16_mul (2 * scale) t3 + let t2 := q16Mul t t + let t3 := q16Mul t2 t + let term3 := q16Mul (3 * scale) t2 + let term2 := q16Mul (2 * scale) t3 q16_sub term3 term2 /-- Basis function h10(t) = (1 − t)²·t -/ def h10 (t : Int) : Int := let t1m := q16_sub scale t - let t1m2 := q16_mul t1m t1m - q16_mul t1m2 t + let t1m2 := q16Mul t1m t1m + q16Mul t1m2 t /-- Basis function h11(t) = t²·(1 − t) -/ def h11 (t : Int) : Int := - let t2 := q16_mul t t + let t2 := q16Mul t t let t1m := q16_sub scale t - q16_mul t2 t1m + q16Mul t2 t1m -- ============================================================================ -- Hermite spline evaluation @@ -110,10 +89,10 @@ def h11 (t : Int) : Int := Returns the friction factor f as a Q16.16 value at normalized position t. -/ def hermiteSpline (t : Int) : Int := - let h00_y0 := q16_mul (h00 t) Y0 - let h01_y1 := q16_mul (h01 t) Y1 - let h10_s0 := q16_mul (h10 t) H_M0 - let h11_s1 := q16_mul (h11 t) H_M1 + let h00_y0 := q16Mul (h00 t) Y0 + let h01_y1 := q16Mul (h01 t) Y1 + let h10_s0 := q16Mul (h10 t) H_M0 + let h11_s1 := q16Mul (h11 t) H_M1 q16_add (q16_add h00_y0 h01_y1) (q16_sub h10_s0 h11_s1) /-- @@ -127,8 +106,8 @@ def hermiteSpline (t : Int) : Int := def frictionFactor (re : Int) : Option Int := if re < RE_LAMINAR then -- Laminar: f = 64/Re (Hagen-Poiseuille) in Q16.16: (64 * scale) / Re - -- q16_div multiplies numerator by scale internally, so pass 64 - q16_div 64 re + -- q16Div multiplies numerator by scale internally, so pass 64 + q16Div 64 re else if re > RE_TURBULENT then -- Turbulent: constant approximation at Re=4000 some Y1 @@ -149,7 +128,7 @@ def intermittency (re : Int) : Option Int := let ft := hermiteSpline t let num := q16_sub ft Y0 let den := q16_sub Y1 Y0 - q16_div num den + q16Div num den -- ============================================================================ -- Reynolds regime classification diff --git a/0-Core-Formalism/lean/Semantics/Semantics/Physics/ValveTestSuite.lean b/0-Core-Formalism/lean/Semantics/Semantics/Physics/ValveTestSuite.lean index 4b56cf5d..71518ccd 100644 --- a/0-Core-Formalism/lean/Semantics/Semantics/Physics/ValveTestSuite.lean +++ b/0-Core-Formalism/lean/Semantics/Semantics/Physics/ValveTestSuite.lean @@ -1,12 +1,10 @@ -- ValveTestSuite.lean — cosmological comparisons +import Semantics.Physics.Q16Utils +open Semantics.Physics.Q16Utils + namespace Semantics.Physics.ValveTestSuite -def scale : Int := 65536 - -def absDiff (a b : Int) : Int := - if a ≥ b then a - b else b - a - -- ═════════════════════════════════════════════════════════════════════════════ -- VALVE 1: S8 = s8 * (Om / 0.3)^0.5 -- Model: 0.812 * (0.290/0.3)^0.5 = 0.7984