Masses Mass Genesis T10 Joint Scale Homogeneity No Go Shared Magnitude Signed Gr

The joint-scale wall

In the Recognition Science framework, particle masses are not free parameters but are supposed to emerge from a discrete record of recognition events, which the framework calls a ledger. The specific question at issue is whether the amplitude of a posted mass, the number that sets its scale, can be forced by the structure of the pattern it belongs to. The framework's library, a machine-checked collection of formal theorems, answers this with a precise negative result, the joint-scale homogeneity no-go wall.

The theorem named sharedMagnitudeSignedGreenEmission_does_not_force_amplitude_of_jointScale proves that a certain class of amplitude selectors cannot determine the posted amplitude. These selectors are invariant under joint rescaling: if you scale both the posted amplitude and the pattern together, the selector's verdict does not change. The theorem shows that no such selector, even when it accepts the intended gap-one factor and satisfies all the window and carrier conditions, can force the amplitude to equal the topology factor primitivePositiveStationaryFactorAmplitude. In plain terms, scale symmetry alone cannot pin down the mass scale.

The result is part of a broader class wall. Nine separate scale attacks each produced the same fact, and the module proves it once at the level of the class IsJointScaleInvariantSelector. The shared-magnitude signed Green package is one instance: it is inhabited at every positive magnitude, so its amplitude-only lift is joint-scale invariant, and the banked transport wall is recovered as a corollary. The theorem is axiom-clean, with no sorry and no new Lean axiom.

What the theorem does not claim is equally important. It does not say that amplitude forcing is impossible in general; it says only that joint-scale-invariant selectors cannot do it. A selector that is not invariant under joint rescaling, such as the amplitude-forcing selector that the module explicitly shows is not joint-scale invariant, is not covered by the wall. The no-go result also does not touch the affine-Weyl dilation stationarity facts, which live on a different object and are not re-derived as members of the class. The wall is a precise boundary, not a blanket impossibility.

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

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

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

What this page does not claim

The theorem does not rule out all amplitude forcing, only forcing by joint-scale-invariant selectors. The no-go result does not apply to affine-Weyl dilation stationarity, which lives on a different object. The theorem does not say the intended amplitude is unreachable, only that this class of selectors cannot force it.

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: