Constants

Scales set by the golden ratio

The constants of the framework are the fixed numbers that set every scale: the tick of the ledger, the reduced Planck constant ħ, Newton's constant G, and the couplings built from them. In ordinary physics such numbers are measured and then inserted by hand. Here they are outputs instead: ħ and G reduce to closed expressions in the golden ratio φ, and the nontrivial facts about those expressions are established theorems of the formal library, not fits to data.

The framework works in RS-native units. The tick τ₀ is the unit of time, and the speed of light c and the base length ℓ₀ are both set to one, with c · τ₀ = ℓ₀ holding by definition. Into these units enters the golden ratio φ, defined as (1 + sqrt 5) / 2, which the framework forces as the unique self-similar scaling of the cost structure. The reduced Planck constant is ħ = φ^(-5), and the library establishes the bounds 0.088 < ħ < 0.093. A separate pair of theorems records that ħ is positive and stays below one.

Newton's constant comes next, defined from the base length, the speed of light, and ħ. With the unit values substituted, Newton's constant reads G = φ^5 / π. The Einstein coupling κ = 8 π G / c^4 then carries the forced value straight into the notation of general relativity. Two more scales round out the picture: a factor K = φ^(1/2), established nonnegative, and the coherence energy, which makes ħ the energy of one tick.

The direction of explanation is the point. A framework with free constants takes their values from measurement and stops; this one fixes the values first and faces measurement afterward. Every scale above is either a definition in RS-native units or a theorem about those definitions, and the theorems audit to the kernel's three standard axioms with nothing RS-specific added. Whether the forced values agree with the measured ones is an empirical check, asked with the numbers already fixed.

THEOREM hbar · hbar_bounds · IndisputableMonolith/Constants.lean

THEOREM G · lambda_rec · c_ell0_tau0 · IndisputableMonolith/Constants.lean

MODEL tau0 · c · ell0 · IndisputableMonolith/Constants.lean

THEOREM hbar_positive · hbar_lt_one · IndisputableMonolith/Constants.lean

What this page does not claim

Agreement between the forced values and the measured constants is not claimed; that comparison is an empirical check, not a theorem. The fine-structure constant α is not derived here; exact α remains OPEN. The forcing of three spatial dimensions is not treated here; it belongs to the foundation chain.

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/Constants.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: