Encyclopedia Masses Masses Mass Genesis R4 Round2 Homogeneity Dichotomy Scratch Dimensionless Observ

ARTICLE 3 claims 3 theorems

Masses Mass Genesis R4 Round2 Homogeneity Dichotomy Scratch Dimensionless Observ

A dimensionless observable in this framework can only be a function of the ratio of two masses, which pins down what scale invariance can and cannot mean.

Verify this page

The ratio theorem

A dimensionless observable is a quantity that does not change when you change your units. In the Recognition Science framework, a pattern carries two mass-like numbers: restMass, read from a window, and predictedMass, read from a topology record. The theorem dimensionlessObservable_factors_through_ratio states that any dimensionless observable must be a function of the ratio of these two masses: there exists a function g such that F(ψ) = g(restMass ψ / predictedMass ψ) for every pattern ψ.

This is a structural constraint, not a numerical prediction. It says the only way to build a unit-free quantity from the two mass channels is to divide one by the other. The theorem is proved in the machine-checked library of formal theorems, and it is a theorem, not a definitional choice. It follows from the definition of a dimensionless observable, which requires that scaling both masses by the same factor leaves the observable unchanged. Dividing restMass by predictedMass is the canonical way to achieve that, and the theorem shows it is the only way.

The theorem does not claim that every function of the ratio is a valid observable. It only says that if something is a dimensionless observable, it must factor through the ratio. It also does not claim that the ratio itself is scale-invariant. In fact, the library proves the opposite: the ratio changes when the pattern is scaled by the golden ratio φ, while the predictedMass stays fixed. This is the key to the homogeneity dichotomy: a unit-free quantity can still detect scale, because scaling a pattern is not the same as changing units. The window action moves restMass but fixes predictedMass, so a common rescaling of both channels is not a unit change.

The theorem also does not say that the ratio is the only dimensionless observable in a practical sense. It says any dimensionless observable must be a function of the ratio, but the function g could be constant, or it could be the identity. The theorem leaves open what that function is. It is a classification of the form, not a determination of the content. The content sits in the choice of g, and that choice is where the physics lives.

THEOREM dimensionlessObservable_factors_through_ratio · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean
dimensionlessObservable_factors_through_ratio · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean:401 
/-- **Every dimensionless observable is a function of one number**, the window-to-
topology mass ratio. This is what makes the class say something: the whole unit-free
content of a single pattern is a single real. -/
theorem dimensionlessObservable_factors_through_ratio
    {F : LightPattern (Fin 8) → ℝ} (h : DimensionlessObservable F) :
    ∃ g : ℝ → ℝ, ∀ ψ : LightPattern (Fin 8),
      F ψ = g (restMass ψ / predictedMass ψ) := by
  obtain ⟨f, hrep, hunit⟩ := h
  refine ⟨fun x => f x 1, ?_⟩
  intro ψ
  have hp : 0 < predictedMass ψ := predictedMass_pos ψ
  have hk : 0 < 1 / predictedMass ψ := by positivity
  have hu := hunit (1 / predictedMass ψ) hk (restMass ψ) (predictedMass ψ)
  have hone : (1 / predictedMass ψ) * predictedMass ψ = 1 :=
    one_div_mul_cancel (ne_of_gt hp)
  rw [hone] at hu
  rw [hrep ψ, ← hu]
  congr 1
  ring
THEOREM massRatio_dimensionlessObservable · 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)
THEOREM scalePattern_is_not_a_unit_change · exists_dimensionlessObservable_not_scaleInvariant · 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 ψ⟩
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

The theorem does not specify what the function g is. The theorem does not claim that every function of the ratio is a valid observable. The theorem does not claim that the ratio is scale-invariant; it proves the opposite.

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