Pith. sign in
def

canonicalThreshold

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

plain-language theorem explainer

Defines the canonical real threshold φ − 3/2 used in the RS gravity structural layer. Gravity and lattice-cost arguments cite it as the fixed cutoff separating subcritical from supercritical domain cost. It is a one-line constant definition in terms of the golden ratio.

Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio fixed by self-similarity.

background

Recognition Science forces the golden ratio $\varphi$ as the unique self-similar fixed point (forcing step T6). The same chain forces the eight-tick octave: period $2^D = 8$ with $D = 3$ spatial dimensions (T7–T8), i.e. one complete traversal of the binary recognition lattice.

This module packages structural gravity facts that sit on that lattice. Domain cost is the non-negative cost functional pulled back to the recognition domain; thresholds on that cost decide when a configuration is admissible. The constant $\varphi - 3/2$ is the canonical numerical cut used by those comparisons.

Imports bring in Constants (for $\varphi$) and Cost (for the underlying J-cost and related inequalities).

proof idea

Pure definition: the real constant is introduced by the arithmetic expression $\varphi - 3/2$. No proof obligations; positivity and downstream comparisons are handled by sibling lemmas.

why it matters

Supplies the fixed numerical gate for RS gravity structural certificates in this module (siblings such as positivity of the threshold and the inhabited certificate). It ties the gravity layer to the forced value of $\varphi$ and to the eight-tick lattice period $2^3 = 8$. Without a single shared cutoff, domain-cost comparisons would be ad hoc; this definition locks the cut to the same $\varphi$ that appears in the mass ladder, $\hbar$, and $G$.

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