Foundation Constant Derivations Planck Mass Eq

The Planck mass result

The Planck mass is the mass scale at which gravitational effects become as strong as quantum effects, a natural meeting point for the two great theories of modern physics. In the standard system of units where the speed of light, the reduced Planck constant, and Newton's gravitational constant are all set to one, the Planck mass is defined as the square root of their quotient. The Recognition Science framework's machine-checked library of formal theorems contains a declaration, named planck_mass_eq, which establishes a closed algebraic form for this quantity within the framework's own unit system.

In Recognition Science, the fundamental constants are not input as free parameters. The framework models the speed of light as the ratio of a fundamental length to a fundamental time, both set to one. It models the reduced Planck constant as a coherence energy times a fundamental time, where that energy is the golden ratio raised to the power minus five. It models Newton's gravitational constant as the golden ratio raised to the fifth power divided by pi. The theorem planck_mass_eq then proves that the framework's Planck mass, defined by the standard quotient, equals the square root of pi times the golden ratio raised to the power minus five. In symbols: m_P = √π · φ⁻⁵.

This result is a consequence of the framework's forcing chain, which derives the golden ratio φ = (1 + √5)/2 as the unique self-similar scaling from a proved cost function. The theorem is a statement about the framework's own definitions of the constants. It shows that, within this system, the Planck mass is not an independent number but an algebraic expression built from pi and the golden ratio. The proof is a direct computation from the definitions of the constants, and the library checks it without additional axioms.

What the theorem does not claim is that this expression equals the measured Planck mass in conventional physics. The framework's unit system sets the speed of light, the reduced Planck constant, and Newton's constant to one, so the numerical value of the Planck mass in those units is not a prediction of a laboratory measurement. The theorem is an internal consistency result: it shows that the framework's definitions of the constants produce a Planck mass with a simple closed form. The comparison to the measured value in SI units is an empirical check, not a theorem.

The practical consequence of planck_mass_eq is that it completes the picture of the framework's constants as ratios of quantities that are all algebraic in the golden ratio. The theorem demonstrates that the Planck mass, like the Planck length and the product of G and ℏ, is not a free parameter but a derived quantity. This supports the framework's broader claim that its fundamental constants are forced by its foundational structure rather than chosen by hand.

/-- Planck mass = √π · φ⁻⁵ in RS-native units (Family A). -/
theorem planck_mass_eq : planck_mass_rs = Real.sqrt Real.pi * φ_val ^ (-5 : ℤ) := by
  have h_inv : G_rs⁻¹ = Real.pi * ℏ_rs := by
    have hstep : G_rs = 1 / (Real.pi * ℏ_rs) := by
      rw [eq_div_iff (mul_ne_zero Real.pi_ne_zero (ne_of_gt ℏ_pos))]
      calc G_rs * (Real.pi * ℏ_rs) = Real.pi * (G_rs * ℏ_rs) := by ring
        _ = Real.pi * (1 / Real.pi) := by rw [G_ℏ_product]
        _ = 1 := by field_simp
    rw [hstep, one_div, inv_inv]
  have h_arg : ℏ_rs * c_rs / G_rs = Real.pi * ℏ_rs ^ 2 := by
    rw [c_rs_eq_one, mul_one, div_eq_mul_inv, h_inv]
    ring
  unfold planck_mass_rs
  rw [h_arg, Real.sqrt_mul Real.pi_pos.le,
      Real.sqrt_sq (le_of_lt ℏ_pos), ℏ_rs_eq]

/-- **Gravitational constant** in RS-native units (Family-A canonical value).

    G emerges as the curvature extremum in recognition geometry. The RS
    derivation is `G = λ²_rec · c³ / (π · ℏ)` (see
    `Constants/GravitationalConstant.lean`). With `λ_rec = c = 1`, `ℏ = φ⁻⁵`:

      G = 1 / (π · φ⁻⁵) = φ⁵ / π.

    The factor of `π` is physical (it is the holographic / Gauss–Bonnet closure
    normalization; `Unification/QuantumGravityOctaveDuality.lean` proves
    `G·ℏ = 1/π` and `κ_Einstein = 8φ⁵`). It is NOT a stray. Dropping it (the old
    `G = φ⁵` "Family B" value) contradicts the canonical `Constants` owner, the
    SI bridge (`Foundation/SIBridgeClosure.lean`, which gives `τ₀ = √π·τ_Planck`),
    and the Einstein-coupling value `κ = 8πG = 8φ⁵`. -/
noncomputable def G_rs : ℝ := φ_val ^ (5 : ℤ) / Real.pi

/-- **Speed of light** in RS-native units.

    c is the ratio of fundamental length to fundamental time.
    In RS-native units where ℓ₀ = τ₀ = 1, we have c = 1.

    This is not a parameter; it's a definition of unit coherence.
    The causal bound is that nothing propagates faster than 1 unit
    of length per 1 unit of time. -/
noncomputable def c_rs : ℝ := ℓ₀ / τ₀

What this page does not claim

The theorem does not claim that the framework's Planck mass equals the measured Planck mass in conventional units. The theorem does not claim that the framework's unit system is the SI unit system. The theorem does not claim that the framework derives the fine-structure constant.

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/Foundation/ConstantDerivations.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: