Encyclopedia Masses Masses Mass Genesis T10 Joint Scale Homogeneity No Go

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Joint Scale Homogeneity No Go

A theorem in the framework's library shows that no amplitude selector which ignores the absolute scale of a signal can ever determine the value of a particle mass.

Verify this page

The scale invariance wall

In the Recognition Science framework, particle masses are not free parameters but are supposed to be forced by the structure of recognition events. The framework keeps a discrete record of events, called a ledger, and the central question for mass generation is whether the recorded amplitude of a pattern uniquely determines the pattern's topology factor, the quantity that fixes the mass. The module T10JointScaleHomogeneityNoGo addresses a specific class of candidate mechanisms: those that are invariant under jointly rescaling both the posted amplitude and the pattern itself.

The main theorem, jointScaleInvariantSelector_does_not_force_amplitude, proves that no such selector can force the posted amplitude to equal the topology factor. The proof constructs a witness: a scaled pattern with a doubled amplitude that satisfies all the same conditions as the intended one, yet has a different amplitude. This witness is explicitly built in the theorem exists_jointScaleInvariantSelector_doubledAmplitudeWitness. The result is a no-go theorem: any selector that is blind to absolute scale cannot distinguish the intended amplitude from its doubled decoy.

Two concrete instances of this class are shown to exist. First, any selector that depends only on the ledger topology, ignoring the amplitude argument entirely, is joint-scale invariant by construction. Second, the shared-magnitude signed Green emission package is inhabited at every positive magnitude, so its amplitude-only lift is also joint-scale invariant. Both instances recover the previously banked walls as corollaries of the class theorem.

The module also proves a complementary result: any selector that does force the amplitude to the topology factor cannot be joint-scale invariant. This is the theorem amplitudeForcingSelector_not_jointScaleInvariant. Together, the two theorems carve out the boundary: scale invariance and amplitude forcing are mutually exclusive properties for any selector.

The certificate structure T10JointScaleHomogeneityNoGoCert packages all these results into a single object, confirming that the class wall holds for the ledger-topology-only parents, the shared-magnitude package, and the relative window selector. The module contains no sorry and introduces no new axioms, so the no-go result is fully machine-checked.

THEOREM jointScaleInvariantSelector_does_not_force_amplitude · IndisputableMonolith/Masses/MassGenesis/T10JointScaleHomogeneityNoGo.lean
jointScaleInvariantSelector_does_not_force_amplitude · IndisputableMonolith/Masses/MassGenesis/T10JointScaleHomogeneityNoGo.lean:148 
/-- Main class theorem: no joint-scale-invariant selector that accepts the
intended witness can force posted amplitude to the topology factor. -/
theorem jointScaleInvariantSelector_does_not_force_amplitude
    (S : Q3SettledLedgerOctave → ℝ → LightPattern (Fin 8) → Prop)
    (hS : IsJointScaleInvariantSelector S)
    (octave : Q3SettledLedgerOctave)
    (hintended :
      S octave intendedGapOneFactorAmplitude intendedGapOneFactorPattern) :
    ¬ ∀ (a : ℝ) (ha : 0 < a) (ψ : LightPattern (Fin 8)),
      S octave a ψ →
        Q3MatterCarrier ψ →
          SettledAnchorWindow a ψ →
            PhotonWindowReadsPatternAnchor
                (originEmittedPhotonStateScaled octave a ha).window ψ →
              a = primitivePositiveStationaryFactorAmplitude ψ := by
  intro hall
  obtain ⟨a, ha, ψ, hparent, hcarrier, hwin, hread, hne⟩ :=
    exists_jointScaleInvariantSelector_doubledAmplitudeWitness
      S hS octave hintended
  exact hne (hall a ha ψ hparent hcarrier hwin hread)
THEOREM exists_jointScaleInvariantSelector_doubledAmplitudeWitness · IndisputableMonolith/Masses/MassGenesis/T10JointScaleHomogeneityNoGo.lean
exists_jointScaleInvariantSelector_doubledAmplitudeWitness · IndisputableMonolith/Masses/MassGenesis/T10JointScaleHomogeneityNoGo.lean:81 
/-- If a joint-scale-invariant selector accepts the intended factor-scaled
gap-one witness, it also accepts the doubled sourced-emission decoy whose
posted amplitude misses the topology factor. -/
theorem exists_jointScaleInvariantSelector_doubledAmplitudeWitness
    (S : Q3SettledLedgerOctave → ℝ → LightPattern (Fin 8) → Prop)
    (hS : IsJointScaleInvariantSelector S)
    (octave : Q3SettledLedgerOctave)
    (hintended :
      S octave intendedGapOneFactorAmplitude intendedGapOneFactorPattern) :
    ∃ (a : ℝ) (ha : 0 < a) (ψ : LightPattern (Fin 8)),
      S octave a ψ ∧
        Q3MatterCarrier ψ ∧
          SettledAnchorWindow a ψ ∧
            PhotonWindowReadsPatternAnchor
                (originEmittedPhotonStateScaled octave a ha).window ψ ∧
              a ≠ primitivePositiveStationaryFactorAmplitude ψ := by
  let seed := worldlinePattern gapOneTwoPhaseMode
  let f := intendedGapOneFactorAmplitude
  let ground := intendedGapOneFactorPattern
  let a := 2 * f
  let ψ := scalePattern 2 ground
  have hf : 0 < f := by
    simpa [f, intendedGapOneFactorAmplitude, seed] using gapOne_factorAmplitude_pos
  have ha : 0 < a := mul_pos (by norm_num) hf
  obtain ⟨Eseed⟩ := q3MatterCarrier_worldlinePattern_gapOne
  have Eground : Q3ClosedPatternEvidence ground := by
    simpa [ground, intendedGapOneFactorPattern, f, intendedGapOneFactorAmplitude,
      seed] using scalePattern_q3ClosedEvidence f hf Eseed
  have Eψ : Q3ClosedPatternEvidence ψ :=
    scalePattern_q3ClosedEvidence 2 (by norm_num) Eground
  have hgroundWin : SettledAnchorWindow f ground := by
    simpa [ground, intendedGapOneFactorPattern, f, intendedGapOneFactorAmplitude,
      seed] using scalePattern_settledAnchor f worldlineGapOne_settledAnchor_unit
  have hwin : SettledAnchorWindow a ψ := by
    simpa [a, ψ] using scalePattern_settledAnchor 2 hgroundWin
  have hparent : S octave a ψ := by
    have hground : S octave f ground := by
      simpa [f, ground, intendedGapOneFactorAmplitude,
        intendedGapOneFactorPattern] using hintended
    exact (hS 2 (by norm_num) octave f ground).mp hground
  have hread :
      PhotonWindowReadsPatternAnchor
        (originEmittedPhotonStateScaled octave a ha).window ψ := by
    unfold PhotonWindowReadsPatternAnchor
    simp [ψ, ground, a, f, intendedGapOneFactorPattern,
      intendedGapOneFactorAmplitude, originEmittedScaled_window_eq_scaledGapOne,
      scalePattern, worldlinePattern, mul_assoc]
  have hfactorψ :
      primitivePositiveStationaryFactorAmplitude ψ = f := by
    calc
      primitivePositiveStationaryFactorAmplitude ψ =
          primitivePositiveStationaryFactorAmplitude ground := by
            simpa [ψ] using
              primitivePositiveStationaryFactorAmplitude_scalePattern 2 ground
      _ = primitivePositiveStationaryFactorAmplitude seed := by
            simpa [ground, intendedGapOneFactorPattern, f,
              intendedGapOneFactorAmplitude, seed] using
              primitivePositiveStationaryFactorAmplitude_scalePattern f seed
      _ = f := by
            simp [f, intendedGapOneFactorAmplitude, seed]
  have hne : a ≠ primitivePositiveStationaryFactorAmplitude ψ := by
    rw [hfactorψ]
    intro heq
    dsimp [a] at heq
    nlinarith
  exact ⟨a, ha, ψ, hparent, ⟨Eψ⟩, hwin, hread, hne⟩
THEOREM liftLedgerTopologyOnlyParent_jointScaleInvariant · IndisputableMonolith/Masses/MassGenesis/T10JointScaleHomogeneityNoGo.lean
liftLedgerTopologyOnlyParent_jointScaleInvariant · IndisputableMonolith/Masses/MassGenesis/T10JointScaleHomogeneityNoGo.lean:343 
theorem liftLedgerTopologyOnlyParent_jointScaleInvariant
    (P : Q3SettledLedgerOctave → LightPattern (Fin 8) → Prop)
    (hP : IsLedgerTopologyOnlyParent P) :
    IsJointScaleInvariantSelector (liftLedgerTopologyOnlyParent P) := by
  intro c _hc octave a ψ
  simpa [liftLedgerTopologyOnlyParent] using
    ledgerTopologyOnlyParent_scaleInvariant P hP octave c ψ
THEOREM amplitudeForcingSelector_not_jointScaleInvariant · IndisputableMonolith/Masses/MassGenesis/T10JointScaleHomogeneityNoGo.lean
amplitudeForcingSelector_not_jointScaleInvariant · IndisputableMonolith/Masses/MassGenesis/T10JointScaleHomogeneityNoGo.lean:169 
/-- Admission-gate export: any selector that forces amplitude on the intended
witness cannot be joint-scale invariant. -/
theorem amplitudeForcingSelector_not_jointScaleInvariant
    (S : Q3SettledLedgerOctave → ℝ → LightPattern (Fin 8) → Prop)
    (octave : Q3SettledLedgerOctave)
    (hintended :
      S octave intendedGapOneFactorAmplitude intendedGapOneFactorPattern)
    (hforces :
      ∀ (a : ℝ) (ha : 0 < a) (ψ : LightPattern (Fin 8)),
        S octave a ψ →
          Q3MatterCarrier ψ →
            SettledAnchorWindow a ψ →
              PhotonWindowReadsPatternAnchor
                  (originEmittedPhotonStateScaled octave a ha).window ψ →
                a = primitivePositiveStationaryFactorAmplitude ψ) :
    ¬ IsJointScaleInvariantSelector S := by
  intro hS
  exact
    (jointScaleInvariantSelector_does_not_force_amplitude
      S hS octave hintended) hforces
THEOREM t10JointScaleHomogeneityNoGoCert · IndisputableMonolith/Masses/MassGenesis/T10JointScaleHomogeneityNoGo.lean
t10JointScaleHomogeneityNoGoCert · IndisputableMonolith/Masses/MassGenesis/T10JointScaleHomogeneityNoGo.lean:477 
theorem t10JointScaleHomogeneityNoGoCert :
    T10JointScaleHomogeneityNoGoCert where
  class_wall := jointScaleInvariantSelector_does_not_force_amplitude
  admission_export := amplitudeForcingSelector_not_jointScaleInvariant
  relative_window_in_class := relativeWindowSelector_jointScaleInvariant
  relative_window_nonvacuous := relativeWindowSelector_accepts_intended
  ledger_topology_instance :=
    liftLedgerTopologyOnlyParent_jointScaleInvariant
  shared_magnitude_instance :=
    sharedMagnitudeAmplitudeSelector_jointScaleInvariant
  residual_still_false := postedAmplitudeMatchesTopologyFactor_wall

What this page does not claim

This theorem does not claim that no selector can ever force the amplitude, only that no joint-scale-invariant one can. The module does not prove that the topology factor itself is the correct mass value. The affine-Weyl dilation stationary properties are not re-derived as members of the joint-scale-invariant selector class.

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/T10JointScaleHomogeneityNoGo.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