Pith. sign in
module module moderate

IndisputableMonolith.Physics.SolarConstantFromPhiLadder

show as:
view Lean formalization →

Packages a Recognition Science account of the solar constant on the phi-ladder. Introduces a domain cost, a positive canonical threshold, and an inhabited SolarConstantCert bundling them. Observers checking RS irradiance predictions against the ladder would cite the certificate. The module is definitional bookkeeping with nonnegativity and positivity lemmas, not a deep forcing proof.

claimDefines a domain cost $C$, equality and nonnegativity facts for $C$, a canonical threshold $\theta>0$, and an inhabited certificate that the solar constant is the $\varphi$-ladder evaluation of $C$ against $\theta$ in RS-native units.

background

Recognition Science places dimensionful quantities on a discrete $\varphi$-ladder fixed by the self-similar point of the $J$-cost (forcing step T6). Particle masses use the yardstick form $\mathrm{yardstick}\cdot\varphi^{r\mathrm{-}8+\mathrm{gap}(Z)}$; the same ladder is the natural home for macroscopic fluxes once units are RS-native ($c=1$, $\hbar=\varphi^{-5}$, etc.).

The solar constant is the mean solar electromagnetic irradiance at 1 AU. This module treats it as a ladder-derived claim rather than a pure empirical input. It imports the Constants layer (fundamental tick $\tau_0$) and the Cost layer ($J$-cost and related functionals), then introduces a domain cost, a canonical threshold, and a certificate object that packages the claim.

proof idea

Definition-and-certificate module, not a deep proof chain. It defines the domain cost, records an evaluation identity and nonnegativity, fixes a strictly positive canonical threshold, and assembles these into SolarConstantCert with an inhabitation witness. Supporting lemmas are short algebraic or positivity facts; there is no appeal here to the T0-T8 forcing spine beyond the ambient $\varphi$-ladder.

why it matters in Recognition Science

Gives the physics layer a named, inhabitable certificate that the solar constant sits on the same $\varphi$-ladder used for masses and couplings. The graph currently lists no downstream consumers, so the certificate is a leaf ready for observational or units-conversion clients. It ties the irradiance claim to T6 ($\varphi$ uniqueness) and the RS-native constant set, without reopening the Recognition Composition Law or the eight-tick octave.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)