canonicalThreshold
plain-language theorem explainer
Defines the real number φ − 3/2 as the module’s canonical threshold scale. Anyone citing the 3D Anderson localization-from-J-cost structural package uses this constant as the fixed comparison value against domain cost. The body is a one-line definitional equality; no proof obligations.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden-ratio fixed point of the Recognition self-similarity relation.
background
The ambient module treats the 3D Anderson localization–delocalization transition as forced by the Recognition J-cost. In RS units the critical disorder sits near $W_c \sim J(\varphi)^{-1}$ times the bandwidth energy scale (numerically about $8.47$ in the stated units). The golden ratio $\varphi$ is the unique self-similar fixed point fixed earlier in the forcing chain (T6).
J-cost itself is the unique nonnegative cost satisfying the Recognition Composition Law; on the positive reals it is $J(x)=(x+x^{-1})/2-1$. Domain cost in this file is the restriction of that cost to the lattice/disorder setting used for the Anderson certificate. The present constant simply freezes a concrete real comparison point built from $\varphi$ and the rational $3/2$.
proof idea
Pure definition: the identifier is bound to the real expression $\varphi - 3/2$. No tactics, no lemmas, no sorry. Downstream positivity or comparison lemmas (e.g. the sibling that asserts the threshold is positive) unfold this equality and finish by arithmetic on $\varphi$.
why it matters
Gives the Anderson-from-J-cost package a single named real against which domain cost is compared when building the structural certificate (siblings such as the inhabited AndersonLoc4Cert). It sits inside the broader RS claim that the 3D localization transition is fixed by J-cost scales rather than by free phenomenological parameters, consistent with the forcing landmarks that already fix $\varphi$ (T6) and $D=3$ (T8). It does not itself derive the numerical factor $8.47$; that comes from evaluating $J(\varphi)^{-1}$ against bandwidth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.