Pith. sign in
def

canonicalThreshold

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

plain-language theorem explainer

Defines the canonical astrophysical threshold as φ − 3/2 in RS-native units. Anyone comparing domain costs or positivity bounds in the solar-surface module cites this constant. The body is a one-line real abbreviation of the golden ratio minus three halves.

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

background

Recognition Science forces the dimensionless scale $\varphi$ as the unique self-similar fixed point of the cost functional (forcing step T6). In RS-native units the same $\varphi$ generates the mass ladder, the eight-tick period, and the numerical constants $c=1$, $\hbar=\varphi^{-5}$.

This module (Astrophysics RS Module 1) records the exact solar-surface temperature match $\varphi^{18},\mathrm{K}=5778,\mathrm{K}$. The local cost infrastructure imports the global $J$-cost and the constant $\varphi$ so that domain-level thresholds can be written without repeating the arithmetic.

canonicalThreshold simply packages the combination $\varphi-3/2$ that later positivity and comparison lemmas treat as the reference scale for those domain costs.

proof idea

Pure definitional abbreviation: the real constant is declared equal to $\varphi-3/2$. No tactics, no lemmas, no proof obligations.

why it matters

Supplies the numerical yardstick against which the module’s domain-cost predicates are measured. Sibling lemmas (positivity of the threshold, non-negativity of domain cost, the inhabited certificate RSAstro001Cert) all read this constant. In the broader RS chain it sits downstream of T6 ($\varphi$ uniqueness) and upstream of the exact solar-temperature claim that the module advertises as a structural theorem with zero sorry. It does not itself derive the solar match; it only freezes the comparison scale used by those later statements.

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