pith. machine review for the scientific record. sign in
theorem proved term proof high

solar_calibration

show as:
view Lean formalization →

The solar calibration theorem states that the luminosity scaling function returns exactly one when evaluated at unit solar mass. Stellar modelers anchoring mass-luminosity relations to solar observations would cite this result to fix the zero point of the L(M) curve. The proof is a one-line wrapper that unfolds the definition of luminosity scaling and applies simplification to the resulting power.

claimLet $L(M) = M^{3.9}$ denote the luminosity scaling for main-sequence stars. Then $L(1) = 1$.

background

The module derives main-sequence relations from Recognition Science by combining nuclear burning equilibrium with radiative transport and hydrostatic equilibrium. The key definition is luminosity scaling, given explicitly as the power law $L(M) = M^{3.9}$ that follows from Kramers opacity scaling as density times temperature to the minus 3.5 together with the pp-chain burning rate scaling as density times temperature to the fourth. The module document states that this yields the observed main-sequence $L$ proportional to $M^{3.9}$ relation and lists related results such as virial temperature scaling and main-sequence lifetime scaling as $M$ to the minus 2.9.

proof idea

The proof is a one-line wrapper. It unfolds the definition of luminosity scaling to obtain the expression $1^{3.9}$ and then applies simplification to reduce the power to the constant 1.

why it matters in Recognition Science

This theorem supplies the normalization point for the luminosity-mass scaling used throughout the stellar-evolution development. It directly implements the solar calibration step required by the paper RS_Stellar_Evolution_HR_Diagram.tex so that the derived $L$ proportional to $M^{3.9}$ relation passes through the observed solar values. The result sits inside the broader Recognition Science chain that obtains stellar properties from the J-cost functional and the eight-tick octave structure, though no downstream theorems in the current module depend on it.

scope and limits

formal statement (Lean)

  90theorem solar_calibration : luminosity_scaling 1 = 1 := by

proof body

Term-mode proof.

  91  unfold luminosity_scaling
  92  simp
  93
  94/-- More massive stars are much more luminous. -/

depends on (1)

Lean names referenced from this declaration's body.