Allaun Silverfox f69d7e84af Fix: resolve sorrys across PVGS, UniversalEncoding, ChiralitySpace, QAOA ... - 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		2026-06-21 05:35:53 -05:00
..
ChiralitySpace.lean	Fix: resolve sorrys across PVGS, UniversalEncoding, ChiralitySpace, QAOA	2026-06-21 05:35:53 -05:00
UniversalMathEncoding.lean	Fix: resolve sorrys across PVGS, UniversalEncoding, ChiralitySpace, QAOA	2026-06-21 05:35:53 -05:00