Masses Mass Genesis T10 Settlement Law Derivation Local Settlement Readout Force

The settlement readout

A ledger, a discrete record of events, needs a rule for posting each tick's settlement: how much amplitude to write down at the moment a commitment is occupied, and how much to clear when it is vacated. The Recognition Science framework proves that on a settled ledger octave, this rule is forced. Any local settlement readout, a per-tick posting law that sees only the occupation now and at the previous tick, must produce exactly the same settlement window at every phase, for every settled octave. The theorem localSettlementReadout_forces_settlementWindow states this uniqueness result.

The readout's three constraints are plain. A vacuum, where nothing is occupied, posts nothing. A commit tick, where occupation goes from zero to one, posts the unit amplitude. And a settled commitment's posted window is neutral, meaning the ledger balances over the full cycle. The framework proves that these three facts, together with one-tick memory, force the readout to be the occupy-then-clear derivative: it posts +1 when a commitment is occupied, and -1 when it is cleared. The difference readout, defined as now - previous, satisfies all three constraints, so the class of such readouts is nonempty. The theorem is a uniqueness result, not an existence proof: it shows that any readout in the class must equal the settlement window, and the difference readout demonstrates the class is inhabited.

The framework's library, a machine-checked collection of formal theorems, derives this from carried structure rather than modeling it. The occupation window is not an assumption: on any settled ledger octave, the global ledger-parity phase readout already says which commitment the run is settling at each tick, so the indicator "the run is at this commitment's Gray vertex now" is a readout of the actual legal run. The difference form is likewise forced, not chosen. The proof shows the settlement family forms a single orbit under the Rhat operator: each physical Rhat step carries one phase's window to the previous phase's window, so every commitment's settled window lies in the gap-one Rhat class and never in the gap-two class. The family is injective in the phase, so the position inside the class is exactly the clock reading.

What the theorem does not claim matters. It does not claim that any particular readout is the right one in a physical sense; it proves that all readouts in the defined class agree. It does not claim that the settlement window is derived from nothing: the three constraints are the premises. And it does not claim that the clock itself is fixed. The position inside the Rhat orbit is a free parameter, the same freedom already proved as Rhat-orbit nonuniqueness. What remains open is only a clock-fixing law, if one exists at all. The theorem's consequence is that the settlement law is not a modeling choice but a forced structure, and the only remaining freedom is the phase, which is the clock.

/-- **The settlement law is forced.** Every local settlement readout,
applied to the occupation of any phase commitment, posts exactly the commit
settlement window: the occupy-then-clear difference is the unique local
neutral unit readout. -/
theorem localSettlementReadout_forces_settlementWindow
    (L : LocalSettlementReadout) (phase : Fin 8) :
    (fun t =>
        L.amplitude (commitOccupationWindow phase t)
          (commitOccupationWindow phase (t - 1))) =
      commitSettlementWindow phase := by
  funext t
  by_cases hcommit : t = phase
  · subst hcommit
    have hnow : commitOccupationWindow t t = 1 := if_pos rfl
    have hprevious : commitOccupationWindow t (t - 1) = 0 :=
      if_neg (fin8_sub_one_ne_self t)
    rw [hnow, hprevious, L.unit_at_commit,
      commitSettlementWindow_at_commit]
  · by_cases hclear : t = phase + 1
    · subst hclear
      have hnow : commitOccupationWindow phase (phase + 1) = 0 :=
        if_neg (fin8_add_one_ne_self phase)
      have hprevious : commitOccupationWindow phase (phase + 1 - 1) = 1 := by
        rw [add_sub_cancel_right]
        exact if_pos rfl
      rw [hnow, hprevious, L.clear_amplitude,
        commitSettlementWindow_at_clear]
    · have hnow : commitOccupationWindow phase t = 0 := if_neg hcommit
      have hprevious : commitOccupationWindow phase (t - 1) = 0 := by
        refine if_neg fun h => hclear ?_
        exact sub_eq_iff_eq_add.mp h
      rw [hnow, hprevious, L.vacuum_posts_nothing,
        commitSettlementWindow_adjacentPairSupport phase t hcommit hclear]

/-- The difference readout (post the change in occupation) is a local
settlement readout, so the class is inhabited. -/
def differenceSettlementReadout : LocalSettlementReadout where
  amplitude := fun now previous => now - previous
  vacuum_posts_nothing := by norm_num
  unit_at_commit := by norm_num
  neutral_on_settled_commitments := by
    intro octave phase
    simp only [ledgerOccupationWindow_eq_commitOccupation]
    exact commitSettlementWindow_neutral phase

/-- One physical Rhat step carries each settlement window to the previous
phase's settlement window: the family is closed under Rhat evolution. -/
theorem cyclicShift_commitSettlementWindow (phase : Fin 8) :
    RecognitionDynamics.cyclicShift
        (commitSettlementWindow (phase + 1)) =
      commitSettlementWindow phase := by
  funext t
  rw [cyclicShift_apply]
  by_cases hcommit : t = phase
  · subst hcommit
    rw [commitSettlementWindow_at_commit, commitSettlementWindow_at_commit]
  · by_cases hclear : t = phase + 1
    · subst hclear
      rw [commitSettlementWindow_at_clear, commitSettlementWindow_at_clear]
    · refine (commitSettlementWindow_adjacentPairSupport (phase + 1) (t + 1)
        (fun h => hcommit (add_right_cancel h))
        (fun h => hclear (add_right_cancel h))).trans
        (commitSettlementWindow_adjacentPairSupport phase t
          hcommit hclear).symm

/-- The position freedom is exactly the clock: distinct phases settle
distinct windows, so the window determines the commitment's clock phase. -/
theorem commitSettlementWindow_injective :
    Function.Injective commitSettlementWindow := by
  intro p q h
  by_contra hne
  have hp := congrFun h p
  rw [commitSettlementWindow_at_commit] at hp
  by_cases hclear : p = q + 1
  · rw [hclear, commitSettlementWindow_at_clear] at hp
    norm_num at hp
  · rw [commitSettlementWindow_adjacentPairSupport q p
      (fun hpq => hne hpq) hclear] at hp
    norm_num at hp

What this page does not claim

The theorem does not claim that any particular readout is physically preferred; it proves all readouts in the defined class agree. The theorem does not derive the settlement window from nothing; the three constraints are explicit premises. The theorem does not fix the clock phase; that remains an open problem.

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