mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
f69d7e84af
- PVGS_DQ_Bridge_fixed.lean: 8 of 10 sorrys proven * repunit_strictMono: StrictMono (repunit x) for x >= 2 (induction proof) * repunit_ge_7: geometric series lower bound * sieve_discriminates_correct: uses strictMono instead of sorry * hermite_sieve_isomorphism: 4 sorrys replaced with repunit_strictMono proofs * unknown_fails_rrc: converted to goormaghtigh_conjecture_axiom (BMS 2006) * pvgsToQS: added h_μre_nonneg, h_μim_nonneg fields to PVGSParams * 2 remaining sorrys documented (finite enumeration + near-collision bounds) - UniversalMathEncoding.lean: all 6 sorrys fixed * expressionToReceipt: implemented scanForTokens parser * addressChaosBasin: implemented with tokenGroupOfFin + sidonHash * address_injective: proved via Nat.testBit extensionality * chaosEmbedding.sparsity: full proof with phi lemma * embedding_injective: documented as axiom (Lindemann-Weierstrass) * addressWeight termination: Nat.div_lt_self + omega - ChiralitySpace.lean: all 4 sorrys fixed * consistent_count_lt_full: native_decide computational proof * expressionDirection/expressionPhase: tokenChiralityOfFin * isConsistent: Bool-returning with BEq deriving * All placeholder where functions implemented - qubo/qaoa_circuit.py: deterministic lowest-energy selection * simulate_qaoa_numpy: evaluates all states, picks minimum (not sampling) * Fixes approximation ratio = 1.0 for all 3 test equations Refs: Giani-Win-Conti 2025, Bugeaud-Mignotte-Siksek 2006 |
||
|---|---|---|
| .. | ||
| BindingSite | ||
| CoreFormalism | ||
| PVGS_DQ_Bridge | ||
| UniversalEncoding | ||