Masses Mass Genesis T10 Posting Rate Verdict Parity Phase Occupation Cast Eq Led

The occupancy readout

In the Recognition Science framework, a ledger is a discrete record of events, and its occupancy is a readout of how full it is at a given moment. The declaration parityPhaseOccupation_cast_eq_ledgerOccupationWindow proves that the occupancy readout the theory commits to is exactly the two-valued indicator called parityPhaseOccupation: at each of the eight ticks in a cycle, this readout is either 0 or 1, depending on whether the ledger's parity state matches a chosen phase. This is a theorem in the machine-checked library of formal theorems, and it holds for every settled octave, which is a completed eight-tick cycle of the ledger.

The content of this theorem is definitional rather than derived. The readout is defined to be two-valued, so the theorem merely confirms that this definition matches the ledger occupation window used elsewhere in the framework. It does not derive this identification from deeper principles. The proof is a direct unfolding of definitions, with no premises about legal atomic ticks or any other constraints. This means the theorem excludes nothing that the two-valued readout did not already exclude: it cannot distinguish between one posting per tick and an occupation that alternates 0 and 1 every tick, both of which would be called unit rate.

The theorem is part of a larger verdict about posting rates. A separate theorem proves that any faithful count readout, one that registers every posting, violates the one-posting-per-tick bound over the cyclic wrap of an eight-tick cycle. The concrete balance readout of the canonical settled octave violates it by computation, moving four units across the wrap. The posting rate verdict certifies that the committed occupancy readout satisfies the bound vacuously, while every faithful count readout fails it. The missing piece is not a rate but an identification: for matter windows, the identification of the standing count with the two-valued parity-phase occupation remains open.

The theorem does not claim that the parity-phase occupation is the only possible readout, nor that it is physically forced. It does not claim that the one-posting-per-tick bound is derived from the ledger dynamics; the bound is automatic for the two-valued readout and false for faithful counts. It does not claim that the matter-window identification is closed; that remains an open gap recorded in the framework. The theorem's role is to make explicit that the committed readout is two-valued, and that this two-valuedness is what supplies the posting-rate bridge, not a modeled rate.

/-- The integer readout casts to the tree's committed carried occupation. -/
theorem parityPhaseOccupation_cast_eq_ledgerOccupationWindow
    (octave : Q3SettledLedgerOctave) (phase : Fin 8) (t : Fin 8) :
    ((parityPhaseOccupation octave.initial octave.schedule phase t : ℤ) : ℂ) =
      ledgerOccupationWindow octave phase t := by
  unfold parityPhaseOccupation ledgerOccupationWindow
  by_cases h : q3PhaseOfLedgerParity (run octave.initial octave.schedule t.val) = phase <;>
    simp [h]

/-- The integer readout casts to the tree's committed carried occupation. -/
theorem parityPhaseOccupation_cast_eq_ledgerOccupationWindow
    (octave : Q3SettledLedgerOctave) (phase : Fin 8) (t : Fin 8) :
    ((parityPhaseOccupation octave.initial octave.schedule phase t : ℤ) : ℂ) =
      ledgerOccupationWindow octave phase t := by
  unfold parityPhaseOccupation ledgerOccupationWindow
  by_cases h : q3PhaseOfLedgerParity (run octave.initial octave.schedule t.val) = phase <;>
    simp [h]

/-- **No faithful standing count satisfies the cyclic rate bound.** Over seven
steps the count rises by seven, so the wrap tick alone moves seven units. This
is the sharp half of the verdict: the bound is not merely underived for
counts, it is false. -/
theorem no_faithfulCountReadout_onePostingPerTick (r : LedgerState 3 → ℤ)
    (hf : FaithfulCountReadout r) (initial : LedgerState 3) (sched : ℕ → PostInstr 3) :
    ¬ OnePostingPerTick (fun t : Fin 8 => r (run initial sched t.val)) := by
  intro hrate
  have hstep : (r (run initial sched (7 : Fin 8).val) -
      r (run initial sched ((7 : Fin 8) + 1).val)).natAbs ≤ 1 := hrate (7 : Fin 8)
  have hwrapval : ((7 : Fin 8) + 1).val = 0 := by decide
  have hv7 : (7 : Fin 8).val = 7 := by decide
  rw [hwrapval, hv7] at hstep
  rw [faithfulCountReadout_run r hf initial sched 7,
    faithfulCountReadout_run r hf initial sched 0] at hstep
  have hdiff : r initial + ((7 : ℕ) : ℤ) - (r initial + ((0 : ℕ) : ℤ)) = 7 := by
    push_cast
    ring
  rw [hdiff] at hstep
  exact (by decide : ¬ ((7 : ℤ).natAbs ≤ 1)) hstep

/-- **The countermodel.** The library's canonical settled legal octave, read
by the standing balance of axis zero, violates the cyclic posting-rate bound:
the wrap tick compares a balance of `4` against a balance of `0`. So the bound
is false, not merely underived, for the integer "standing count" reading,
already on the one settled octave the library exhibits. -/
theorem canonicalOctave_axisBalance_violates_onePostingPerTick :
    ¬ OnePostingPerTick (axisBalanceOccupation q3ZeroLedger q3GrayPostingSchedule 0) := by
  intro hrate
  have hstep : (phiVec (run q3ZeroLedger q3GrayPostingSchedule (7 : Fin 8).val) 0 -
      phiVec (run q3ZeroLedger q3GrayPostingSchedule ((7 : Fin 8) + 1).val) 0).natAbs ≤ 1 :=
    hrate (7 : Fin 8)
  have hwrapval : ((7 : Fin 8) + 1).val = 0 := by decide
  have hv7 : (7 : Fin 8).val = 7 := by decide
  rw [hwrapval, hv7, canonicalOctave_axisBalance_seven,
    canonicalOctave_axisBalance_zero] at hstep
  exact (by decide : ¬ ((4 : ℤ) - 0).natAbs ≤ 1) hstep

What this page does not claim

The parity-phase occupation is the only possible readout of the ledger. The one-posting-per-tick bound is derived from the ledger dynamics rather than being automatic for the two-valued readout. The matter-window identification is closed; it remains an open gap in the framework.

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