Encyclopedia Masses Masses Mass Genesis R4 Round2 Homogeneity Dichotomy Scratch Rest Mass Not Dimens

ARTICLE 3 claims 3 theorems

Masses Mass Genesis R4 Round2 Homogeneity Dichotomy Scratch Rest Mass Not Dimens

In the framework's mass model, rest mass resists being re-expressed as a pure ratio of other masses, a fact with a proof.

Verify this page

Rest mass is not a ratio

In physics, a dimensionless quantity is one that stays the same no matter what units you measure it in. The ratio of two masses is dimensionless: whether you weigh them in kilograms or pounds, the quotient is unchanged. The Recognition Science framework's machine-checked library of formal theorems proves that its rest mass, the mass read off a pattern's window, is not such a quantity. The declaration restMass_not_dimensionlessObservable establishes, for every stable closed light pattern, that there is no way to write rest mass as a function of the pattern that is invariant under common rescaling of both mass channels.

The proof rests on a structural fact about the framework's two mass channels. A pattern carries rest mass, read from its window, and predicted mass, read from its topology record. The framework's scaling operation multiplies the window channel by the square of a factor while leaving the topology channel untouched. The theorem scalePattern_is_not_a_unit_change records this asymmetry: scaling changes rest mass but fixes predicted mass. Because a genuine change of units would multiply every mass in the theory at once, common rescaling is not a change of units, and a functional that ignores the distinction cannot be unit-free yet scale-detecting.

The declaration's content is negative but precise. It says rest mass does not factor through the ratio restMass / predictedMass, the way a true dimensionless observable must by the theorem dimensionlessObservable_factors_through_ratio. The library also proves the converse positively: the ratio itself is a dimensionless observable (massRatio_dimensionlessObservable), and it is not scale-invariant (exists_dimensionlessObservable_not_scaleInvariant). So the framework's account is not that no dimensionless observables exist; it is that rest mass, taken alone, is not one of them.

What the declaration does not claim is broader. It does not say rest mass is physically meaningless, nor that the framework's mass predictions are untestable. The theorem applies to a specific formal class of observables, those invariant under simultaneous rescaling of both mass channels. It leaves open the possibility of admissible observables that read the topology record, and it does not touch the empirical comparison of predicted masses against measured values. The framework's mass ladder remains a separate, empirical claim.

THEOREM restMass_not_dimensionlessObservable · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean
restMass_not_dimensionlessObservable · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean:455 
/-- **The observable class is PROPER, and the witness is not the target.** `restMass` is
not a dimensionless observable. The separating pair comes from `retopoRung`, not from
anything about scale: move the stored rung up by one, then rescale the window by
`√φ`, and the ratio comes back to where it started while the rest mass has moved by a
factor of `φ`. So the class genuinely excludes something, and it excludes exactly what
it should: a magnitude with no unit attached. -/
theorem restMass_not_dimensionlessObservable
    {ψ : LightPattern (Fin 8)} (h : StableClosedLightPattern ψ) :
    ¬ DimensionlessObservable restMass := by
  intro hobs
  obtain ⟨g, hg⟩ := dimensionlessObservable_factors_through_ratio hobs
  have hp : 0 < predictedMass ψ := predictedMass_pos ψ
  have hm : 0 < restMass ψ := restMass_pos_of_stable ψ h
  have hsqrt : (0 : ℝ) < Real.sqrt phi := Real.sqrt_pos.mpr phi_pos
  have hsq : (Real.sqrt phi) ^ 2 = phi := Real.sq_sqrt (le_of_lt phi_pos)
  set χ := scalePattern (Real.sqrt phi) (retopoRung 1 ψ) with hχ
  have hstable1 : StableClosedLightPattern (retopoRung 1 ψ) :=
    (retopoRung_stable 1 ψ).mpr h
  have hmχ : restMass χ = phi * restMass ψ := by
    rw [hχ, restMass_scalePattern (ne_of_gt hsqrt) hstable1, hsq,
      retopoRung_restMass]
  have hpχ : predictedMass χ = phi * predictedMass ψ := by
    rw [hχ, predictedMass_scalePattern, retopoRung_predictedMass]
    rw [zpow_one]
  have hratio : restMass χ / predictedMass χ = restMass ψ / predictedMass ψ := by
    rw [hmχ, hpχ]
    exact mul_div_mul_left _ _ (ne_of_gt phi_pos)
  have hcontra : restMass χ = restMass ψ := by
    rw [hg χ, hratio, ← hg ψ]
  rw [hmχ] at hcontra
  have hfac : (phi - 1) * restMass ψ = 0 := by linear_combination hcontra
  rcases mul_eq_zero.1 hfac with h1 | h1
  · exact absurd (by linarith : phi = 1) phi_ne_one
  · exact absurd h1 (ne_of_gt hm)
THEOREM scalePattern_is_not_a_unit_change · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean
scalePattern_is_not_a_unit_change · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean:109 
/-- **Branch B's premise, refuted.** A change of unit rescales every mass at once. The
window action rescales the window channel and fixes the topology channel, so it is not
a change of unit, and the inference "unit-free, therefore invariant under common
rescaling" fails. -/
theorem scalePattern_is_not_a_unit_change
    {ψ : LightPattern (Fin 8)} (h : StableClosedLightPattern ψ) :
    restMass (scalePattern phi ψ) ≠ restMass ψ ∧
      predictedMass (scalePattern phi ψ) = predictedMass ψ :=
  ⟨R4GenesisRouteCD.scalePattern_changes_restMass h phi_pos phi_ne_one,
   predictedMass_scalePattern phi ψ⟩
THEOREM massRatio_dimensionlessObservable · exists_dimensionlessObservable_not_scaleInvariant · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean
massRatio_dimensionlessObservable · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean:421 
/-- The window-to-topology mass ratio is a dimensionless observable. -/
theorem massRatio_dimensionlessObservable :
    DimensionlessObservable (fun ψ => restMass ψ / predictedMass ψ) := by
  refine ⟨fun m p => m / p, fun _ => rfl, ?_⟩
  intro k hk m p
  exact mul_div_mul_left m p (ne_of_gt hk)
exists_dimensionlessObservable_not_scaleInvariant · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean:428 
/-- **ANSWER TO THE SECTION-3 QUESTION: NO.** Not every dimensionless observable is
invariant under common rescaling of all patterns. The window-to-topology mass ratio is
unit-free and is moved by the window action, because that action moves one mass channel
and fixes the other. Branch B therefore fails, and by
`dimensionlessObservable_factors_through_ratio` this single ratio is the *only*
unit-free degree of freedom a pattern has, so the failure is not a loophole to exploit:
the one dimensionless quantity common rescaling moves is the quantity R4 is about. -/
theorem exists_dimensionlessObservable_not_scaleInvariant
    {ψ : LightPattern (Fin 8)} (h : StableClosedLightPattern ψ) :
    DimensionlessObservable (fun χ => restMass χ / predictedMass χ) ∧
      (fun χ => restMass χ / predictedMass χ) (scalePattern phi ψ)
        ≠ (fun χ => restMass χ / predictedMass χ) ψ := by
  refine ⟨massRatio_dimensionlessObservable, ?_⟩
  have hp : 0 < predictedMass ψ := predictedMass_pos ψ
  have hm : 0 < restMass ψ := restMass_pos_of_stable ψ h
  have hnum : restMass (scalePattern phi ψ) = phi ^ 2 * restMass ψ :=
    restMass_scalePattern (ne_of_gt phi_pos) h
  have hphi2 : (1 : ℝ) < phi ^ 2 := by nlinarith [one_lt_phi, phi_pos]
  have hlt : restMass ψ < phi ^ 2 * restMass ψ := by nlinarith [hphi2, hm]
  have hinv : (0 : ℝ) < (predictedMass ψ)⁻¹ := inv_pos.mpr hp
  have hdiv : restMass ψ / predictedMass ψ
      < phi ^ 2 * restMass ψ / predictedMass ψ := by
    rw [div_eq_mul_inv, div_eq_mul_inv]
    exact mul_lt_mul_of_pos_right hlt hinv
  simp only [predictedMass_scalePattern, hnum]
  exact ne_of_gt hdiv

What this page does not claim

Rest mass is physically meaningless or untestable. No dimensionless observables exist in the framework; the ratio restMass / predictedMass is one. The theorem applies to observables that are allowed to read the topology record.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND