Masses Mass Genesis R4 Round2 Homogeneity Dichotomy Scratch Power Of Two Would N

The unabsorbable two

The golden ratio, usually written φ, is the number that solves r² = r + 1, about 1.618. A classical fact about it is that its integer powers never hit a whole number: φ, φ², φ³, and so on are all irrational, so none of them equals 2, or 3, or any other integer. The machine-checked theorem power_of_two_would_not_be_absorbable records the specific case: there is no integer k for which φ raised to the k-th power equals 2. That is, the number 2 does not sit on the golden-ratio ladder.

In the Recognition Science framework, this fact has a job. The framework's mass-generation program arranges particle masses on a ladder of φ-powers. A proposed shortcut would absorb a factor of 2 into the ladder by shifting the rung index, effectively claiming that 2 is some φ^k. The theorem blocks that move: because 2 is not a φ-power, the shortcut cannot hide the factor of 2 by renumbering the ladder. The obstruction is not a matter of computation or approximation; it is a proved impossibility.

What the theorem does not do is say anything about the masses themselves. It does not claim that no mass ratio equals 2, nor that the ladder is the only way to organize masses. It speaks only to the arithmetic of φ and 2. The theorem is a gatekeeper for one specific class of arguments, not a verdict on the mass program as a whole.

/-- The control that keeps the previous theorem from being vacuous: a would-be unit that
is a power of two is NOT absorbable into rung shifts. So absorbability is a real test
that `E_coh` fails and something else passes. -/
theorem power_of_two_would_not_be_absorbable : ¬ ∃ k : ℤ, (2 : ℝ) = phi ^ k :=
  LadderOffsetGauge.power_of_two_not_absorbable

What this page does not claim

The theorem does not state that the golden ratio is irrational, only that 2 is not one of its integer powers. The theorem does not say that no particle mass ratio can equal 2. The theorem does not prove that the ladder of φ-powers is the only possible mass organization.

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/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.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: