Encyclopedia Masses Masses Mass Genesis T10 Ledger Topology Amplitude Force Wall Ledger Topology Onl

ARTICLE 4 claims 4 theorems

Masses Mass Genesis T10 Ledger Topology Amplitude Force Wall Ledger Topology Onl

A machine-checked theorem proves that any rule reading only settled records and shape labels cannot fix the size of a posting, and names the missing ingredient.

Verify this page

The wall around amplitude

In the Recognition Science account of how masses arise, a central question is whether the size of a quantum event is forced by the structure of a discrete record. The framework's library of formal theorems has now settled one boundary of that question. A theorem named ledgerTopologyOnlyParent_does_not_force_amplitude proves that no rule which reads only the settled ledger, the discrete record of past events, and the topology, the shape labels of a pattern, can determine the posting amplitude, the positive size attached to a quantum emission. The proof is machine-checked, meaning it is verified by a computer from the framework's axioms.

The argument is a wall around an entire class of candidate rules, not a single failure. The theorem first shows that any such rule is blind to rescaling: if it accepts a pattern at one scale, it accepts the same pattern at any positive scale, because the scale is not part of the ledger or the topology. It then constructs a doubled witness, a second pattern with twice the posting amplitude that still satisfies every ledger and topology condition. A rule that accepts the intended pattern must therefore also accept the doubled one, and so it cannot force the amplitude to be the specific value the framework expects. The wall is generic: it rules out every parent rule in the class at once.

The theorem does not claim that the amplitude is unforced, only that this particular route cannot force it. A separate theorem, amplitudeForcingParent_not_ledgerTopologyOnly, states the exact boundary: any rule that really does force the scaled amplitude and accepts the intended witness cannot be ledger/topology-only. The framework's campaign therefore requires a lower-level field that carries scale independently, and an explicit rejection of the doubled witness. The wall is a precise negative result that redirects the search, not a dead end.

What the theorem changes is the shape of the remaining work. It converts an open question, how the amplitude is forced, into a proven constraint on the answer: the forcing must come from information outside the settled ledger and the topology labels. This is a structural result about what kind of theory can succeed, and it is the kind of statement the framework is built to deliver.

THEOREM ledgerTopologyOnlyParent_does_not_force_amplitude · IndisputableMonolith/Masses/MassGenesis/T10LedgerTopologyAmplitudeForceWall.lean
ledgerTopologyOnlyParent_does_not_force_amplitude · IndisputableMonolith/Masses/MassGenesis/T10LedgerTopologyAmplitudeForceWall.lean:126 
/-- A ledger/topology-only parent that accepts the intended witness cannot
force the posting amplitude on all scaled sourced-emission readings. -/
theorem ledgerTopologyOnlyParent_does_not_force_amplitude
    (P : Q3SettledLedgerOctave → LightPattern (Fin 8) → Prop)
    (hP : IsLedgerTopologyOnlyParent P)
    (octave : Q3SettledLedgerOctave)
    (hfactor :
      P octave
        (scalePattern
          (primitivePositiveStationaryFactorAmplitude
            (worldlinePattern gapOneTwoPhaseMode))
          (worldlinePattern gapOneTwoPhaseMode))) :
    ¬ ∀ (a : ℝ) (ha : 0 < a) (ψ : LightPattern (Fin 8)),
      P octave ψ →
        Q3MatterCarrier ψ →
          SettledAnchorWindow a ψ →
            PhotonWindowReadsPatternAnchor
                (originEmittedPhotonStateScaled octave a ha).window ψ →
              a = primitivePositiveStationaryFactorAmplitude ψ := by
  intro hall
  obtain ⟨a, ha, ψ, hparent, hcarrier, hwin, hread, hne⟩ :=
    exists_ledgerTopologyOnlyParent_doubledAmplitudeWitness
      P hP octave hfactor
  exact hne (hall a ha ψ hparent hcarrier hwin hread)
THEOREM ledgerTopologyOnlyParent_scaleInvariant · IndisputableMonolith/Masses/MassGenesis/T10LedgerTopologyAmplitudeForceWall.lean
ledgerTopologyOnlyParent_scaleInvariant · IndisputableMonolith/Masses/MassGenesis/T10LedgerTopologyAmplitudeForceWall.lean:41 
/-- Every ledger/topology-only parent is invariant under pattern rescaling. -/
theorem ledgerTopologyOnlyParent_scaleInvariant
    (P : Q3SettledLedgerOctave → LightPattern (Fin 8) → Prop)
    (hP : IsLedgerTopologyOnlyParent P)
    (octave : Q3SettledLedgerOctave)
    (c : ℝ) (ψ : LightPattern (Fin 8)) :
    P octave ψ ↔ P octave (scalePattern c ψ) :=
  hP octave ψ (scalePattern c ψ) rfl
THEOREM exists_ledgerTopologyOnlyParent_doubledAmplitudeWitness · IndisputableMonolith/Masses/MassGenesis/T10LedgerTopologyAmplitudeForceWall.lean
exists_ledgerTopologyOnlyParent_doubledAmplitudeWitness · IndisputableMonolith/Masses/MassGenesis/T10LedgerTopologyAmplitudeForceWall.lean:56 
/-- If a ledger/topology-only parent accepts the intended factor-scaled
gap-one witness, it also accepts a doubled sourced-emission witness whose
posting amplitude misses the topology factor. -/
theorem exists_ledgerTopologyOnlyParent_doubledAmplitudeWitness
    (P : Q3SettledLedgerOctave → LightPattern (Fin 8) → Prop)
    (hP : IsLedgerTopologyOnlyParent P)
    (octave : Q3SettledLedgerOctave)
    (hfactor :
      P octave
        (scalePattern
          (primitivePositiveStationaryFactorAmplitude
            (worldlinePattern gapOneTwoPhaseMode))
          (worldlinePattern gapOneTwoPhaseMode))) :
    ∃ (a : ℝ) (ha : 0 < a) (ψ : LightPattern (Fin 8)),
      P octave ψ ∧
        Q3MatterCarrier ψ ∧
          SettledAnchorWindow a ψ ∧
            PhotonWindowReadsPatternAnchor
                (originEmittedPhotonStateScaled octave a ha).window ψ ∧
              a ≠ primitivePositiveStationaryFactorAmplitude ψ := by
  let seed := worldlinePattern gapOneTwoPhaseMode
  let f := primitivePositiveStationaryFactorAmplitude seed
  let ground := scalePattern f seed
  let a := 2 * f
  let ψ := scalePattern 2 ground
  have hf : 0 < f := by
    simpa [f, seed] using gapOne_factorAmplitude_pos
  have ha : 0 < a := by
    exact mul_pos (by norm_num) hf
  obtain ⟨Eseed⟩ := q3MatterCarrier_worldlinePattern_gapOne
  have Eground : Q3ClosedPatternEvidence ground := by
    exact scalePattern_q3ClosedEvidence f hf Eseed
  have Eψ : Q3ClosedPatternEvidence ψ := by
    exact scalePattern_q3ClosedEvidence 2 (by norm_num) Eground
  have hgroundWin : SettledAnchorWindow f ground := by
    simpa [ground, f] using
      scalePattern_settledAnchor f worldlineGapOne_settledAnchor_unit
  have hwin : SettledAnchorWindow a ψ := by
    simpa [a, ψ] using scalePattern_settledAnchor 2 hgroundWin
  have hparent : P octave ψ := by
    have hground : P octave ground := by
      simpa [ground, f, seed] using hfactor
    exact
      (ledgerTopologyOnlyParent_scaleInvariant P hP octave 2 ground).mp
        hground
  have hread :
      PhotonWindowReadsPatternAnchor
        (originEmittedPhotonStateScaled octave a ha).window ψ := by
    unfold PhotonWindowReadsPatternAnchor
    simp [ψ, ground, a, f, seed,
      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] using
              primitivePositiveStationaryFactorAmplitude_scalePattern f seed
      _ = f := rfl
  have hne : a ≠ primitivePositiveStationaryFactorAmplitude ψ := by
    rw [hfactorψ]
    intro heq
    dsimp [a] at heq
    nlinarith
  exact ⟨a, ha, ψ, hparent, ⟨Eψ⟩, hwin, hread, hne⟩
THEOREM amplitudeForcingParent_not_ledgerTopologyOnly · IndisputableMonolith/Masses/MassGenesis/T10LedgerTopologyAmplitudeForceWall.lean
amplitudeForcingParent_not_ledgerTopologyOnly · IndisputableMonolith/Masses/MassGenesis/T10LedgerTopologyAmplitudeForceWall.lean:151 
/-- Exact theorem boundary: any parent that really forces the scaled posting
amplitude and accepts the intended witness cannot be ledger/topology-only.
Lower-level provenance remains a separate campaign admission condition. -/
theorem amplitudeForcingParent_not_ledgerTopologyOnly
    (P : Q3SettledLedgerOctave → LightPattern (Fin 8) → Prop)
    (octave : Q3SettledLedgerOctave)
    (hfactor :
      P octave
        (scalePattern
          (primitivePositiveStationaryFactorAmplitude
            (worldlinePattern gapOneTwoPhaseMode))
          (worldlinePattern gapOneTwoPhaseMode)))
    (hforces :
      ∀ (a : ℝ) (ha : 0 < a) (ψ : LightPattern (Fin 8)),
        P octave ψ →
          Q3MatterCarrier ψ →
            SettledAnchorWindow a ψ →
              PhotonWindowReadsPatternAnchor
                  (originEmittedPhotonStateScaled octave a ha).window ψ →
                a = primitivePositiveStationaryFactorAmplitude ψ) :
    ¬ IsLedgerTopologyOnlyParent P := by
  intro hP
  exact
    (ledgerTopologyOnlyParent_does_not_force_amplitude
      P hP octave hfactor) hforces

What this page does not claim

The theorem does not claim that the posting amplitude is unforced, only that this route cannot force it. The theorem does not claim that the doubled witness is physically realized, only that it is consistent with every ledger and topology condition. The theorem does not claim that the settled ledger and topology are irrelevant, only that they are insufficient by themselves.

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