Astrophysics Solar Radius Rs

The solar radius in RS

The solar radius is a measured quantity: the distance from the Sun's center to its photosphere, the visible surface. The standard value is about 6.96 × 10⁸ meters. In Recognition Science, the framework asks whether this measured length can be expressed as a power of the golden ratio φ ≈ 1.618, the number satisfying φ² = φ + 1. The research note in the module records a candidate: φ⁴³ ≈ 7.0 × 10⁸ meters, which lands within about 1 percent of the measured value. That comparison is a numerical observation, not a derived result.

What the module actually proves is narrower and fully general. It defines a cost function, a measure of mismatch between a measured quantity and a reference value, as J(m/e), where J(x) = (x + 1/x)/2 − 1. The machine-checked library of formal theorems proves three facts about this cost: it is zero when the two values are equal, it is never negative for positive inputs, and the threshold φ − 3/2 is positive. These are properties of the cost function itself, stated for any positive real numbers m and e. The module does not define what m and e mean for the Sun, so it proves nothing specific to the solar radius.

In plain language: the framework has a general tool for measuring how far one number is from another, and the tool behaves sensibly. But the solar radius page is a template shared with 2,383 sibling modules. It becomes a theorem about the Sun only when someone supplies a definition of m and e in the Sun's own terms, for example a physical model that identifies what the golden-ratio power is supposed to represent. Until then, the golden-ratio match is a research note, and the exact solar radius remains a measured fact, not a framework derivation.

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem cert_inhabited : Nonempty SolarRadiusCert := ⟨cert⟩

What this page does not claim

The framework derives the solar radius from first principles. The golden-ratio match φ^43 is a proved theorem. The template's general cost properties are specific to astrophysics.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Astrophysics/Solar_Radius_RS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: