planck_mass_eq
plain-language theorem explainer
Physicists deriving mass scales from the Recognition Science phi-ladder cite the equality of the RS Planck mass to φ^{-5}. This follows directly from substituting the RS-native values of ℏ, c, and G into the standard Planck mass formula and simplifying the resulting square root. The tactic proof applies field simplification and the square root identity for positive reals.
Claim. In RS-native units with c = 1, ℏ = φ^{-5}, and G = φ^5, the Planck mass defined by m_P = √(ℏ c / G) satisfies m_P = φ^{-5}.
background
Recognition Science derives physical constants from the functional equation for the J-cost, J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), whose unique solution is J(x) = (x + x^{-1})/2 - 1. The self-similar fixed point forces φ = (1 + √5)/2, and the eight-tick octave forces three spatial dimensions. In this setting the module derives c = 1, ℏ = φ^{-5}, G = φ^5 (RS-native units).
proof idea
The proof introduces the equalities ℏ_rs = φ^{-5} from ℏ_rs_eq, c_rs = 1 from c_rs_eq_one, and G_rs = φ^5 by reflexivity. It substitutes these into planck_mass_rs and applies simp. Then it proves φ^{-5}/φ^5 = φ^{-10} using field_simp with positivity lemmas pow_pos. It rewrites the power -10 as the square of power -5 via zpow_mul, and concludes with sqrt_sq on the positive quantity zpow_pos phi_pos (-5).
why it matters
This result completes the derivation of the Planck mass within the ConstantDerivations module, which traces all constants back to the J-cost and the forced value of φ. It supplies the fundamental mass unit for the phi-ladder constructions used in nucleosynthesis tiers and large-scale structure scaling. The framework landmark is the reduction of all dimensionful constants to powers of φ once c=1 and the IR gate ℏ=φ^{-5} are fixed by the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.