Masses Mass Genesis T10 Posting Rate Verdict

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

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

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