Research-Stack/0-Core-Formalism/lean
Brandon Schneider 791dd55d4f feat(lean): spectrum invariant verification harness for Burgers-PhiNUVMAP bridge
Comprehensive §10 test suite running the bridge across 9 initial conditions
and verifying against known invariants:

Test fixtures:
  • smooth parabola (convex, all diffs ≥ 0)
  • shock step (mixed-sign diffs)
  • sinusoidal (convex, same as parabola)
  • rarefaction wave (linear, identity under contraction)
  • asymmetric ramp (linear, non-zero winding)
  • gaussian bump (mixed-sign diffs)
  • zero field (trivial, identity)
  • constant field (linear, identity)
  • double shock (mixed-sign diffs)

Invariant checks:
  • Regime classification via spectral discriminant gate
  • Kinetic energy of initial state (non-negative)
  • Golden-contraction energy dissipation (convex/linear fields)
  • Spatial & temporal winding numbers (physically consistent)
  • CFL-like stability proxy

Key finding: Q16_16.mul/div use raw UInt64 arithmetic on the underlying
UInt32 values, which produces incorrect results for negative operands
(the sign bit is treated as magnitude).  This affects fields where the
golden contraction has negative local deviations (u−c < 0).  Working
cases (convex/linear fields where all u−c ≥ 0) verify correctly:
  – Parabola: E=17.0 → 14.55 (delta = −2.45)  ✓
  – Linear fields: identity contraction (delta = 0)  ✓
  – Zero field: identity (delta = 0)  ✓

Build: lake build Semantics green at 3541 jobs.

Generated with [Devin](https://cli.devin.ai/docs)

Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
2026-05-21 01:26:00 -05:00
..
external/OTOM Refactor provenance sources for open witness backends 2026-05-12 05:57:04 -05:00
LeanGPT Remove legacy Python prototypes superseded by Lean formalization 2026-05-19 15:34:17 +00:00
Semantics feat(lean): spectrum invariant verification harness for Burgers-PhiNUVMAP bridge 2026-05-21 01:26:00 -05:00
CHAIN_ALL_REVIEW_REPORT.md initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00