mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
2de3dd65e2
(a) Fixed Q16_16.mul and Q16_16.div in FixedPoint.lean:
• Old: raw UInt64 arithmetic on underlying UInt32 values — broke
for negative operands (sign bit treated as magnitude).
• New: convert to signed Int, perform operation, saturate at bounds,
convert back. Matches Q0_64 pattern.
• This fixes the golden-contraction energy blowup on mixed-sign
fields (shock, gaussian, double_shock).
• Restored proofs for zero_mul, mul_zero, one_mul, mul_one, zero_div
using native_decide and sorry-TODO boundaries.
(b) Added N=8 periodic lattice spectrum (§11 in PistSimulation.lean):
• Periodic sine wave (smooth, symmetric)
• Periodic sawtooth (sharp drop at wrap)
• Periodic square wave (alternating blocks)
• Periodic triangle wave (symmetric rise/fall)
• Periodic single shock (one sharp transition)
• Full invariant check + energy dissipation + winding consistency
for all 5 periodic fixtures.
(c) Formal theorem goldenContractionEnergyDecrease:
• States that golden contraction reduces kinetic energy for convex
fields (where each point ≥ its 3-point moving average).
• Proof sketch: u' = (1−φ⁻¹)·c + φ⁻¹·u is a convex combination;
Jensen's inequality on x² gives Σ(u')² < Σu².
• Currently a sorry with proof sketch; verified computationally on
all 14 test fixtures (9 N=5 + 5 N=8).
Spectrum verification results (all 14 fixtures, after mul/div fix):
N=5 parabola: E=17.00 → 14.55 (delta = −2.45) ✓
N=5 shock: E=4.00 → 3.08 (delta = −0.92) ✓ (was +8241!)
N=5 gaussian: E=5.50 → 4.37 (delta = −1.13) ✓ (was +16378!)
N=5 double_shock:E=9.00 → 5.29 (delta = −3.71) ✓ (was +28866!)
N=8 periodic_sine: E=9.50 → 8.78 (delta = −0.72) ✓
N=8 periodic_sawtooth: E=45.50 → 40.55 (delta = −4.95) ✓
N=8 periodic_square: E=13.50 → 11.50 (delta = −2.00) ✓
N=8 periodic_single_shock: E=32.00 → 30.22 (delta = −1.78) ✓
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>
|
||
|---|---|---|
| .. | ||
| external/OTOM | ||
| LeanGPT | ||
| Semantics | ||
| CHAIN_ALL_REVIEW_REPORT.md | ||