[L-S37] PhiPriorQuantCorrect: Coq formal proof of phi-prior weight quantizer correctness

[gHashTag]

Tracking Issue: L-S37 φ-prior Quantizer Formal Proof

Objective

Provide a Coq formal proof of correctness for the L-S37 φ-prior on-chip weight quantizer (FP Q1.15 → ternary).

Theorems to prove

1. Ternary completeness: forall w, quantize w = +1 \/ quantize w = 0 \/ quantize w = -1
2. Zero region: forall w, |w| < phi_inv_sq -> quantize w = 0

Location

docs/phd/theorems/igla/PhiPriorQuantCorrect.v

Acceptance criteria

• coqc PhiPriorQuantCorrect.v exits 0
• All proofs end Qed. (not Admitted.)
• Apache-2.0

Anchor

φ² + φ⁻² = 3 ; φ⁻² (Q1.15) = 12533 ; DOI: 10.5281/zenodo.19227877