Masses Mass Genesis T10 Run History Scale Coupling Boundary Run Only Carrier Rea

The run-only boundary

In the Recognition Science account of mass generation, an emitted carrier is a data packet with two separate parts: a settled ledger, a discrete record of past recognition events, and a freely chosen positive amplitude that scales a continuum pattern. The question at stake is whether a filter, a rule for accepting or rejecting carriers, may look only at the ledger run and ignore the amplitude. The declaration runOnly_carrierRealized_violates_r4 answers no, and it does so by a forced contradiction.

The proof starts with a carrier displayed at its intended gap-one factor amplitude. A run-only filter that accepts this carrier must, by definition, give the same verdict on any carrier with an identical settled ledger octave. Positive joint rescaling preserves that octave exactly, while multiplying the amplitude and scaling the pattern. So the filter must also accept the doubled carrier, the phi-scaled carrier, and the inverse-phi-scaled carrier. Each of these carries a different pattern, and the induced realization class, the set of patterns the filter permits, therefore contains all four. That class violates RecognitionGroundStateSelection, the requirement that the ground state be selected uniquely, already at the doubled carrier. The theorem is proved in the machine-checked library of formal theorems with no axioms beyond the standard three.

What the declaration does not claim is just as important. It does not construct a surviving coupling that uses both the ledger run and the pattern. The library states an interface, a set of four witness behaviors such a coupling must exhibit, and proves that any filter meeting that interface is not run-only. But no filter satisfying the interface is built or assumed. The interface records witness behavior only; it does not certify that the pattern predicate has independent physical ancestry, nor that its definition avoids factor posting, zero load recognition cost, or an equivalent predicate. Those are intensional provenance requirements, audited separately for any future construction.

The boundary is therefore precise: a run-only filter is closed off as a proposal, and the exact shape of what must replace it is recorded, but the replacement itself remains open. The consequence is that mass pattern readout in this framework cannot be a pure function of the settled ledger run alone; it must couple to the free amplitude in a way that the interface names but does not yet realize.

/-- A run-only filter accepting the intended carrier accepts all three scale decoys. -/
theorem runOnly_accepts_doubled_phi_inversePhi
    (P : EmittedScaledSettledReadoutCarrier → Prop)
    (hP : IsRunOnly P)
    (octave : Q3SettledLedgerOctave)
    (hintended : P (intendedGapOneFactorCarrier octave)) :
    P (doubledCarrier (intendedGapOneFactorCarrier octave)) ∧
      P (phiScaledCarrier (intendedGapOneFactorCarrier octave)) ∧
        P (inversePhiScaledCarrier
          (intendedGapOneFactorCarrier octave)) := by
  have hdoubled :
      P (doubledCarrier (intendedGapOneFactorCarrier octave)) :=
    (runOnly_doubledCarrier_iff
      P hP (intendedGapOneFactorCarrier octave)).mp hintended
  have hphi :
      P (phiScaledCarrier (intendedGapOneFactorCarrier octave)) := by
    exact
      (runOnly_rescaledCarrier_iff
        P hP Constants.phi Constants.phi_pos
        (intendedGapOneFactorCarrier octave)).mp hintended
  have hinverse :
      P (inversePhiScaledCarrier
        (intendedGapOneFactorCarrier octave)) := by
    exact
      (runOnly_rescaledCarrier_iff
        P hP
        (Constants.phi⁻¹)
        (inv_pos.mpr Constants.phi_pos)
        (intendedGapOneFactorCarrier octave)).mp hintended
  exact ⟨hdoubled, hphi, hinverse⟩

/-- The class induced by any run-only filter accepting the intended carrier fails R4 at the double. -/
theorem runOnly_carrierRealized_violates_r4
    (P : EmittedScaledSettledReadoutCarrier → Prop)
    (hP : IsRunOnly P)
    (octave : Q3SettledLedgerOctave)
    (hintended : P (intendedGapOneFactorCarrier octave)) :
    ¬ RecognitionGroundStateSelection (CarrierRealized P) := by
  have hdoubled :
      P (doubledCarrier (intendedGapOneFactorCarrier octave)) :=
    (runOnly_accepts_doubled_phi_inversePhi
      P hP octave hintended).1
  have hmem :
      CarrierRealized P
        (doubledCarrier (intendedGapOneFactorCarrier octave)).pattern :=
    carrierRealized_of_accepts hdoubled
  exact
    doubled_intended_carrier_violates_r4
      octave
      (CarrierRealized P)
      (by
        simpa only [intendedGapOneFactorCarrier] using hmem)

/-- Any carrier filter meeting the four-witness coupling interface is necessarily non-run-only. -/
theorem runPatternScaleCouplingInterface_not_runOnly
    (P : EmittedScaledSettledReadoutCarrier → Prop)
    (octave : Q3SettledLedgerOctave)
    (hgate : RunPatternScaleCouplingInterface P octave) :
    ¬ IsRunOnly P := by
  intro hrun
  have hdoubled :
      P (doubledCarrier (intendedGapOneFactorCarrier octave)) :=
    (runOnly_accepts_doubled_phi_inversePhi
      P hrun octave hgate.1).1
  exact hgate.2.1 (carrierRealized_of_accepts hdoubled)

/-- The four-witness admission interface for an unconstructed joint run-pattern coupling. -/
def RunPatternScaleCouplingInterface
    (P : EmittedScaledSettledReadoutCarrier → Prop)
    (octave : Q3SettledLedgerOctave) : Prop :=
  P (intendedGapOneFactorCarrier octave) ∧
    (¬ CarrierRealized P
      (doubledCarrier (intendedGapOneFactorCarrier octave)).pattern) ∧
    (¬ CarrierRealized P
      (phiScaledCarrier (intendedGapOneFactorCarrier octave)).pattern) ∧
    (¬ CarrierRealized P
      (inversePhiScaledCarrier
        (intendedGapOneFactorCarrier octave)).pattern)

What this page does not claim

A surviving run-pattern coupling is constructed. The pattern predicate has independent physical ancestry or avoids factor posting. The declaration derives R4 or assumes a selector.

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/T10RunHistoryScaleCouplingBoundary.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: