Masses Mass Genesis T10 Directed Posting Run Scale Wall Settled Schedule Account

The settled schedule account

The declaration settled_schedule_account_eq_grayPhaseAxis3 is a theorem about a discrete record of events, a ledger. It concerns a settled schedule, a fixed, repeating sequence of eight posting instructions that move value between accounts. The theorem states that for any such schedule, the first component of the instruction at each of its eight phases is exactly equal to a predetermined spatial axis, called grayPhaseAxis3. In plain terms, the theorem proves that the ledger's schedule is not arbitrary: each of its eight steps is tied to a specific one of three spatial directions, and that tie is forced by the structure of the ledger itself.

This is a precise, machine-checked result. The theorem is part of a larger campaign to understand how the framework's core concepts, like cost and recognition, might generate the masses of elementary particles. The theorem about the schedule account is a necessary step in that campaign, but it is only a step. It establishes a structural fact about the ledger's internal organization, not a physical law about particles. The framework's library proves this fact, but the library does not claim that this fact alone explains mass. The connection between the ledger's schedule and the actual masses of particles remains an open problem, a target for future work.

What the theorem does not claim is as important as what it proves. It does not claim that the schedule account itself determines any physical quantity, like a particle's mass or charge. It does not claim that the spatial axis it identifies is the same as a physical direction in space. The theorem is about the ledger's internal structure, not about the external world. Also, the theorem does not claim that the ledger's schedule is the only possible schedule, or that the grayPhaseAxis3 is the only possible set of axes. It proves a specific equality, and that is all.

/-- Settlement forces the account instruction, not merely the parity image. -/
theorem settled_schedule_account_eq_grayPhaseAxis3
    (octave : Q3SettledLedgerOctave) (phase : Fin 8) :
    (octave.schedule phase.val).1 = grayPhaseAxis3 phase := by
  have hrun :
      parity 3
          (run octave.initial octave.schedule (phase.val + 1)) =
        flipAt
          (parity 3 (run octave.initial octave.schedule phase.val))
          (octave.schedule phase.val).1 := by
    rw [run_succ_eq_post, parity_post_eq_flipAt]
  have hdiff :
      q3VertexAtPhase phase (octave.schedule phase.val).1 ≠
        q3VertexAtPhase (phase + 1)
          (octave.schedule phase.val).1 := by
    rw [← octave.settlement.1 phase,
      ← settled_next_parity octave phase,
      hrun, flipAt_apply_self]
    intro h
    exact Bool.not_ne_self _ h.symm
  unfold grayPhaseAxis3
  exact
    (Classical.choose_spec
      (Patterns.grayCycle3_oneBit_step phase)).2
        (octave.schedule phase.val).1
        (by simpa [q3VertexAtPhase] using hdiff)

What this page does not claim

The theorem does not claim that the schedule account determines any physical quantity, such as a particle's mass or charge. The theorem does not claim that the grayPhaseAxis3 axes correspond to physical directions in space. The theorem does not claim that the settled schedule is the only possible schedule for the ledger.

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