canonicalThreshold
plain-language theorem explainer
The definition assigns the real number phi minus three halves to the canonical threshold, which equals the J-cost function evaluated at the golden ratio. Physicists constructing lattice certificates for the muon anomalous magnetic moment cite this scale when verifying domain cost non-negativity. It arises by direct definition with no lemmas or reduction steps.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$ denote the recognition cost function and let $phi$ be the golden ratio. The canonical threshold is defined as $phi - 3/2$, which equals $J(phi)$.
background
Recognition Science introduces the J-cost $J(x) = (x + x^{-1})/2 - 1$, equivalently $cosh(log x) - 1$, together with the golden ratio $phi$ as the unique positive self-similar fixed point. The module adapts this threshold from the RecognitionLattice3 foundation to define domain costs for the muon g-2 anomaly calculation. The module doc presents the setting as a structural placeholder: the predicted $Delta a_mu = J(phi) alpha / (2 pi)$ exceeds the experimental discrepancy by a factor of roughly 100.
proof idea
The declaration is a direct definition that equates canonicalThreshold to the arithmetic expression phi minus three halves. No lemmas are invoked and no tactics are applied.
why it matters
The definition supplies the numerical value $J(phi) approx 0.118$ that populates the threshold_pos field inside both RecogLattice3Cert and Muong23Cert. It realizes the T6 forcing step in which phi is fixed as the self-similar point of the eight-tick octave. The module doc explicitly flags the construction as a placeholder, leaving open the reconciliation of the predicted anomaly magnitude with the measured 25.1 pm 5.9 times 10 to the minus 10.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.