Pith. sign in
def

canonicalThreshold

definition
show as:
module
IndisputableMonolith.Foundation.RS_FDN_Structural_010
domain
Foundation
line
20 · github
papers citing
none yet

plain-language theorem explainer

The canonical threshold is the fixed real scale φ − 3/2, with φ the golden ratio. Structural calibration and domain-cost arguments in the Recognition foundation cite it as the comparison level against which costs are measured. The declaration is a one-line definitional abbreviation with no proof obligations.

Claim. Define the canonical threshold by $T_{\mathrm{can}} := \varphi - 3/2 \in \mathbb{R}$, where $\varphi$ is the golden ratio.

background

Module RS_FDN_Structural_010 is a structural foundation file: E_coh is fixed once from the electron mass, after which predictions are parameter-free, with status claimed as a structural theorem (no sorry, no axioms).

The constant $\varphi$ is imported from IndisputableMonolith.Constants; in the forcing chain it is the unique self-similar fixed point (T6). The Cost import supplies the J-cost and related nonnegativity infrastructure used by sibling lemmas that compare domain costs to a fixed real level.

Numerically $\varphi \approx 1.618$, so $\varphi - 3/2 \approx 0.118 > 0$. That positivity is not part of this definition; it is stated separately.

proof idea

Definitional. The body is the single real expression $\varphi - 3/2$; there is no tactic proof, no lemma application, and no hypothesis to discharge.

why it matters

Gives a named, reusable real scale for structural cost comparisons in the foundation layer. Sibling results (positivity of the threshold, domain-cost nonnegativity and evaluation lemmas, and the module certificate) sit next to it and treat this value as the canonical cutoff.

In the broader Recognition picture it is a calibration constant in RS-native units once $\varphi$ is forced, consistent with the module claim that E_coh is set once and the rest is parameter-free. It does not itself invoke the RCL, the eight-tick octave, or the mass ladder; those enter only if downstream cost or mass arguments import this scale.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.