allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
SilverSight/formal
History
Exact
allaun 1eb7a0d924 fix(lean): Resolve CartanConnection sorries with integer bypass and correct lemma names 
- Add C_int integer version for Jacobiator proof
- Add integer bypass with D=1792 scaling
- Fix mu_scale proof using Finset.sum_div instead of mul_div_assoc
- Fix Jacobiator_basis_all using ext pattern instead of eq_empty_iff_forall_not_mem
- Update proof strategy documentation

Build: lake build SilverSight (pending)
2026-06-27 14:46:21 -05:00
..
BindingSite chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00
CoreFormalism chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00
PVGS_DQ_Bridge chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00
RRCLib feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
SilverSight fix(lean): Resolve CartanConnection sorries with integer bypass and correct lemma names 2026-06-27 14:46:21 -05:00
UniversalEncoding chore(quality): native_decide migration, docs, and phi pipeline cleanup 2026-06-27 01:56:54 -05:00