canonicalThreshold
plain-language theorem explainer
The definition sets the canonical threshold equal to the golden ratio minus three halves. Lattice researchers cite this cutoff when certifying that J-cost vanishes only on the diagonal and remains nonnegative elsewhere. The declaration is a direct algebraic substitution of the imported golden-ratio constant.
Claim. The canonical threshold is defined by the expression $phi - 3/2$, where $phi$ denotes the golden ratio fixed point of the self-similar map.
background
The Recognition Lattice consists of the discrete set of powers $phi^k$ for integer $k$, equipped with the J-cost metric whose distance between rungs $k$ and $j$ is the absolute value of $J(phi^{k-j})$. The ground state lies at rung zero where the cost is identically zero; the first excited rung sits at $k=1$. This module imports the same numerical threshold already introduced in the muon $g-2$ derivation from J-cost, ensuring the foundation and physics layers share a common cutoff value.
proof idea
The declaration is a direct definition that substitutes the golden-ratio constant and performs the indicated subtraction. No lemmas or tactics are invoked beyond the imported definition of $phi$.
why it matters
The value is required by the RecogLattice3Cert structure, which packages the three lattice axioms (cost vanishes at equality, cost is nonnegative, and the threshold is positive). The same field appears in the Muong23Cert structure used for the muon anomalous moment certification. Within the Recognition framework the threshold supplies the concrete separation between the ground state and the first rung of the $phi$-ladder, consistent with the eight-tick octave and the forced value of $phi$ at step T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.