canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold in the Recognition Lattice is positive. This follows from its definition as the golden ratio minus three halves combined with the bound that the golden ratio exceeds 1.5. Lattice certification proofs cite this result to establish the threshold lies above zero. The argument is a direct unfolding followed by linear arithmetic.
Claim. $0 < phi - 3/2$ where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
The RecognitionLattice3 module builds a lattice on integer powers of the golden ratio phi, taking absolute J-cost values as rung distances. The ground state is at rung zero with J-cost zero; the first excited rung sits at k=1. The canonical threshold is defined as phi minus 3/2 and serves as the positivity marker required for lattice certification records.
proof idea
The proof is a one-line wrapper that unfolds the definition of canonicalThreshold to phi minus 3/2. It then applies the linarith tactic with the phi_gt_onePointFive lemma to obtain the strict inequality.
why it matters
This theorem supplies the threshold positivity fact required by the cert definition in the same module, which constructs the RecogLattice3Cert record. The identical pattern appears in the muon g-2 module for its certification. It closes a basic positivity check in the J-cost lattice construction, consistent with the self-similar fixed point property of phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.