Masses Mass Genesis R4 Round2 Homogeneity Dichotomy Scratch Exists Dimensionless

The mass ratio that detects scale

A dimensionless quantity is one that does not change when you change your units of measurement. In the Recognition Science framework's model of particle masses, the ratio of a pattern's rest mass to its predicted mass is dimensionless: multiply both masses by the same factor, and the ratio stays the same. But the framework's library proves that this same ratio is not scale-invariant: rescale the pattern by the golden ratio phi, and the ratio changes. The declaration exists_dimensionlessObservable_not_scaleInvariant establishes that a quantity can be unit-free yet still detect scale, and it does so without any hidden unit or absolute scale being chosen.

The framework models a particle pattern with two mass-carrying quantities. The rest mass is read off the pattern's window, and the predicted mass is read off its topology record. A rescaling operation, scalePattern, multiplies the rest mass by the square of the scaling factor but leaves the predicted mass untouched. So the ratio restMass / predictedMass changes when you rescale by phi, even though it is dimensionless. The declaration states this explicitly: for any stable closed light pattern, the ratio is a dimensionless observable, and its value at the rescaled pattern differs from its value at the original.

This result matters because it settles a structural question in the framework's mass-genesis program. A proposed dichotomy claimed that any window functional must be either scale-covariant of some degree or scale-invariant, with no third kind. The framework's library shows the dichotomy is false: the logarithm of the load is neither invariant nor covariant of any degree. What survives is a different dichotomy about fixing a section, not about polynomial degree. The mass-ratio result is the positive counterpart: it exhibits a dimensionless observable that is not scale-invariant, so unit-freedom does not force scale-blindness.

The declaration does not claim that this mass ratio is the target mass law. It does not provide a functional that computes the framework's target value for a pattern. The target law involves the sector and rung of the pattern, which read the topology record. The mass ratio reads both mass channels, so it is not a window-only functional. The declaration's role is narrower: it proves that a dimensionless observable can detect scaling, and it does so by reading the topology channel, which is why it is not a route to the target law. The missing ingredient for the target remains an admissibility condition on which window-topology pairs exist, not a cleverer functional.

/-- A functional is a **dimensionless observable** when it reads the theory's two mass
channels and is unchanged by a common positive rescaling of both. `scalePattern` does
not appear here. -/
def DimensionlessObservable (F : LightPattern (Fin 8) → ℝ) : Prop :=
  ∃ f : ℝ → ℝ → ℝ,
    (∀ ψ : LightPattern (Fin 8), F ψ = f (restMass ψ) (predictedMass ψ)) ∧
    (∀ k : ℝ, 0 < k → ∀ m p : ℝ, f (k * m) (k * p) = f m p)

/-- 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)

/-- **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 ψ⟩

/-- **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

The mass ratio is not the target mass law and does not compute the target value for a pattern. The declaration does not prove that all dimensionless observables detect scale; it exhibits one that does. The declaration does not establish that the framework's mass law is correct or matches measured particle masses.

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: