canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2 built from the golden ratio. Black-hole entropy and RS gravity workers cite it as the native cutoff that organizes the log-correction regime against the pure area law. It is introduced by a one-line definitional assignment, with no proof obligation.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden ratio (the self-similar fixed point of the Recognition forcing chain).
background
This module develops the black-hole entropy logarithmic correction from the Recognition Science J-cost. The module status line records a structural theorem (zero sorry, zero axiom) whose RS coefficient is $c_{\mathrm{RS}} = -\log(\varphi)/2 \approx -0.2406$, matching Sen's 2013 Kerr–Newman 4D value exactly and Falls–Litim 2014 asymptotic-safety numerics to three digits.
The golden ratio $\varphi$ is the forced self-similar fixed point (forcing step T6). The J-cost is the unique cost functional $J(x) = (x + x^{-1})/2 - 1$ fixed by the Recognition Composition Law and T5 uniqueness. Sibling definitions in the same file package a domain cost, its nonnegativity, and a certificate object for the log-correction claim; the present constant supplies the numerical threshold those objects refer to.
proof idea
Definitional one-liner: the name is bound to the real expression $\varphi - 3/2$. There is no tactic script, no lemma application, and no proof term beyond the equality that defines the abbreviation.
why it matters
Inside the BH-entropy log-correction development, this constant is the RS-native scale that separates regimes in the J-cost analysis. The parent structural result of the module asserts that the RS log coefficient equals $-\log(\varphi)/2$ and thereby reproduces the Sen and Falls–Litim values. The threshold sits downstream of the forcing-chain landmarks that fix $\varphi$ (T5 J-uniqueness, T6 self-similar fixed point) and upstream of the certificate objects (BHEntropyLog2Cert, cert) that package the structural theorem for export. It does not itself compute $c_{\mathrm{RS}}$; it only names the cutoff those arguments use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.