canonicalThreshold_pos
plain-language theorem explainer
The positivity of the canonical threshold, defined as the golden ratio minus 1.5, follows from the established lower bound on phi. Lattice modelers in Recognition Science cite this when confirming that cost functions remain non-negative above the threshold in lattice models. The proof is a one-line wrapper that unfolds the definition and applies linear arithmetic to the phi inequality.
Claim. $0 < phi - 3/2$, where $phi = (1 + sqrt(5))/2$ is the golden ratio.
background
In the Recognition Lattice framework the canonical threshold is defined as phi minus three halves to mark the boundary separating positive and non-positive cost domains. The module Muon g-2 from J-Cost imports this definition together with domainCost functions to build structural certificates for the muon anomaly. Upstream the lemma phi_gt_onePointFive supplies the tighter bound 1.5 < phi that drives the positivity argument.
proof idea
This is a one-line wrapper. It unfolds canonicalThreshold to phi - 3/2 and then invokes linarith on the hypothesis phi_gt_onePointFive.
why it matters
The result supplies the threshold_pos field required by both RecogLattice3Cert and Muong23Cert, closing the basic positivity check that lets the certificates be inhabited. It sits inside the structural theorem block of the muon g-2 module, which the module doc describes as a placeholder pending refinement of the J-cost scaling factor. The construction aligns with the Recognition Science forcing chain that forces D = 3 and the eight-tick octave once the lattice is certified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.