canonicalThreshold
plain-language theorem explainer
Defines the real number φ − 3/2 as the canonical cost threshold in the proton-radius-from-J-cost development. Anyone citing the structural proton-radius certificate or domain-cost comparisons will use this constant. The body is a one-line arithmetic definition from the golden ratio.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden-ratio fixed point of the Recognition self-similarity relation.
background
The module aims at a structural account of the proton charge radius on the φ-ladder, using the J-cost of Recognition Science rather than a fitted length. Status is a structural theorem with no sorry and no extra axioms.
Here φ is the unique self-similar fixed point forced by the Recognition Composition Law (T6 in the forcing chain). The cost side of the story comes from the imported Cost layer: domain cost is a non-negative real functional built from J, and thresholds on that cost mark when a geometric or spectral feature is recognized.
The constant 3/2 is the natural half-integer offset once spatial dimension D = 3 (T8) enters the ladder counting; subtracting it from φ yields a small positive scale against which domain cost is compared.
proof idea
Pure definition: unfold to the real expression φ − 3/2. No lemmas, no tactics. Downstream positivity or comparison facts (e.g. the sibling that the threshold is positive) are separate theorems.
why it matters
Gives a single named scale for every domain-cost comparison in the proton-radius certificate. The module frames the proton radius as a structural consequence of J-cost on the φ-ladder in D = 3, not a free fit; this threshold is the cut that makes those comparisons canonical.
It sits next to domainCost, domainCost_nonneg, and the ProtonRadius3Cert package. Framework landmarks in play are T6 (φ forced) and T8 (D = 3), together with the J-cost uniqueness from T5. No open scaffold remains in this definition itself; it is closed arithmetic used by the surrounding structural claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.