allaun 8bed931037 feat(lean): BlockCoprimeDensity — C(n) block-coprime density Euler product ... Formalizes the Euler product for the natural density of (r, M) pairs satisfying gcd(r, M+j) = 1 for all j = 0..n: C(n) = ζ(2) · ∏_p (1 − min(n+1, p) / p²) Key theorems: - localFactor_saturated / localFactor_active (saturation partition) - C_finite_zero_eq_one (C_G(0) = 1 for any G, ζ(2) identity) - D_finite_zero_eq, D_finite_one_eq (Feller-Tornier product) All 5 #eval witnesses verified. 0 sorries. Build: 3297 jobs, 0 errors (lake build SilverSight.BlockCoprimeDensity)		2026-07-07 02:24:26 -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	feat(lean): BlockCoprimeDensity — C(n) block-coprime density Euler product	2026-07-07 02:24:26 -05:00