Pith. sign in
def

canonicalThreshold

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

plain-language theorem explainer

Defines the canonical materials threshold as the real number $\varphi-3/2$, where $\varphi$ is the RS self-similar fixed point. Materials and structural-certificate work in the eight-tick lattice cite this constant as the comparison level for domain cost. The body is a one-line abbreviation, not a derived identity.

Claim. The canonical threshold is the real constant $\varphi - 3/2$, with $\varphi$ the golden-ratio fixed point of Recognition Science.

background

This module sits in the materials layer of the Recognition Science monolith and is labeled a structural theorem package (zero sorry, zero axiom). Its local setting is the RS eight-tick: one full traversal of the binary recognition lattice with period $2^D=8$ (forcing step T7, $D=3$).

The constant $\varphi$ is imported from the Constants layer; by the forcing chain it is the unique self-similar fixed point forced at T6. The Cost import supplies the J-cost infrastructure against which domain costs are later compared. Sibling declarations name a nonnegative domain cost and assert positivity of this same threshold; the present declaration only fixes the numerical level.

proof idea

Pure definition. The right-hand side is the real expression $\varphi-3/2$; no lemma applications, tactics, or algebraic reductions appear.

why it matters

Gives a single named real that materials certificates can compare against domain cost without re-inlining $\varphi-3/2$. It sits next to the positivity lemma and the structural certificate inhabitation proofs in the same module, so any later claim that a domain cost clears the canonical level can point here. Framework-wise it is a materials-side constant in the eight-tick (T7) lattice, not a new forcing step; it does not itself re-derive $\varphi$ or the octave period.

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