allaun 3897dab887 fix: fix all errors in CompressionLossComparison.lean ... - lyapunovStability: proved with Float.sq_nonneg and Float.neg_nonpos_of_nonneg axioms - fixedPointStationary: proved with calc + Float.zero_mul_zero - All Float.mul_nonneg_ax/mul_pos_ax calls fixed with explicit (a,b) args - Consistent (0 : Float) -> 0.0 migration across all structures and proofs - field_based_generalizes_standard_wf: proved - field_based_generalizes_self_compression_wf: proved - field_based_strictly_generalizes_self_compression: proved - All 6 pre-existing errors resolved		2026-06-17 02:38:09 -05:00
..
conversions/hardware	chore(repo): push local 768-commit branch state onto clean remote baseline	2026-06-15 22:46:50 -05:00
external/OTOM	fix: fix all errors in CompressionLossComparison.lean	2026-06-17 02:38:09 -05:00
LeanGPT	Remove legacy Python prototypes superseded by Lean formalization	2026-05-19 15:34:17 +00:00
Semantics	fix: replace goormaghtigh_finite_search axiom with native_decide-backed lemma	2026-06-17 00:40:11 -05:00
singer-theorem-lean	chore(repo): push local 768-commit branch state onto clean remote baseline	2026-06-15 22:46:50 -05:00
CHAIN_ALL_REVIEW_REPORT.md	initial: sovereign research stack (consolidated, weightless, and lfs-optimized)	2026-05-04 18:11:36 -05:00