Encyclopedia Masses Masses Mass Genesis T10 Settled Origin Decision

ARTICLE 4 claims 3 theorems 1 open

Masses Mass Genesis T10 Settled Origin Decision

A machine-checked proof chooses a relative, not absolute, starting point for phase in the framework's matter-formation chain, and states plainly what that choice does not claim.

The settled origin decision

Every settled legal octave, a discrete record of eight recognition events, already carries its own origin with phase zero. The framework proves this fact and then makes a decision about how far that origin can be trusted. The decision, called Branch B, accepts the carried origin as final for this rung of the framework's forced-matter closure. The proof is a certificate: a machine-checked collection of formal theorems, in this case a single structure that packages three facts together.

The first fact is the starting point itself: for any settled octave, the initial parity phase is zero. The second fact is what that zero implies for the settlement window: the commitment function applied to that zero phase yields gap-one mode, the first of the two-phase modes. The third fact is the scope of the claim. The certificate states that uniqueness and anchor support are relative to the carried run origin, not to any observer-free absolute phase naming. That third fact is the honest boundary of the whole decision.

Why does the boundary matter? The framework tried to find an observer-independent reindexing law that would preserve the physical settlement class and still force the same absolute anchor phases. The search did not yield a kernel-checked positive theorem from existing carriers. So the framework does not pretend the stronger claim holds. It states the weaker, provable claim: relative to the carried origin, the anchor position is fixed. Absolute observer-free phase naming remains outside the closed claim, an open target rather than a failure.

In plain language, the framework settles a question about where to start counting. It proves that every settled octave starts at zero, that this zero lands in the first settlement mode, and that the framework's guarantees about anchor position hold only relative to that carried starting point. The consequence is a stable foundation for the next rung of the matter-formation chain, with the limits of that stability written into the proof itself.

THEOREM settledOrigin_is_phaseZero · IndisputableMonolith/Masses/MassGenesis/T10SettledOriginDecision.lean
/-- Every settled legal octave's own origin reads phase zero. -/
theorem settledOrigin_is_phaseZero
    (octave : Q3SettledLedgerOctave) :
    q3PhaseOfLedgerParity octave.initial = 0 :=
  settledOctave_initial_phase_zero octave
THEOREM settledOrigin_commitSettlement_eq_gapOne · IndisputableMonolith/Masses/MassGenesis/T10SettledOriginDecision.lean
settledOrigin_commitSettlement_eq_gapOne · IndisputableMonolith/Masses/MassGenesis/T10SettledOriginDecision.lean:32
/-- Relative to the carried origin, the run-origin commitment settles exactly
gap-one. -/
theorem settledOrigin_commitSettlement_eq_gapOne
    (octave : Q3SettledLedgerOctave) :
    commitSettlementWindow (q3PhaseOfLedgerParity octave.initial) =
      gapOneTwoPhaseMode := by
  rw [settledOrigin_is_phaseZero octave,
    commitSettlementWindow_zero_eq_gapOne]
THEOREM CarriedSettledOriginFinalForm · IndisputableMonolith/Masses/MassGenesis/T10SettledOriginDecision.lean
/-- The final T10 origin claim for matter rigidity: anchor position is fixed
relative to the carried settled-octave indexing. This is Branch B of the
forced-matter closure plan. -/
structure CarriedSettledOriginFinalForm : Prop where
  every_settled_octave_origin_phase_zero :
    ∀ octave : Q3SettledLedgerOctave,
      q3PhaseOfLedgerParity octave.initial = 0
  run_origin_settlement_is_gap_one :
    ∀ octave : Q3SettledLedgerOctave,
      commitSettlementWindow (q3PhaseOfLedgerParity octave.initial) =
        gapOneTwoPhaseMode
  claim_scope :
    -- Uniqueness/anchor claims using this form are relative to the carried
    -- clock, not absolute observer-free phase naming.
    True

What this page does not claim

This framework does not prove that absolute observer-free phase naming is impossible, only that it is not derived here. No claim is made about the physical meaning of phase zero beyond its role in the carried indexing. The certificate does not establish the full matter-formation chain, only this rung's origin decision.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND