Encyclopedia Masses Masses Mass Genesis R4 Round2 Homogeneity Dichotomy Scratch

ARTICLE 5 claims 5 theorems

Masses Mass Genesis R4 Round2 Homogeneity Dichotomy Scratch

A proposed fork in a theory of mass turns out to be a false choice, and the real obstruction is not what the fork assumed.

Verify this page

The homogeneity dichotomy

The homogeneity dichotomy is a proposed fork in the Recognition Science account of particle masses. The fork asks whether the theory has an absolute unit of mass. If it does, a certain function V exists but merely restates the target law. If it does not, common rescaling is supposed to be only a change of unit, leaving no unit-free V. Both branches were meant to follow from a trichotomy: a window functional is either degree-2 covariant or degree-0 invariant, with no third kind.

The trichotomy is false. The logarithm of the load is a window functional that is neither invariant nor covariant of any degree. It is not a pathology; it is exactly the V the test asks for. What survives is a dichotomy about fixing a section, not about polynomial degree. The window action on the load is the free transitive action of the positive reals on the positive ray, so a load functional either is constant on the whole ray, and then it cannot shift, or it separates two points of one orbit, and then its value at one point of that orbit is a free choice.

Branch B's premise is also false. A change of unit multiplies every mass in the theory at once. The window action multiplies one of the theory's two mass channels and fixes the other. So common rescaling of all patterns is not a change of unit, and branch B's inference from unit-freedom to scale-invariance does not hold. A functional that is unit-free yet scale-detecting exists; it reads the topology channel, which is why it is not a route to the target.

Branch A's V exists, and its existence is empty. Vunit_shift proves the test is passed, by a window-only functional, for every positive unit U. V_test_pins_nothing proves that for every integer n some unit makes the value at a fixed witness equal n, and the unit that does it is load / phi ^ n, a literal read off the target exponent. So exhibiting a V is not evidence for R4; the whole content sits in the choice of U, and choosing U is choosing the answer.

The obstruction is not scale at all. no_windowOnly_V is unconditional and uses no analysis. spinClass is free data that enters rungOf and nothing else, so retopoRung moves the target's right-hand side by any integer while leaving the window, the support, and therefore every window functional fixed. Hence no window-only integer functional can equal the target law on the type. The missing ingredient is an admissibility condition on which (window, topology) pairs exist, not a cleverer functional. The negative results kill window-only integer functionals as a route to the target law stated on the whole type; they do not kill the law restricted to an admissibility class, which is exactly where routes A and charge 3 are working.

THEOREM loadIndexReal_not_covariantOfDegree · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean
loadIndexReal_not_covariantOfDegree · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean:181 
/-- **The section-2 trichotomy is FALSE.** The load index is covariant of no degree at
all, including degree zero. At the unit it vanishes; two rungs up it equals two; and
`c ^ d * 0 = 0` for every `d`. So window functionals are not exhausted by
{degree-0 invariant, degree-2 covariant}, and the counterexample is exactly the
functional the `V` test asks for, not a pathology at the edge of the class. -/
theorem loadIndexReal_not_covariantOfDegree (d : ℕ) :
    ¬ CovariantOfDegree (loadIndexReal 1) d := by
  intro h
  have h1 := h phi phi_pos 1 one_pos
  have hzero : loadIndexReal 1 1 = 0 := loadIndexReal_self one_pos
  have htwo : loadIndexReal 1 (phi ^ 2 * 1) = 2 := by
    rw [loadIndexReal_phi_sq one_pos one_pos, hzero]
    norm_num
  rw [htwo, hzero, mul_zero] at h1
  norm_num at h1
THEOREM load_orbit_is_the_full_ray · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean
load_orbit_is_the_full_ray · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean:122 
/-- **The scale orbit of any pattern with positive load realizes every positive load.**
This is the geometric fact that replaces the failed trichotomy: the window action on
the load is the free transitive action of the positive reals on the positive ray. -/
theorem load_orbit_is_the_full_ray
    {ψ : LightPattern (Fin 8)} (hpos : 0 < integratedMeaningLoad ψ)
    (t : ℝ) (ht : 0 < t) :
    ∃ c : ℝ, 0 < c ∧ integratedMeaningLoad (scalePattern c ψ) = t := by
  refine ⟨Real.sqrt (t / integratedMeaningLoad ψ), Real.sqrt_pos.mpr (by positivity), ?_⟩
  rw [integratedMeaningLoad_scalePattern, Real.sq_sqrt (by positivity)]
  field_simp
THEOREM unitFree_scaleDetecting_exists · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean
unitFree_scaleDetecting_exists · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean:490 
/-- **Charge 2's third kind of functional EXISTS.** A functional that is unit-free
(degree zero for the unit action) yet detects the window scale, shifting by exactly two
under multiplication of the window by `φ`. It is the `φ`-logarithm of the mass ratio.
The catch, and it is the whole story: unit-freedom forced a denominator, the only
same-degree denominator a single pattern owns is the topology channel, and reading that
channel is reading `rungOf`. -/
theorem unitFree_scaleDetecting_exists
    {ψ : LightPattern (Fin 8)} (h : StableClosedLightPattern ψ) :
    ∃ F : LightPattern (Fin 8) → ℝ,
      DimensionlessObservable F ∧
        F (scalePattern phi ψ) = F ψ + 2 := by
  refine ⟨fun χ => Real.log (restMass χ / predictedMass χ) / Real.log phi, ?_, ?_⟩
  · refine ⟨fun m p => Real.log (m / p) / Real.log phi, fun _ => rfl, ?_⟩
    intro k hk m p
    show Real.log (k * m / (k * p)) / Real.log phi = Real.log (m / p) / Real.log phi
    rw [mul_div_mul_left m p (ne_of_gt hk)]
  · 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 : (0 : ℝ) < phi ^ 2 := pow_pos phi_pos 2
    have hratio : (0 : ℝ) < restMass ψ / predictedMass ψ := div_pos hm hp
    have hlog : Real.log (phi ^ 2 * restMass ψ / predictedMass ψ)
        = 2 * Real.log phi + Real.log (restMass ψ / predictedMass ψ) := by
      rw [show phi ^ 2 * restMass ψ / predictedMass ψ
          = phi ^ 2 * (restMass ψ / predictedMass ψ) by ring,
        Real.log_mul (ne_of_gt hphi2) (ne_of_gt hratio), Real.log_pow]
      push_cast
      ring
    simp only [predictedMass_scalePattern, hnum]
    rw [hlog, add_div, mul_div_assoc, div_self log_phi_ne_zero, mul_one]
    ring
THEOREM Vunit_shift · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean
Vunit_shift · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean:213 
/-- **The `V` test is passed.** For every positive unit, `Vunit U` shifts by exactly two
under multiplication of the window by `φ`, and it never mentions `rungOf`. -/
theorem Vunit_shift {U : ℝ} (hU : 0 < U)
    {ψ : LightPattern (Fin 8)} (hpos : 0 < integratedMeaningLoad ψ) :
    Vunit U (scalePattern phi ψ) = Vunit U ψ + 2 := by
  unfold Vunit
  rw [integratedMeaningLoad_scalePattern]
  exact loadIndex_phi_sq hU hpos
THEOREM no_Vunit_satisfies_target_law · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean
no_Vunit_satisfies_target_law · IndisputableMonolith/Masses/MassGenesis/R4Round2HomogeneityDichotomyScratch.lean:378 
/-- The same statement for the concrete candidate: no choice of unit rescues it. -/
theorem no_Vunit_satisfies_target_law (U : ℝ) :
    ¬ ∀ ψ : LightPattern (Fin 8),
        Vunit U ψ = Anchor.r0 (sectorOf ψ) + rungOf ψ - 14 :=
  no_windowOnly_V (Vunit U) (Vunit_windowOnly U)

What this page does not claim

The target mass law is false; it is only unreachable by window-only functionals on the whole type. The module proves a positive result about particle masses; it is a negative structural result about a proposed route. The trichotomy failure means the framework is inconsistent; it means a proposed classification was incomplete.

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