17 receipts inline · 115 lines · pinned 22590365b7f4fd36 — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean ledger.lean prints nothing when every receipt passes
import Face
open Room Face
set_option autoImplicit false
namespace Ledger
def give (l : List (Nat × Nat)) (a b k : Nat) : List (Nat × Nat) :=
l.map (fun e => cond (Nat.beq e.1 a) (e.1, e.2 - k) (cond (Nat.beq e.1 b) (e.1, e.2 + k) e))
/-- info: 'Ledger.give' does not depend on any axioms -/
#guard_msgs in #print axioms give
def total : List (Nat × Nat) → Nat
| [] => 0
| e :: l => e.2 + total l
/-- info: 'Ledger.total' does not depend on any axioms -/
#guard_msgs in #print axioms total
def held (l : List (Nat × Nat)) (a : Nat) : Nat := total (l.filter (fun e => Nat.beq e.1 a))
/-- info: 'Ledger.held' does not depend on any axioms -/
#guard_msgs in #print axioms held
def totalFace : Face := ⟨List (Nat × Nat), Unit, Nat, fun l _ => total l⟩
/-- info: 'Ledger.totalFace' does not depend on any axioms -/
#guard_msgs in #print axioms totalFace
def seatsFace : Face := ⟨List (Nat × Nat), Nat, Nat, fun l a => held l a⟩
/-- info: 'Ledger.seatsFace' does not depend on any axioms -/
#guard_msgs in #print axioms seatsFace
def isaac : Nat := 1
/-- info: 'Ledger.isaac' does not depend on any axioms -/
#guard_msgs in #print axioms isaac
def abe : Nat := 2
/-- info: 'Ledger.abe' does not depend on any axioms -/
#guard_msgs in #print axioms abe
def rose : Nat := 3
/-- info: 'Ledger.rose' does not depend on any axioms -/
#guard_msgs in #print axioms rose
def books : List (Nat × Nat) := [(isaac, 10), (abe, 5), (rose, 0)]
/-- info: 'Ledger.books' does not depend on any axioms -/
#guard_msgs in #print axioms books
def afterGift : List (Nat × Nat) := give books isaac rose 4
/-- info: 'Ledger.afterGift' does not depend on any axioms -/
#guard_msgs in #print axioms afterGift
def afterTwo : List (Nat × Nat) := give afterGift rose abe 2
/-- info: 'Ledger.afterTwo' does not depend on any axioms -/
#guard_msgs in #print axioms afterTwo
def totalBefore : Nat := total books
/-- info: 'Ledger.totalBefore' does not depend on any axioms -/
#guard_msgs in #print axioms totalBefore
def totalAfter : Nat := total afterGift
/-- info: 'Ledger.totalAfter' does not depend on any axioms -/
#guard_msgs in #print axioms totalAfter
def totalAfterTwo : Nat := total afterTwo
#guard totalBefore == 15
#guard totalAfter == totalBefore
#guard totalAfterTwo == totalBefore
#guard held afterGift isaac == 6
#guard held afterGift rose == 4
#guard held afterGift abe == 5
#guard held afterTwo abe == 7
#guard held afterTwo rose == 2
#guard afterGift != books
/-- info: 'Ledger.totalAfterTwo' does not depend on any axioms -/
#guard_msgs in #print axioms totalAfterTwo
theorem the_gift_is_unheard_at_the_total : alike totalFace afterGift books :=
by (intro x; induction x; all_goals ((intros; rfl)))
/-- info: 'Ledger.the_gift_is_unheard_at_the_total' does not depend on any axioms -/
#guard_msgs in #print axioms the_gift_is_unheard_at_the_total
theorem the_gift_is_heard_at_a_seat : ¬ alike seatsFace afterGift books :=
fun h => absurd (h isaac) (by show ¬ (held afterGift isaac = held books isaac); decide)
/-- info: 'Ledger.the_gift_is_heard_at_a_seat' does not depend on any axioms -/
#guard_msgs in #print axioms the_gift_is_heard_at_a_seat
theorem the_handshake_at_the_books :
alike totalFace afterGift books ∧ ¬ alike seatsFace afterGift books ∧ alike totalFace afterTwo books :=
by
(intros; (repeat' constructor);
all_goals
(intros;
first
| (apply the_gift_is_unheard_at_the_total <;> fail)
| (apply the_gift_is_heard_at_a_seat <;> fail)))
/-- info: 'Ledger.the_handshake_at_the_books' does not depend on any axioms -/
#guard_msgs in #print axioms the_handshake_at_the_books
end Ledger
the vestibule — what the assay would say and cannot yet, each with what it waits on (assays/ledger.held); a stranger could answer one
a hand for the induction — the names apart, the giver and the taker distinct, the gift affordable
-- the vestibule of the ledger: a transfer between two seats keeps the total — the handshake at money, read
-- by bin/counter book. isaac's jotting (2026-10-02): money movement carries someone else's cognitive process,
-- an unknowably plural someone else; "time is money" as parameterization, a timestream a cashflow, and flow
-- dynamics hold. the house's reading: a charge is fuel one reader spent, spendable by any reader at the same
-- fingerprint, the payer dark (the memo's observer column was dropped because a memo need not know who paid);
-- the bill is the word; and conservation is a symmetry over who is holding, the Noether reading — a transfer
-- is unheard at the face whose one probe is the total and heard at the face whose probes are the seats.
-- the concrete rows are seated in the assay; what waits is the law in general.
-- held (waiting on: a hand for the induction — the names apart, the giver and the taker distinct, the gift affordable)
-- theorem the_gift_keeps_the_total (l : List (Nat × Nat)) (a b k : Nat) (hn : Apart (l.map (·.1))) (hab : a ≠ b)
-- (hk : Nat.ble k (held l a) = true) : total (give l a b k) = total l := sorry
-- theorem an_affordable_gift_is_unheard_at_the_total (a b k : Nat) (hab : a ≠ b) :
-- ∀ l, Apart (l.map (·.1)) → Nat.ble k (held l a) = true → totalFace.obs (give l a b k) () = totalFace.obs l () := sorry
the map of relations — every law a node, an arrow for each citation the elaborator reads (bin/counter chart; without --laws the carriers join the map)
graph LR
subgraph Ledger["Ledger"]
the_gift_is_heard_at_a_seat["the_gift_is_heard_at_a_seat"]
the_gift_is_unheard_at_the_total["the_gift_is_unheard_at_the_total"]
the_handshake_at_the_books["the_handshake_at_the_books"]
end
the_handshake_at_the_books --> the_gift_is_heard_at_a_seat
the_handshake_at_the_books --> the_gift_is_unheard_at_the_total
the data-model shadow — every structure a table, every seat a view over the columns its probes read, every wall theorem the policy it licenses (bin/counter schema)
-- the data-model shadow of grown/assays/ledger.lean, read from the kernel (bin/counter schema)
-- every foreign key is a field; every policy is a theorem; nothing here that the treaty does not need