allaun 7f0d199289 feat(lean): Layer 2d Yang-Baxter integrability (rfl, no native_decide) ... R = B⊗B satisfies R12 R13 R23 = R23 R13 R12 on Q^2 x Q^2 x Q^2. Sidon crossing block B = [[39/256, 1/7], [1/7, 39/256]]. Proof is by alpha-equivalence (rfl) — both sides differ only by renaming bound variable r→s. No native_decide needed. Previous derivation used wrong YB equation form ((R⊗I)(I⊗R)(R⊗I) vs (I⊗R)(R⊗I)(I⊗R)) which had 32/64 false. Correct form (R12 R13 R23) verified 0 violations via Python. Build: 3335/3336 jobs, 0 errors (lake build SilverSightRRC)		2026-06-27 01:18:10 -05:00
..
BindingSite	fix: ChentsovFinite rewritten with adversarial-reviewed proof structure	2026-06-23 15:57:02 -05:00
CoreFormalism	fix(chentsov): Remove sorry placeholder from axiom parameters	2026-06-26 00:00:35 -05:00
PVGS_DQ_Bridge	fix: Hkdf formula now uses (α*β)^(m+n+1) denominator; zero sorries	2026-06-23 11:42:16 -05:00
RRCLib	feat(rrc): bare-minimum RRC refactor into SilverSight	2026-06-21 09:08:48 -05:00
SilverSight	feat(lean): Layer 2d Yang-Baxter integrability (rfl, no native_decide)	2026-06-27 01:18:10 -05:00
UniversalEncoding	Fix: resolve sorrys across PVGS, UniversalEncoding, ChiralitySpace, QAOA	2026-06-21 05:35:53 -05:00