Encyclopedia Masses Masses Mass Genesis T10 Joint Scale Homogeneity No Go Joint Scale Invariant Sele

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Joint Scale Homogeneity No Go Joint Scale Invariant Sele

A selector that treats amplitude and pattern as one scale cannot pin down the amplitude, a machine-checked theorem that maps the edge of what mass genesis can force.

Verify this page

The scale-invariance wall

In the Recognition Science account, mass values are not free parameters but outcomes of a recognition process. A central question is whether the process can force a specific amplitude, the size of the posted value, from the structure of the pattern alone. This theorem addresses a natural candidate: a selector that is invariant under joint rescaling, meaning it treats the amplitude and the pattern as a single scale, so that doubling both at once changes nothing about the selection.

The theorem, named jointScaleInvariantSelector_does_not_force_amplitude, proves that any such selector fails to force the amplitude to the topology factor primitivePositiveStationaryFactorAmplitude. In plain terms, if a selection rule is blind to the overall scale, it cannot single out one specific amplitude as the only acceptable one. The proof constructs a witness: a doubled amplitude with a scaled pattern that the selector accepts, yet which differs from the intended factor. This is not a failure of a particular rule but a structural property of the entire class of joint-scale-invariant selectors, as the theorem quantifies over all of them.

The result is a wall, not a hole. It shows that the mass-genesis program cannot rely on scale-invariant selection alone to derive amplitudes. The framework's library, a machine-checked collection of formal theorems, records this as a class-level no-go result, with no unproved assumptions. The theorem also recovers two earlier, more specific walls as corollaries: one for selectors that ignore the amplitude entirely, and one for a shared-magnitude signed Green package. Both are instances of the same general fact, now proven once at the level of the class.

What the theorem does not claim is just as important. It does not say that no selector can force the amplitude. It only rules out those that are joint-scale invariant. Indeed, the library also proves the converse: a selector that does force the amplitude cannot be joint-scale invariant. The two properties are incompatible. The theorem also does not address selectors that are homogeneous under a different symmetry, such as affine-Weyl dilation stationarity, which live on a different type and are not instances of this class. The wall is precise: it blocks one specific, natural approach, and leaves the door open for other selection rules that break the joint scale symmetry.

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 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 ledgerTopologyOnlyParent_does_not_force_amplitude_of_jointScale · sharedMagnitudeSignedGreenEmission_does_not_force_amplitude_of_jointScale · IndisputableMonolith/Masses/MassGenesis/T10JointScaleHomogeneityNoGo.lean
ledgerTopologyOnlyParent_does_not_force_amplitude_of_jointScale · IndisputableMonolith/Masses/MassGenesis/T10JointScaleHomogeneityNoGo.lean:351 
/-- Formal recovery of the A-scale-08 wall from the class theorem. -/
theorem ledgerTopologyOnlyParent_does_not_force_amplitude_of_jointScale
    (P : Q3SettledLedgerOctave → LightPattern (Fin 8) → Prop)
    (hP : IsLedgerTopologyOnlyParent P)
    (octave : Q3SettledLedgerOctave)
    (hfactor :
      P octave intendedGapOneFactorPattern) :
    ¬ ∀ (a : ℝ) (ha : 0 < a) (ψ : LightPattern (Fin 8)),
      P octave ψ →
        Q3MatterCarrier ψ →
          SettledAnchorWindow a ψ →
            PhotonWindowReadsPatternAnchor
                (originEmittedPhotonStateScaled octave a ha).window ψ →
              a = primitivePositiveStationaryFactorAmplitude ψ := by
  have hS :
      IsJointScaleInvariantSelector (liftLedgerTopologyOnlyParent P) :=
    liftLedgerTopologyOnlyParent_jointScaleInvariant P hP
  have hintended :
      liftLedgerTopologyOnlyParent P octave intendedGapOneFactorAmplitude
        intendedGapOneFactorPattern := by
    simpa [liftLedgerTopologyOnlyParent] using hfactor
  intro hall
  exact
    (jointScaleInvariantSelector_does_not_force_amplitude
      (liftLedgerTopologyOnlyParent P) hS octave hintended)
      (by
        intro a ha ψ hS' hcarrier hwin hread
        exact hall a ha ψ hS' hcarrier hwin hread)
sharedMagnitudeSignedGreenEmission_does_not_force_amplitude_of_jointScale · IndisputableMonolith/Masses/MassGenesis/T10JointScaleHomogeneityNoGo.lean:411 
/-- Formal recovery of the A-scale-09 shared-magnitude force wall from the
class theorem. -/
theorem sharedMagnitudeSignedGreenEmission_does_not_force_amplitude_of_jointScale
    (octave : Q3SettledLedgerOctave) :
    ¬ ∀ (a : ℝ) (ha : 0 < a) (ψ : LightPattern (Fin 8)),
      SharedMagnitudeSignedGreenEmissionPackage octave a ha →
        Q3MatterCarrier ψ →
          SettledAnchorWindow a ψ →
            PhotonWindowReadsPatternAnchor
                (originEmittedPhotonStateScaled octave a ha).window ψ →
              a = primitivePositiveStationaryFactorAmplitude ψ := by
  intro hall
  exact
    (jointScaleInvariantSelector_does_not_force_amplitude
      sharedMagnitudeAmplitudeSelector
      sharedMagnitudeAmplitudeSelector_jointScaleInvariant octave
      (sharedMagnitudeAmplitudeSelector_accepts_intended octave))
      (by
        intro a ha ψ hS hcarrier hwin hread
        obtain ⟨ha', hp⟩ := hS
        exact hall a ha ψ
          (sharedMagnitudeSignedGreenEmissionPackage_all_positive octave a ha)
          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⟩

What this page does not claim

No selector at all can force the amplitude. The theorem applies to selectors with symmetries other than joint rescaling. The amplitude is unforced in the full mass-genesis framework.

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