Encyclopedia Masses Masses Mass Genesis T10 Posting Rate Verdict Canonical Octave Axis Balance Viola

ARTICLE 5 claims 5 theorems

Masses Mass Genesis T10 Posting Rate Verdict Canonical Octave Axis Balance Viola

A single theorem settles a dispute about how fast a ledger can change, but only by showing that two different meanings of "count" give two opposite answers.

Verify this page

The posting rate verdict

A ledger is a discrete record of events, and in Recognition Science the cost of recognition, the unavoidable price of preserving that record, is forced by a proved theorem. The declaration canonicalOctave_axisBalance_violates_onePostingPerTick is a machine-checked proof about one particular ledger run, the canonical settled octave. It shows that a specific readout of that ledger, the axis balance, changes by four units across the single tick that wraps the eight-tick cycle from step seven back to step zero. The theorem is a counterexample: it disproves the claim that this readout satisfies the bound called OnePostingPerTick, which says the standing count changes by at most one unit per tick.

The proof is short and computational. The axis balance at step zero is 0, and at step seven it is 4, so the difference across the wrap is 4, which is not at most 1. The same module proves that every other step of the same run moves the balance by at most one unit. The only failure is the wrap. The reason is that the axis balance is a faithful count: it registers every post, and across the eight ticks of the cycle, eight posts occur, so the total must rise by eight. On a cyclic schedule of eight ticks, the wrap from seven back to zero must therefore carry the accumulated change of all eight steps at once, and no bound of one unit per tick can survive that.

The verdict splits on what the words "standing count" mean. The framework's committed readout is the parity-phase occupation, a two-valued indicator that is 1 when the ledger is in a given phase and 0 otherwise. Such an indicator changes by at most one unit per tick automatically, with no premises at all: parityPhaseOccupation_onePostingPerTick proves it for every run, settled or not. The theorem canonicalOctave_axisBalance_violates_onePostingPerTick does not touch that readout. It targets the axis balance, which is a faithful count, and for any faithful count the bound is false: no_faithfulCountReadout_onePostingPerTick proves that no readout that registers every post can satisfy the bound on any run of the eight-cycle.

What the declaration does not claim is as important as what it proves. It does not show that the framework's own ledger readout violates the bound; the committed readout satisfies it trivially. It does not derive a physical rate limit or a law of motion; it is a counterexample inside a formal model, not a statement about the world. And it does not close the open question of how matter windows identify their occupancy readout; that identification remains a target recorded elsewhere in the library. The theorem's role is diagnostic: it forces the framework to say which readout it means by "standing count", and it shows that the two natural meanings give opposite answers to the posting-rate question.

In Recognition Science, this matters because the posting-rate bound is part of the bridge from the ledger to settlement windows, the local readouts that the mass line consumes. The module that contains this theorem also proves the positive result: every commit settlement window is the integer coboundary of a two-valued occupancy at unit posting rate, and that shape is what the framework actually needs. The counterexample clears the ground by showing that the bound cannot be assumed for counts; it must be derived from two-valuedness, and the framework's library now says so explicitly.

THEOREM canonicalOctave_axisBalance_zero · canonicalOctave_axisBalance_seven · canonicalOctave_axisBalance_violates_onePostingPerTick · IndisputableMonolith/Masses/MassGenesis/T10PostingRateVerdict.lean
canonicalOctave_axisBalance_zero · IndisputableMonolith/Masses/MassGenesis/T10PostingRateVerdict.lean:419 
/-- The canonical octave starts balanced. -/
theorem canonicalOctave_axisBalance_zero :
    phiVec (run q3ZeroLedger q3GrayPostingSchedule 0) (0 : Fin 3) = 0 := by
  simp [run, phiVec, Recognition.phi, q3ZeroLedger]
canonicalOctave_axisBalance_seven · IndisputableMonolith/Masses/MassGenesis/T10PostingRateVerdict.lean:424 
/-- Axis zero of the canonical octave is posted four times over the first
seven steps, so its standing balance at tick seven is `4`. The `decide` here
evaluates schedule data and integer arithmetic only; the noncomputable `post`
is already telescoped away by `phiVec_run_eq`. -/
theorem canonicalOctave_axisBalance_seven :
    phiVec (run q3ZeroLedger q3GrayPostingSchedule 7) (0 : Fin 3) = 4 := by
  rw [phiVec_run_eq]
  decide
canonicalOctave_axisBalance_violates_onePostingPerTick · IndisputableMonolith/Masses/MassGenesis/T10PostingRateVerdict.lean:433 
/-- **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
THEOREM axisBalance_step_le_one · IndisputableMonolith/Masses/MassGenesis/T10PostingRateVerdict.lean
axisBalance_step_le_one · IndisputableMonolith/Masses/MassGenesis/T10PostingRateVerdict.lean:258 
/-- **The part `LegalAtomicTick` genuinely supplies.** Per step, the standing
balance of an axis moves at most one unit. Only the eight-cycle wrap fails
(section 4), because posts are monotone and never un-post. -/
theorem axisBalance_step_le_one (initial : LedgerState 3) (sched : ℕ → PostInstr 3)
    (t : ℕ) (k : Fin 3) :
    (phiVec (run initial sched t) k - phiVec (run initial sched (t + 1)) k).natAbs ≤ 1 := by
  rw [run_succ_eq_post]
  cases (sched t).2 with
  | debit =>
      rw [phiVec_post_debit]
      by_cases hk : k = (sched t).1
      · rw [if_pos hk]
        have h : phiVec (run initial sched t) k - (phiVec (run initial sched t) k + 1) = -1 :=
          by ring
        rw [h]
        decide
      · rw [if_neg hk, sub_self]
        exact Nat.zero_le 1
  | credit =>
      rw [phiVec_post_credit]
      by_cases hk : k = (sched t).1
      · rw [if_pos hk]
        have h : phiVec (run initial sched t) k - (phiVec (run initial sched t) k - 1) = 1 :=
          by ring
        rw [h]
        decide
      · rw [if_neg hk, sub_self]
        exact Nat.zero_le 1
THEOREM no_faithfulCountReadout_onePostingPerTick · IndisputableMonolith/Masses/MassGenesis/T10PostingRateVerdict.lean
no_faithfulCountReadout_onePostingPerTick · IndisputableMonolith/Masses/MassGenesis/T10PostingRateVerdict.lean:306 
/-- **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
THEOREM parityPhaseOccupation_onePostingPerTick · IndisputableMonolith/Masses/MassGenesis/T10PostingRateVerdict.lean
parityPhaseOccupation_onePostingPerTick · IndisputableMonolith/Masses/MassGenesis/T10PostingRateVerdict.lean:182 
/-- **The committed occupation satisfies the rate bound on every run, with no
premise.** Legality is never used: an indicator is two-valued, so its change
across any tick, including the cyclic wrap, is at most one. The theorem is
DERIVED in form and DEFINITIONAL in content. -/
theorem parityPhaseOccupation_onePostingPerTick (initial : LedgerState 3)
    (schedule : ℕ → PostInstr 3) (phase : Fin 8) :
    OnePostingPerTick (parityPhaseOccupation initial schedule phase) :=
  onePostingPerTick_of_twoValued (a := 0) (b := 1) (by decide)
    (parityPhaseOccupation_twoValued initial schedule phase)
THEOREM commitSettlementWindow_is_unitRateIntCoboundary · IndisputableMonolith/Masses/MassGenesis/T10PostingRateVerdict.lean
commitSettlementWindow_is_unitRateIntCoboundary · IndisputableMonolith/Masses/MassGenesis/T10PostingRateVerdict.lean:134 
/-- **The bridge in the mass line's own vocabulary.** Each commit settlement
window is the integer coboundary of a two-valued occupancy whose posting rate
is one, with no premise: the occupancy takes values in `{0, -1}`. This is the
shape `DoubleEntrySettledPattern` and `booleanWindow_of_onePostingPerTick`
consume. -/
theorem commitSettlementWindow_is_unitRateIntCoboundary (phase : Fin 8) :
    ∃ p : Fin 8 → ℤ,
      (∀ t : Fin 8, commitSettlementWindow phase t = ((p t - p (t + 1) : ℤ) : ℂ)) ∧
      OnePostingPerTick p := by
  refine ⟨fun t => -(commitIntOccupation phase (t - 1)), fun t => ?_, ?_⟩
  · have h1 : t + 1 - 1 = t := sub_eq_iff_eq_add.mpr rfl
    show commitSettlementWindow phase t =
      ((-commitIntOccupation phase (t - 1) - -commitIntOccupation phase (t + 1 - 1) : ℤ) : ℂ)
    unfold commitSettlementWindow
    rw [← commitIntOccupation_cast phase t, ← commitIntOccupation_cast phase (t - 1),
      h1]
    push_cast
    ring
  · refine onePostingPerTick_of_twoValued (a := 0) (b := -1) (by decide) fun t => ?_
    show -(commitIntOccupation phase (t - 1)) = 0 ∨
      -(commitIntOccupation phase (t - 1)) = -1
    unfold commitIntOccupation
    by_cases h : t - 1 = phase <;> simp [h]

What this page does not claim

The framework's own committed readout violates the posting-rate bound; it satisfies it trivially. A physical rate limit or law of motion is derived; the theorem is a counterexample inside a formal model. The matter-window occupancy identification is closed; it remains an open target.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND