allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-30 17:16:16 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
SilverSight/formal
History
Exact
allaun c3a5e6b60b fix(lean): remove dead code hp_sq_ne_zero in C_finite_zero_eq_one 
Leftover from a previous proof iteration. The hx block proves nonzeroness via positivity arguments alone.
2026-07-07 09:19:13 -05:00
..
BindingSite tag(axioms): justify all 18 custom axioms with HONESTY CLASS tags 2026-07-03 10:54:08 +00:00
CoreFormalism feat(lean): phiInvQ16_mul_strict_lt_pos — proven strict contraction lemma 2026-07-07 02:24:26 -05:00
RRCLib feat(rrc): bare-minimum RRC refactor into SilverSight 2026-06-21 09:08:48 -05:00
SilverSight fix(lean): remove dead code hp_sq_ne_zero in C_finite_zero_eq_one 2026-07-07 09:19:13 -05:00