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

all_constants_from_phi

show as:
view Lean formalization →

Recognition Science fixes the speed of light, reduced Planck constant, gravitational constant and Planck length as algebraic expressions in the golden ratio phi within its native units. A physicist deriving the constant sector from the composition law would cite this result to eliminate free parameters. The proof is a one-line constructor that assembles five prior lemmas on each component.

claimIn RS-native units, $c = 1$, there exists an integer $n$ such that $h = phi^n$, there exists an integer $m$ such that $G = phi^m$, $G h = 1$, and the Planck length equals 1.

background

The module derives physical constants from the Recognition Science foundation. The composition law forces the unique cost J(x) = (x + x^{-1})/2 - 1. Self-similarity fixes phi as the golden ratio. The eight-tick octave then requires three spatial dimensions, yielding fundamental scales tau_0 = 1 tick and ell_0 = 1 with coherence energy phi^{-5}. Constants appear as ratios of these scales. Upstream results include the definition of G_rs as phi^5 and the tick as the unit time quantum.

proof idea

The proof is a one-line wrapper that applies the conjunction of c_rs_eq_one, ℏ_algebraic_in_φ, G_algebraic_in_φ, G_ℏ_product and planck_length_eq_one. These lemmas are established earlier in the module from the phi-ladder and the forcing chain.

why it matters in Recognition Science

This result closes the constant sector by showing every fundamental constant is algebraic in phi, which is forced by J-uniqueness and the self-similar fixed point. It supports the claim that the entire physics follows from the composition law with no free parameters. The module narrative links it to the eight-tick cycle forcing D = 3 and the mass formula on the phi-ladder.

scope and limits

formal statement (Lean)

 270theorem all_constants_from_phi :
 271    -- c = 1
 272    c_rs = 1 ∧
 273    -- ℏ = φ^(-5)
 274    (∃ n : ℤ, ℏ_rs = φ_val^n) ∧
 275    -- G = φ^5
 276    (∃ n : ℤ, G_rs = φ_val^n) ∧
 277    -- G × ℏ = 1
 278    G_rs * ℏ_rs = 1 ∧
 279    -- Planck length = 1
 280    planck_length_rs = 1 :=

proof body

Tactic-mode proof.

 281  ⟨c_rs_eq_one, ℏ_algebraic_in_φ, G_algebraic_in_φ, G_ℏ_product, planck_length_eq_one⟩
 282
 283/-! ## The Derivation Narrative -/
 284
 285/-- **THE CONSTANT DERIVATION NARRATIVE**
 286
 287    1. The composition law (d'Alembert) is the foundation.
 288    2. It uniquely determines J(x) = ½(x + 1/x) - 1.
 289    3. Self-similarity under J forces φ = (1+√5)/2.
 290    4. The eight-tick cycle (2^D = 8) forces D = 3.
 291    5. These determine the fundamental scales:
 292       - τ₀ = 1 (fundamental tick)
 293       - ℓ₀ = 1 (fundamental length)
 294       - E_coh = φ^(-5) (coherence quantum)
 295    6. The constants follow:
 296       - c = ℓ₀/τ₀ = 1
 297       - ℏ = E_coh · τ₀ = φ^(-5)
 298       - G = φ^5 (curvature extremum)
 299       - α ≈ 1/137 (geometric + gap-45)
 300
 301    **No free parameters.** The entire constant sector is determined
 302    by the composition law. -/

depends on (25)

Lean names referenced from this declaration's body.