Masses Mass Genesis T10 Run History Scale Coupling Boundary Rescaled Carrier Pre

Rescaling and the ledger

In the Recognition Science framework, a physical mass readout is a carrier: a package holding two kinds of data. One kind is the ledger, a discrete record of recognition events arranged in an exact settled octave, an eight-tick sequence that is fixed and meaningful. The other kind is a continuum amplitude, a positive real number, together with a pattern read at that amplitude. The framework treats the ledger as the physically forced content and the amplitude as a freely chosen display scale.

The theorem rescaledCarrier_preserves_ledger_run states exactly this separation. If you take any carrier and multiply its amplitude by any positive number, the theorem proves that the entire raw ordered ledger run, every state of the settled octave, remains identical. The formula is simple: for any positive scale s, the rescaled carrier's octave and run equal the original's, while the amplitude becomes s times the original and the pattern is transformed by the scale. This is proved by definitional equality, meaning the construction of the rescaled carrier is literally built to keep the ledger untouched.

This matters because it exposes a boundary. The framework is investigating whether a filter, a rule for accepting or rejecting carriers, can depend only on the ledger run. The theorem shows that any such run-only filter must give the same verdict on a carrier and its rescaled versions, including the doubled, phi-scaled, and inverse-phi-scaled carriers. Those three scale decoys share the identical ledger run, so a run-only filter cannot tell them apart. The framework proves that any filter accepting the intended carrier but rejecting these decoys fails a key consistency condition, RecognitionGroundStateSelection, already at the doubled carrier.

What the theorem does not claim is just as important. It does not construct or assume any actual coupling that would survive this test. The framework records a precise interface, RunPatternScaleCouplingInterface, describing what such a surviving coupling would have to do: accept the intended carrier while rejecting all three scale decoys. It proves that any filter meeting that interface is necessarily not run-only. But the interface itself is a proposal, not a construction. No such filter is built, no physical ancestry for the pattern is certified, and no lawful observable is identified. Those remain open targets for future work.

/-- Rescaling preserves every state of the carrier's raw ordered ledger run. -/
theorem rescaledCarrier_preserves_ledger_run
    (s : ℝ) (hs : 0 < s)
    (c : EmittedScaledSettledReadoutCarrier)
    (t : ℕ) :
    IndisputableMonolith.LedgerPostingAdjacency.run
        (rescaledCarrier s hs c).octave.initial
        (rescaledCarrier s hs c).octave.schedule t =
      IndisputableMonolith.LedgerPostingAdjacency.run
        c.octave.initial c.octave.schedule t :=
  rfl

/-- A run-only filter gives the same verdict before and after every positive joint rescaling. -/
theorem runOnly_rescaledCarrier_iff
    (P : EmittedScaledSettledReadoutCarrier → Prop)
    (hP : IsRunOnly P)
    (s : ℝ) (hs : 0 < s)
    (c : EmittedScaledSettledReadoutCarrier) :
    P c ↔ P (rescaledCarrier s hs c) :=
  hP c (rescaledCarrier s hs c) rfl

/-- 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. The theorem does not derive R4, assume a selector, or identify a lawful order-sensitive unnormalized posting observable. The interface does not certify that the pattern 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: