allaun db39e2c068 feat: Rollup circulant-block compression theorem + YangMillsPerformance bound ... Rollup.lean: proves DFT-based 2-mul per circulant block product (total 8 muls for 4-block 8x8 crossing matrix). Includes dftMultiply, naiveMultiply, dftMatchesNaiveTest #eval! verification. YangMillsPerformance: compression_overhead_bounded now references Rollup.totalCrossingMultCost instead of uncomputable K(data). Build: 3302 jobs, 0 errors		2026-07-05 14:50:56 -05:00
..
BindingSite	tag(axioms): justify all 18 custom axioms with HONESTY CLASS tags	2026-07-03 10:54:08 +00:00
CoreFormalism	fix: agent-reviewed Lean fixes + reorganize rejected theories	2026-07-04 22:28:09 +00:00
RRCLib	feat(rrc): bare-minimum RRC refactor into SilverSight	2026-06-21 09:08:48 -05:00
SilverSight	feat: Rollup circulant-block compression theorem + YangMillsPerformance bound	2026-07-05 14:50:56 -05:00