Masses Mass Genesis T10 Settlement Law Derivation Commit Settlement Window Rhat

The settlement window's orbit

In the Recognition Science framework, a ledger is a discrete record of recognition events, and a settlement window is the pattern of postings that closes out a commitment. The theorem commitSettlementWindow_rhatClass_eq_gapOne proves that every such window, at every one of the eight phases of the recognition cycle, belongs to the same orbit class under a cyclic shift operation, the class called gap-one. It never belongs to the gap-two class. The proof is a short chain: each window can be shifted cyclically until it equals the gap-one mode, and the gap-one and gap-two classes are distinct.

The result is not a definition or a modeling choice. It is a theorem proved in the framework's machine-checked library of formal theorems, with no framework-specific axioms. The theorem relies on earlier results that establish the settlement window's properties from the structure of a settled ledger octave. What it shows is a structural fact: the settlement family is a single orbit under the shift, and the position within that orbit is exactly the clock reading. This is the same freedom already proved as Rhat-orbit nonuniqueness.

What the theorem does not claim is that the clock-fixing law exists. The framework leaves open whether there is a law that selects one particular phase as the starting point. The theorem also does not claim that the gap-one class is physically preferred over gap-two in any empirical sense; it only proves that the settlement windows, as constructed, land in gap-one. The distinction between the two classes is structural, not a claim about which one nature uses.

/-- **Anchor claim, orbit form (positive half).** Every commitment's settled
window lies in the gap-one Rhat class: the settlement family IS the gap-one
orbit. -/
theorem commitSettlementWindow_rhatClass_eq_gapOne (phase : Fin 8) :
    Quotient.mk rhatOrbitSetoid (commitSettlementWindow phase) =
      Quotient.mk rhatOrbitSetoid gapOneTwoPhaseMode := by
  obtain ⟨m, hm⟩ := commitSettlementWindow_reaches_gapOne phase
  exact Quotient.sound ⟨m, 0, by simpa using hm⟩

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

/-- Finitely many Rhat steps carry every settlement window to gap-one. -/
theorem commitSettlementWindow_reaches_gapOne (phase : Fin 8) :
    ∃ m : ℕ,
      (RecognitionDynamics.cyclicShift^[m])
          (commitSettlementWindow phase) = gapOneTwoPhaseMode := by
  have h0 := shift_chain_zero
  have h1 := shift_chain_succ 0 0 h0
  have h2 := shift_chain_succ 1 (0 + 1) h1
  have h3 := shift_chain_succ 2 (0 + 1 + 1) h2
  have h4 := shift_chain_succ 3 (0 + 1 + 1 + 1) h3
  have h5 := shift_chain_succ 4 (0 + 1 + 1 + 1 + 1) h4
  have h6 := shift_chain_succ 5 (0 + 1 + 1 + 1 + 1 + 1) h5
  have h7 := shift_chain_succ 6 (0 + 1 + 1 + 1 + 1 + 1 + 1) h6
  fin_cases phase
  · exact ⟨0, h0⟩
  · exact ⟨1, h1⟩
  · exact ⟨2, h2⟩
  · exact ⟨3, h3⟩
  · exact ⟨4, h4⟩
  · exact ⟨5, h5⟩
  · exact ⟨6, h6⟩
  · exact ⟨7, h7⟩

/-- **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 theorem does not claim that a clock-fixing law exists. The theorem does not claim that the gap-one class is empirically preferred over gap-two. The theorem does not claim that the settlement window is the only possible local readout.

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: