`AccountRS`

definition

show as: view math explainer →

module: IndisputableMonolith.LedgerPostingAdjacency
domain: LedgerPostingAdjacency
line: 35 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.LedgerPostingAdjacency on GitHub at line 35.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  32/-! ## A minimal recognition carrier: accounts = `Fin d` -/
  33
  34/-- Minimal carrier for a d-account ledger. The recognition relation is irrelevant here. -/
  35def AccountRS (d : Nat) : RecognitionStructure :=
  36  { U := Fin d, R := fun _ _ => True }
  37
  38/-!
  39### AtomicTick availability (Workstream B tightening)
  40
  41For the concrete carrier `Fin d` (with `d ≠ 0`), we can construct an `AtomicTick` instance
  42directly: at tick `t`, the posted account is the canonical `Fin d` coercion of `t`.
  43
  44Claim hygiene: this is a *model existence* theorem (THEOREM-level within Lean), not an empirical
  45claim about nature’s tick scheduling.
  46-/
  47
  48noncomputable instance accountRS_atomicTick (d : Nat) [NeZero d] : Recognition.AtomicTick (AccountRS d) :=
  49{ postedAt := fun t u =>
  50    u = ⟨t % d, Nat.mod_lt _ (Nat.pos_of_ne_zero (NeZero.ne d))⟩
  51  unique_post := by
  52    intro t
  53    refine ⟨⟨t % d, Nat.mod_lt _ (Nat.pos_of_ne_zero (NeZero.ne d))⟩, rfl, ?_⟩
  54    intro u hu
  55    simpa [hu]
  56}
  57
  58abbrev LedgerState (d : Nat) : Type := Recognition.Ledger (AccountRS d)
  59
  60abbrev phiVec {d : Nat} (L : LedgerState d) : Fin d → ℤ :=
  61  Recognition.phi L
  62
  63abbrev parity (d : Nat) (L : LedgerState d) : Pattern d :=
  64  parityPattern (phiVec (d := d) L)
  65

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.