Masses Mass Genesis T10 Settlement Law Derivation

The settlement law

A ledger, a discrete record of events over time, must show when a commitment is occupied and when it is cleared. The T10 settlement law derivation in the Recognition Science framework proves that any local rule for posting these events, satisfying three plain conditions, must be the same rule: post +1 when a commitment begins, post -1 when it ends, and post nothing otherwise. This is the occupy-then-clear derivative, and the framework's machine-checked library of formal theorems proves it is the unique such rule.

The three conditions are forced by the ledger's own structure. First, a vacuum state, where no commitment is active, posts nothing. Second, the tick at which a commitment begins posts the unit amplitude, +1. Third, over a full settled commitment, the posted window is neutral, meaning the ledger balances to zero. Any rule with one-tick memory, seeing only the current and previous occupation states, that satisfies these three conditions must equal the occupy-then-clear derivative at every phase of the eight-tick cycle. The framework proves this uniqueness in its library, and also proves that the difference rule, amplitude = now - previous, is a member of this class, so the class is nonempty.

The derivation also shows that the occupation window itself is carried, not modeled. On any settled ledger octave, the global ledger-parity phase readout, already a theorem, determines which commitment the run is settling at each tick. The indicator that the run is at a given commitment's Gray vertex is therefore a readout of the actual legal run, and it equals the modeled occupation window at every phase. This means the settlement law is not an assumption about how the ledger behaves; it is forced by the ledger's own records.

Finally, the settlement windows form a single orbit under the cyclic shift operator Rhat. One Rhat step carries each settlement 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, the same freedom already proved as Rhat-orbit nonuniqueness. What remains genuinely open is only a clock-fixing law, if one exists at all.

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

/-- **The modeled occupation is the carried one.** On every settled legal
octave the ledger-parity readout returns the trajectory phase, so the
carried occupation indicator equals `commitOccupationWindow` exactly. -/
theorem ledgerOccupationWindow_eq_commitOccupation
    (octave : Q3SettledLedgerOctave) (phase : Fin 8) :
    ledgerOccupationWindow octave phase = commitOccupationWindow phase := by
  funext t
  unfold ledgerOccupationWindow commitOccupationWindow
  rw [q3PhaseOfLedgerParity_tracks_settledOctave octave.settlement t]

/-- **Anchor claim, orbit form (negative half).** No commitment's settled
window lies in the gap-two Rhat class. -/
theorem commitSettlementWindow_rhatClass_ne_gapTwo (phase : Fin 8) :
    Quotient.mk rhatOrbitSetoid (commitSettlementWindow phase) ≠
      Quotient.mk rhatOrbitSetoid gapTwoTwoPhaseMode := by
  rw [commitSettlementWindow_rhatClass_eq_gapOne]
  exact gapOne_rhatQuotient_ne_gapTwo

What this page does not claim

The settlement law derivation does not prove the existence of a clock-fixing law. The uniqueness result does not apply to rules with more than one tick of memory. The framework does not claim the ledger's occupation window is modeled rather than carried.

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: