Masses Mass Genesis T10 Run History Scale Coupling Boundary Run Pattern Scale Co

The boundary on run-only filters

In the Recognition Science framework, a ledger (a discrete record of posted events) carries two kinds of data when it is read out as a signal: an exact settled octave of eight ticks, and a freely chosen positive amplitude with a pattern read at that amplitude. A run-only filter (a rule that accepts or rejects a carrier based only on the settled octave, ignoring the amplitude) sounds like a reasonable simplification. The theorem runPatternScaleCouplingInterface_not_runOnly closes that door.

What is proved is a negative boundary. Suppose a run-only filter accepts the intended gap-one factor carrier, the standard readout at its topology-factor amplitude. Because the filter ignores amplitude, it must also accept the doubled carrier, the phi-scaled carrier, and the inverse-phi-scaled carrier: all four share the identical settled ledger octave. But the framework's ground-state selection requirement, called RecognitionGroundStateSelection, demands that the induced realization class not contain all these scale decoys. The theorem shows that any run-only filter accepting the intended carrier necessarily violates that requirement already at the doubled carrier. The proof is short: the filter accepts the doubled carrier, and accepting a carrier realizes its pattern, which the ground-state rule forbids.

The declaration also defines the exact boundary for a surviving coupling. RunPatternScaleCouplingInterface is a four-witness admission interface: a filter that accepts the intended carrier but rejects the patterns of all three scale decoys. The theorem proves that any filter meeting this interface is not run-only. This is the precise sense in which a lawful coupling must depend on the amplitude, not just on the ledger history.

What the theorem does not claim is just as important. No filter satisfying the interface is constructed or assumed to exist. The module does not derive the R4 requirement, does not assume a selector, and does not identify a lawful order-sensitive observable. It only closes the proposal to filter the present free-amplitude readout by a property of the ledger run alone. The interface records witness behavior only; it does not certify that the predicate P has independent physical ancestry, nor that its definition avoids factor posting, loadRecognitionCost = 0, or an equivalent predicate. Those are intensional provenance requirements that must be audited separately for any future construction.

The practical consequence is a clean separation of concerns. The framework has proved that the run-only idea fails at a specific, checkable point, and it has recorded the exact shape of a coupling that could survive. Whether such a coupling exists remains open, and the theorem's status is a boundary result, not a construction.

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

What this page does not claim

No run-pattern coupling satisfying the interface is constructed or assumed to exist. The theorem does not derive the R4 requirement or assume a selector. The interface does not certify that the predicate has independent physical ancestry.

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: