Pith. sign in
def

canonicalThreshold

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

plain-language theorem explainer

The canonical threshold is the real constant φ − 3/2 built from the golden-ratio fixed point. It is the comparison level used in the RS structural count-law module that encodes the seven independent channels forced by D = 3. Anyone working the mathematics layer of the count law or domain-cost inequalities cites it as the fixed cutoff. The declaration is a one-line arithmetic definition in the RS constant φ.

Claim. Define the canonical threshold by $T := \varphi - \tfrac{3}{2}$, where $\varphi$ is the golden-ratio self-similar fixed point of Recognition Science.

background

This module records the RS count law: with spatial dimension $D = 3$ one has $2^D - 1 = 7$ independent channels, treated as an exact structural identity (zero sorry, zero axiom). The constant $\varphi$ is imported from the RS Constants layer; by the forcing chain it is the unique self-similar fixed point (T6) of the cost calculus whose unique generator is the J-cost $J(x) = (x + x^{-1})/2 - 1$.

Domain costs live in the Cost import and are nonnegative real-valued functionals on the configuration side of the count law. The threshold $T = \varphi - 3/2$ sits slightly above zero ($\varphi \approx 1.618$), so it is a natural positive cutoff against which those costs can be compared inside the same module.

proof idea

Pure definition: the symbol is bound to the real expression $\varphi - 3/2$. No lemma applications, no tactics, no proof obligations.

why it matters

The declaration supplies the numerical cutoff that the rest of RS_MTH_Structural_003 uses when it talks about domain costs relative to the seven-channel count law. It sits next to the positivity fact for the same constant and the module certificate that packages the structural theorem. Framework-wise it inherits $\varphi$ from T6 and the channel count $2^D-1=7$ from T8 ($D=3$), so the threshold is not an arbitrary real but a combination of forced RS landmarks. No open scaffold is attached; the module is already marked structural with zero sorry.

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