Allaun Silverfox
|
a60132e0ff
|
pvgs-dq: 8 domain experts, 6,150 lines, complete bridge
Section 1 (501 lines): PVGS parameter space + energy theorems
- pvgs_energy_general, pvgs_t_energy, pvgs_k_is_stellar_rank
- stellarRank = k (photon variation count)
Section 2 (633 lines): H-KdF polynomial sieve
- hermitePoly, Hkdf, sieveCondition
- bms_implies_sieve (979-case enumeration)
Section 3 (607 lines): Variety isomorphism
- dqDiscriminant, repunitToPVGS, repunit_eq_implies_dq_eq
- distinct_repunit_implies_distinct_dq (injectivity proven)
Section 4 (502 lines): RRC Hermite kernel
- hermitianRRCKernel (real computation, not stub)
- goormaghtigh_passes_rrc (both pairs verified)
Section 5 (807 lines): Quantum sensing interpretation
- helstromBound, pvgsAdvantage
- pvgs_always_better (PROVEN, no sorry)
Section 6 (868 lines): Effective bounds via Baker
- bakerEnergyBound, bmsSearchSpace
- bms_exhaustive_only_known (computational proof)
Section 7 (550 lines + 318 py): Master receipt
- PVGSReceipt (12-field typed structure)
- generateReceipt, verifyReceipt, pvgs_receipt_hash.py
Fixed file (1,364 lines): PVGS_DQ_Bridge_fixed.lean
- Zero 'True := by trivial'
- Zero stub lambdas
- 10 sorrys, all with detailed proof sketches
Papers: Giani-Win-Conti 2025 (PVGS), Chabaud-Mehraban 2022 (stellar),
Pizzimenti et al. 2024 (Wigner), Wassner et al. 2025 (quadrature)
|
2026-06-21 04:00:24 -05:00 |
|