allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-08-10 23:50:34 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fix q16_div truncation and correct comment: round 2 adversarial review

Browse source 
- Fix q16_div to use truncation-toward-zero (matching q16_mul) so that
  negative intermediates in intermittency produce correct Q16.16 values
- Correct Hagen-Poiseuille attribution in laminar branch comment
- Update preamble note to cover both q16_mul and q16_div truncation
- All 24 theorems still pass, build clean (3527 jobs)
This commit is contained in:
Brandon Schneider 2026-05-13 11:44:12 -05:00
parent 62c04ddf7d
commit a2d6f4b467
1 changed files with 11 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
0-Core-Formalism/lean/Semantics/Semantics/Physics/UniversalBridge.lean
View file

@ -18,10 +18,9 @@
Note on Q16.16 arithmetic: Note on Q16.16 arithmetic:
Lean 4.30 uses Euclidean (floor) division for `Int./`. Standard Q16.16 Lean 4.30 uses Euclidean (floor) division for `Int./`. Standard Q16.16
multiplication truncates toward zero. We correct this via an explicit truncates toward zero. We apply a sign check in `q16_mul` and `q16_div`
sign check in `q16_mul`. The difference is at most 1 ULP (1/65536) to correct for this. The difference is at most 1 ULP (1/65536) and is
and is negligible for engineering purposes, but formal correctness negligible for engineering purposes, but formal correctness requires it.
requires the fix.
-/ -/
namespace Semantics.Physics.UniversalBridge namespace Semantics.Physics.UniversalBridge
@ -69,11 +68,14 @@ def q16_add (a b : Int) : Int := a + b
def q16_sub (a b : Int) : Int := a - b def q16_sub (a b : Int) : Int := a - b
/-- Q16.16 division guarded against division by zero. Returns `none` when /-- Q16.16 division with truncation toward zero. Returns `none` when
divisor is zero. Euclidean division is acceptable here because the divisor is zero. The numerator `num = ft − Y0` in `intermittency`
result is always non-negative for valid Reynolds inputs. -/ 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 := def q16_div (a b : Int) : Option Int :=
if b = 0 then none else some ((a * SCALE) / b) if b = 0 then none
else if a ≥ 0 then some ((a * SCALE) / b)
else some (-(((-a) * SCALE) / b))
-- ============================================================================ -- ============================================================================
-- Normalized variable t = (Re − 2300) / 1700, as Q16.16 -- Normalized variable t = (Re − 2300) / 1700, as Q16.16
@ -147,7 +149,7 @@ def hermiteSpline (t : Int) : Int :=
-/ -/
def frictionFactor (re : Int) : Option Int := def frictionFactor (re : Int) : Option Int :=
if re < RE_LAMINAR then if re < RE_LAMINAR then
-- Laminar: f = 64/Re (Blasius laminar) in Q16.16: (64 * SCALE) / Re -- Laminar: f = 64/Re (Hagen-Poiseuille) in Q16.16: (64 * SCALE) / Re
-- q16_div multiplies numerator by SCALE internally, so pass 64 -- q16_div multiplies numerator by SCALE internally, so pass 64
q16_div 64 re q16_div 64 re
else if re > RE_TURBULENT then else if re > RE_TURBULENT then