Encyclopedia Masses Masses Mass Genesis T10 Joint Scale Homogeneity No Go Exists Joint Scale Invaria

ARTICLE 2 claims 2 theorems

Masses Mass Genesis T10 Joint Scale Homogeneity No Go Exists Joint Scale Invaria

A machine-checked proof shows why a certain class of amplitude rules can never pin down a unique mass value, no matter how they are designed.

Verify this page

The scale trap

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition is the act of matching a pattern against that record at a fixed cost. The declaration exists_jointScaleInvariantSelector_doubledAmplitudeWitness is a formal theorem, proved in the framework's machine-checked library, about a class of rules called joint-scale-invariant selectors. Such a selector is a rule that, given a posted amplitude and a pattern, decides whether the pattern is recognized; it is joint-scale-invariant if rescaling both the amplitude and the pattern by the same positive factor leaves the decision unchanged.

The theorem states that for any such selector, if it accepts the intended gap-one factor pattern, then there exists another positive amplitude and another pattern that it also accepts, which satisfies all the same physical conditions (it is a matter carrier, has a settled anchor window, and the photon window reads the pattern anchor), but whose amplitude is not the intended topology factor. In plain terms: a rule that is blind to joint rescaling cannot distinguish the intended amplitude from a doubled decoy. The proof is constructive, producing the witness explicitly, and it is a theorem in the framework's library, with no unproven assumptions.

This result is a no-go theorem. It does not say that no selector can ever force the correct amplitude; it says that no joint-scale-invariant selector can. The framework's own amplitude-forcing selector is, in fact, proven not to be joint-scale-invariant, which is how it escapes the trap. The theorem also does not claim that the doubled amplitude is physically realized; it only shows that a certain class of rules cannot rule it out. The proof is part of a larger effort to understand how mass values are forced, and it marks a precise boundary: scale-blind rules are too weak to do the job.

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

What this page does not claim

No selector can ever force the correct amplitude. The doubled amplitude witness is physically realized. The theorem applies to selectors that are not joint-scale-invariant.

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