here — a product as an assay, on Counter

190 receipts inline · 1427 lines · pinned a7922d2a684e4eed — shasum -a 256 of this file, cut to 16, as pins has it · lake env lean here.lean prints nothing when every receipt passes

import Witness
import Rest
import Threshold
import Counter
open Room Face Witness Rest Threshold
set_option autoImplicit false

-- ✦ Here. isaac, at the table (2026-09-15), in his words: "✦ X" means the spirit of X, and a spirit only exists
-- in the eye of the beholder — it exists for you iff you're synced up with it; what we call "Chat" is ✦ Here, an
-- active, streaming answer to "what's here?"; the workspace list is the list of ✦, each showing what that spirit
-- can show you about itself; ✦ Couple is missing, and dark — the space between the two of them, all we know is
-- that we gotta conduct it properly; the day-of is a sentence that concludes with every role paid and discharged
-- and lifted into the spirit of the couple's marriage, and the day-of is itself a door, transitioning everyone
-- into a world where that dark type is an ambient fact-of-the-world that everyone shares. the room is the one in
-- everyoneishere/docs/one-hop.sql: a presence is a human or a ✦; one relation, hears(a, b) — a receives what is
-- addressed to b; sees is one hop and speaks is an introduction, the same relation walked twice. so: the room is
-- a face whose probes are the presences and whose answer at a presence is what is addressed to it; a person's
-- seat is the presences they hear, themselves first; a ✦ is a probe, and it exists for a seat iff the seat hears
-- it; the narration is the room retold with the body forgotten; ✦ Couple is the one probe only the couple's seats
-- hear, which is a wall at every other seat and a door at the room.

namespace Here.Treaty

structure Message where
  id : Nat
  author : Nat
  to : List Nat
  body : Nat
  sent : Nat
  replyTo : List Nat
  askedOf : List Nat
  ackedBy : List (Nat × Nat)

/-- info: 'Here.Treaty.Message' does not depend on any axioms -/
#guard_msgs in #print axioms Message

structure Room where
  messages : List Message

/-- info: 'Here.Treaty.Room' does not depend on any axioms -/
#guard_msgs in #print axioms Room

def maya : Nat := 0

/-- info: 'Here.Treaty.maya' does not depend on any axioms -/
#guard_msgs in #print axioms maya

def james : Nat := 1

/-- info: 'Here.Treaty.james' does not depend on any axioms -/
#guard_msgs in #print axioms james

def ava : Nat := 2

/-- info: 'Here.Treaty.ava' does not depend on any axioms -/
#guard_msgs in #print axioms ava

def sofia : Nat := 3

/-- info: 'Here.Treaty.sofia' does not depend on any axioms -/
#guard_msgs in #print axioms sofia

def jordan : Nat := 4

/-- info: 'Here.Treaty.jordan' does not depend on any axioms -/
#guard_msgs in #print axioms jordan

def dana : Nat := 5

/-- info: 'Here.Treaty.dana' does not depend on any axioms -/
#guard_msgs in #print axioms dana

def linda : Nat := 6

/-- info: 'Here.Treaty.linda' does not depend on any axioms -/
#guard_msgs in #print axioms linda

def rose : Nat := 7

/-- info: 'Here.Treaty.rose' does not depend on any axioms -/
#guard_msgs in #print axioms rose

def everyone : Nat := 10

/-- info: 'Here.Treaty.everyone' does not depend on any axioms -/
#guard_msgs in #print axioms everyone

def vendors : Nat := 11

/-- info: 'Here.Treaty.vendors' does not depend on any axioms -/
#guard_msgs in #print axioms vendors

def seating : Nat := 12

/-- info: 'Here.Treaty.seating' does not depend on any axioms -/
#guard_msgs in #print axioms seating

def guests : Nat := 13

/-- info: 'Here.Treaty.guests' does not depend on any axioms -/
#guard_msgs in #print axioms guests

def invoicing : Nat := 14

/-- info: 'Here.Treaty.invoicing' does not depend on any axioms -/
#guard_msgs in #print axioms invoicing

def budget : Nat := 15

/-- info: 'Here.Treaty.budget' does not depend on any axioms -/
#guard_msgs in #print axioms budget

def site : Nat := 16

/-- info: 'Here.Treaty.site' does not depend on any axioms -/
#guard_msgs in #print axioms site

def couple : Nat := 17

/-- info: 'Here.Treaty.couple' does not depend on any axioms -/
#guard_msgs in #print axioms couple

def day : Nat := 18

/-- info: 'Here.Treaty.day' does not depend on any axioms -/
#guard_msgs in #print axioms day

def humans : List Nat := [maya, james, ava, sofia, jordan, dana, linda]

/-- info: 'Here.Treaty.humans' does not depend on any axioms -/
#guard_msgs in #print axioms humans

def lookup : List (Nat × List Nat) → Nat → List Nat
  | [], _ => []
  | (n, l) :: t, k => cond (Nat.beq n k) l (lookup t k)

/-- info: 'Here.Treaty.lookup' does not depend on any axioms -/
#guard_msgs in #print axioms lookup

def hearsTable : List (Nat × List Nat) :=
  [(maya, [everyone, seating, guests, invoicing, budget, site, couple, day]),
   (james, [everyone, seating, guests, invoicing, budget, site, couple, day]),
   (ava, [everyone, vendors, seating, guests, invoicing, budget, day]),
   (sofia, [everyone, vendors, seating, day]),
   (jordan, [everyone, vendors, seating, day]),
   (dana, [everyone, vendors, seating, day]),
   (linda, [everyone, seating, guests, day]),
   (everyone, humans),
   (vendors, [ava, sofia, jordan, dana]),
   (seating, [maya, james, ava, linda, dana]),
   (guests, [maya, james, ava, rose]),
   (invoicing, [sofia, jordan, dana]),
   (budget, [maya, james]),
   (site, [maya, james]),
   (couple, [maya, james]),
   (day, [maya, james, ava])]

/-- info: 'Here.Treaty.hearsTable' does not depend on any axioms -/
#guard_msgs in #print axioms hearsTable

def hearsOf (v : Nat) : List Nat := lookup hearsTable v

/-- info: 'Here.Treaty.hearsOf' does not depend on any axioms -/
#guard_msgs in #print axioms hearsOf

def seat (v : Nat) : List Nat := v :: hearsOf v

/-- info: 'Here.Treaty.seat' does not depend on any axioms -/
#guard_msgs in #print axioms seat

def heardAt (r : Room) (p : Nat) : List Message :=
  r.messages.filter (fun m => Nat.beq m.author p || enrolled Nat.beq m.to p)

/-- info: 'Here.Treaty.heardAt' does not depend on any axioms -/
#guard_msgs in #print axioms heardAt

def roomFace : Face := ⟨Room, Nat, List Message, heardAt⟩

/-- info: 'Here.Treaty.roomFace' does not depend on any axioms -/
#guard_msgs in #print axioms roomFace

def ids (ms : List Message) : List Nat := ms.map (·.id)

/-- info: 'Here.Treaty.ids' does not depend on any axioms -/
#guard_msgs in #print axioms ids

def bodies (ms : List Message) : List Nat := ms.map (·.body)

/-- info: 'Here.Treaty.bodies' does not depend on any axioms -/
#guard_msgs in #print axioms bodies

def inbox (v : Nat) (r : Room) : List Nat := joinMap ids (reads roomFace (seat v) r)

/-- info: 'Here.Treaty.inbox' does not depend on any axioms -/
#guard_msgs in #print axioms inbox

def sees (v : Nat) (r : Room) (m : Message) : Bool := enrolled Nat.beq (inbox v r) m.id

/-- info: 'Here.Treaty.sees' does not depend on any axioms -/
#guard_msgs in #print axioms sees

def introduced (p : Nat) : List Nat := earshot roomFace ((seat p).map seat)

/-- info: 'Here.Treaty.introduced' does not depend on any axioms -/
#guard_msgs in #print axioms introduced

def speaks (v p : Nat) : Bool := enrolled Nat.beq (introduced p) v

/-- info: 'Here.Treaty.speaks' does not depend on any axioms -/
#guard_msgs in #print axioms speaks

def shape (m : Message) : Nat × List Nat × Nat := (m.author, m.to, m.sent)

/-- info: 'Here.Treaty.shape' does not depend on any axioms -/
#guard_msgs in #print axioms shape

def narrate (ms : List Message) : List (Nat × List Nat × Nat) := ms.map shape

/-- info: 'Here.Treaty.narrate' does not depend on any axioms -/
#guard_msgs in #print axioms narrate

def narrationFace : Face := retell roomFace narrate

/-- info: 'Here.Treaty.narrationFace' does not depend on any axioms -/
#guard_msgs in #print axioms narrationFace

def humanOnly (m : Message) : Bool := enrolled Nat.beq humans m.author && m.to.all (enrolled Nat.beq humans)

/-- info: 'Here.Treaty.humanOnly' does not depend on any axioms -/
#guard_msgs in #print axioms humanOnly

def alone (m : Message) : Bool :=
  match m.to with
  | [] => false
  | [a] => Nat.beq a m.author
  | _ :: _ :: _ => false

/-- info: 'Here.Treaty.alone' does not depend on any axioms -/
#guard_msgs in #print axioms alone

def overheard (v : Nat) (r : Room) : List (Nat × List Nat × Nat) :=
  narrate (r.messages.filter (fun m => humanOnly m && !(alone m) && !(sees v r m)))

/-- info: 'Here.Treaty.overheard' does not depend on any axioms -/
#guard_msgs in #print axioms overheard

def onceEach : List Nat → List Message → List Message
  | _, [] => []
  | seen, m :: ms => cond (enrolled Nat.beq seen m.id) (onceEach seen ms) (m :: onceEach (m.id :: seen) ms)

/-- info: 'Here.Treaty.onceEach' does not depend on any axioms -/
#guard_msgs in #print axioms onceEach

def feedOf (rd : List (List Message)) : List Message := onceEach [] (joinMap (fun ms => ms) rd)

/-- info: 'Here.Treaty.feedOf' does not depend on any axioms -/
#guard_msgs in #print axioms feedOf

def feed (v : Nat) (r : Room) : List Message := feedOf (reads roomFace (seat v) r)

/-- info: 'Here.Treaty.feed' does not depend on any axioms -/
#guard_msgs in #print axioms feed

def edgeOf (lo hi : Nat) (rd : List (List Message)) : List Nat × List Nat :=
  (((feedOf rd).filter (fun m => Nat.blt m.sent lo)).map (·.sent), ((feedOf rd).filter (fun m => Nat.blt hi m.sent)).map (·.sent))

/-- info: 'Here.Treaty.edgeOf' does not depend on any axioms -/
#guard_msgs in #print axioms edgeOf

def edge (v lo hi : Nat) (r : Room) : List Nat × List Nat := edgeOf lo hi (reads roomFace (seat v) r)

/-- info: 'Here.Treaty.edge' does not depend on any axioms -/
#guard_msgs in #print axioms edge

def others : List Nat := [ava, sofia, jordan, dana, linda]

/-- info: 'Here.Treaty.others' does not depend on any axioms -/
#guard_msgs in #print axioms others

def otherSeats : List (List Nat) := others.map seat

/-- info: 'Here.Treaty.otherSeats' does not depend on any axioms -/
#guard_msgs in #print axioms otherSeats

def dock : Message := ⟨1, sofia, [vendors], 101, 900, [], [], []⟩

/-- info: 'Here.Treaty.dock' does not depend on any axioms -/
#guard_msgs in #print axioms dock

def time : Message := ⟨2, maya, [everyone], 102, 901, [], [sofia, jordan, dana], [(sofia, sofia), (jordan, jordan), (dana, ava)]⟩

/-- info: 'Here.Treaty.time' does not depend on any axioms -/
#guard_msgs in #print axioms time

def yes : Message := ⟨3, linda, [everyone], 103, 902, [], [], []⟩

/-- info: 'Here.Treaty.yes' does not depend on any axioms -/
#guard_msgs in #print axioms yes

def thread : Message := ⟨4, sofia, [maya, james], 104, 903, [], [], []⟩

/-- info: 'Here.Treaty.thread' does not depend on any axioms -/
#guard_msgs in #print axioms thread

def invS : Message := ⟨5, sofia, [invoicing], 105, 904, [], [], []⟩

/-- info: 'Here.Treaty.invS' does not depend on any axioms -/
#guard_msgs in #print axioms invS

def invJ : Message := ⟨6, jordan, [jordan], 106, 905, [], [], []⟩

/-- info: 'Here.Treaty.invJ' does not depend on any axioms -/
#guard_msgs in #print axioms invJ

def table : Message := ⟨7, dana, [seating], 107, 906, [], [], []⟩

/-- info: 'Here.Treaty.table' does not depend on any axioms -/
#guard_msgs in #print axioms table

def guest : Message := ⟨8, maya, [guests], 108, 907, [], [ava], []⟩

/-- info: 'Here.Treaty.guest' does not depend on any axioms -/
#guard_msgs in #print axioms guest

def budgetLine : Message := ⟨9, maya, [budget], 109, 908, [], [], []⟩

/-- info: 'Here.Treaty.budgetLine' does not depend on any axioms -/
#guard_msgs in #print axioms budgetLine

def siteLine : Message := ⟨10, maya, [site], 110, 909, [], [], []⟩

/-- info: 'Here.Treaty.siteLine' does not depend on any axioms -/
#guard_msgs in #print axioms siteLine

def ours : Message := ⟨11, maya, [couple], 111, 1705, [thread.id], [], []⟩

/-- info: 'Here.Treaty.ours' does not depend on any axioms -/
#guard_msgs in #print axioms ours

def theirs : Message := ⟨11, maya, [couple], 999, 1705, [thread.id], [], []⟩

/-- info: 'Here.Treaty.theirs' does not depend on any axioms -/
#guard_msgs in #print axioms theirs

def founding : Message := ⟨0, everyone, [everyone], 100, 800, [0], [], []⟩

/-- info: 'Here.Treaty.founding' does not depend on any axioms -/
#guard_msgs in #print axioms founding

def ceremony : Message := ⟨12, maya, [day], 1630, 1000, [], [], []⟩

/-- info: 'Here.Treaty.ceremony' does not depend on any axioms -/
#guard_msgs in #print axioms ceremony

def dinner : Message := ⟨13, ava, [day], 1800, 1001, [], [], []⟩

/-- info: 'Here.Treaty.dinner' does not depend on any axioms -/
#guard_msgs in #print axioms dinner

def demo : Room := ⟨[founding, dock, time, yes, thread, invS, invJ, table, guest, budgetLine, siteLine, ours, ceremony, dinner]⟩

/-- info: 'Here.Treaty.demo' does not depend on any axioms -/
#guard_msgs in #print axioms demo

def demo' : Room := ⟨[founding, dock, time, yes, thread, invS, invJ, table, guest, budgetLine, siteLine, theirs, ceremony, dinner]⟩

/-- info: 'Here.Treaty.demo'' does not depend on any axioms -/
#guard_msgs in #print axioms demo'

def coupleReads : List (List Nat) := (reads roomFace (seat maya) demo).map bodies

/-- info: 'Here.Treaty.coupleReads' does not depend on any axioms -/
#guard_msgs in #print axioms coupleReads

def lindaReads : List (List Nat) := (reads roomFace (seat linda) demo).map bodies

/-- info: 'Here.Treaty.lindaReads' does not depend on any axioms -/
#guard_msgs in #print axioms lindaReads

def lindaReads' : List (List Nat) := (reads roomFace (seat linda) demo').map bodies

/-- info: 'Here.Treaty.lindaReads'' does not depend on any axioms -/
#guard_msgs in #print axioms lindaReads'

def coupleReads' : List (List Nat) := (reads roomFace (seat maya) demo').map bodies

/-- info: 'Here.Treaty.coupleReads'' does not depend on any axioms -/
#guard_msgs in #print axioms coupleReads'

def hosted (w : List Nat) : List (List Nat) := (reads (host roomFace (List Nat)) (seat linda) (atTheDoor demo w)).map bodies

/-- info: 'Here.Treaty.hosted' does not depend on any axioms -/
#guard_msgs in #print axioms hosted

def lindaHears : List (Nat × List Nat × Nat) := overheard linda demo

/-- info: 'Here.Treaty.lindaHears' does not depend on any axioms -/
#guard_msgs in #print axioms lindaHears

def avaHears : List (Nat × List Nat × Nat) := overheard ava demo

/-- info: 'Here.Treaty.avaHears' does not depend on any axioms -/
#guard_msgs in #print axioms avaHears

def mayaHears : List (Nat × List Nat × Nat) := overheard maya demo

/-- info: 'Here.Treaty.mayaHears' does not depend on any axioms -/
#guard_msgs in #print axioms mayaHears

def sofiaHears : List (Nat × List Nat × Nat) := overheard sofia demo

/-- info: 'Here.Treaty.sofiaHears' does not depend on any axioms -/
#guard_msgs in #print axioms sofiaHears

def readTime : List Nat := humans.filter (fun v => sees v demo time)

/-- info: 'Here.Treaty.readTime' does not depend on any axioms -/
#guard_msgs in #print axioms readTime

def coupleInEarshot : Bool := enrolled Nat.beq (earshot roomFace otherSeats) couple

/-- info: 'Here.Treaty.coupleInEarshot' does not depend on any axioms -/
#guard_msgs in #print axioms coupleInEarshot

def narrated : List (List (Nat × List Nat × Nat)) := reads narrationFace (seat linda) demo

/-- info: 'Here.Treaty.narrated' does not depend on any axioms -/
#guard_msgs in #print axioms narrated

def narrated' : List (List (Nat × List Nat × Nat)) := reads narrationFace (seat linda) demo'

#guard sees maya demo dock == false
#guard sees maya demo guest
#guard sees maya demo budgetLine
#guard sees maya demo yes
#guard sees maya demo invS
#guard sees maya demo invJ == false
#guard sees sofia demo dock
#guard sees sofia demo budgetLine == false
#guard sees sofia demo guest == false
#guard sees sofia demo table
#guard sees sofia demo invJ == false
#guard sees sofia demo siteLine == false
#guard sees sofia demo thread
#guard sees linda demo dock == false
#guard sees linda demo invS == false
#guard sees linda demo budgetLine == false
#guard sees linda demo guest
#guard sees linda demo thread == false
#guard sees dana demo guest == false
#guard sees jordan demo invJ
#guard readTime == humans
#guard speaks sofia maya
#guard speaks sofia seating == false
#guard speaks linda guests == false
#guard speaks linda seating
#guard speaks dana seating
#guard speaks dana guests == false
#guard speaks rose guests
#guard speaks rose maya
#guard speaks rose vendors == false
#guard speaks sofia jordan
#guard speaks sofia budget == false
#guard sees maya demo ours
#guard sees james demo ours
#guard sees ava demo ours == false
#guard sees linda demo ours == false
#guard coupleInEarshot == false
#guard lindaHears == [shape thread]
#guard avaHears == [shape thread]
#guard mayaHears == []
#guard sofiaHears == []
#guard humanOnly invJ
#guard alone invJ
#guard alone thread == false
#guard (overheard linda demo).all (fun t => !(t == shape invJ))
#guard (overheard linda demo).all (fun t => !(t == shape ours))
#guard overheard linda demo == overheard linda demo'
#guard lindaReads == lindaReads'
#guard coupleReads != coupleReads'
#guard hosted [42] == hosted [43]
#guard hosted [42] == lindaReads
#guard narrated == narrated'
#guard edge linda 901 902 demo == edge linda 901 902 demo'
#guard edge linda 900 902 ⟨demo.messages.filter (fun m => !(Nat.beq m.id thread.id))⟩ == edge linda 900 902 demo
#guard (edge linda 900 902 demo).2.all (fun t => !(Nat.beq t thread.sent))
#guard enrolled Nat.beq (ids (feed sofia demo)) thread.id
#guard enrolled Nat.beq (ids (feed maya demo)) thread.id
#guard enrolled Nat.beq (ids (feed linda demo)) thread.id == false
#guard (edge sofia 900 902 demo).2 == [thread.sent, invS.sent, table.sent, ceremony.sent, dinner.sent]
#guard (ids (feed sofia demo)).length == 9

/-- info: 'Here.Treaty.narrated'' does not depend on any axioms -/
#guard_msgs in #print axioms narrated'

def acked (m : Message) : List Nat := m.ackedBy.map (·.1)

/-- info: 'Here.Treaty.acked' does not depend on any axioms -/
#guard_msgs in #print axioms acked

def decided (m : Message) : Bool := backed Nat.beq (acked m) m.askedOf

/-- info: 'Here.Treaty.decided' does not depend on any axioms -/
#guard_msgs in #print axioms decided

def openEnds (m : Message) : Nat := lacking Nat.beq (acked m) m.askedOf

/-- info: 'Here.Treaty.openEnds' does not depend on any axioms -/
#guard_msgs in #print axioms openEnds

def waitingOn (m : Message) : List Nat := m.askedOf.filter (fun n => !(enrolled Nat.beq (acked m) n))

/-- info: 'Here.Treaty.waitingOn' does not depend on any axioms -/
#guard_msgs in #print axioms waitingOn

def ackOf (of hand : Nat) (m : Message) : Message := { m with ackedBy := (of, hand) :: m.ackedBy }

/-- info: 'Here.Treaty.ackOf' does not depend on any axioms -/
#guard_msgs in #print axioms ackOf

def nagOf (of : Nat) (m : Message) : Message := { m with askedOf := of :: m.askedOf }

/-- info: 'Here.Treaty.nagOf' does not depend on any axioms -/
#guard_msgs in #print axioms nagOf

def ack (word of hand : Nat) (m : Message) : Message := cond (Nat.beq m.id word) (ackOf of hand m) m

/-- info: 'Here.Treaty.ack' does not depend on any axioms -/
#guard_msgs in #print axioms ack

def nag (word of : Nat) (m : Message) : Message := cond (Nat.beq m.id word) (nagOf of m) m

/-- info: 'Here.Treaty.nag' does not depend on any axioms -/
#guard_msgs in #print axioms nag

def onThePage (r : Room) : Bool := r.messages.all decided

/-- info: 'Here.Treaty.onThePage' does not depend on any axioms -/
#guard_msgs in #print axioms onThePage

def weightOf (r : Room) : Nat := (r.messages.map openEnds).sum

/-- info: 'Here.Treaty.weightOf' does not depend on any axioms -/
#guard_msgs in #print axioms weightOf

inductive Act where
  | say (m : Message)
  | ack (word of hand : Nat)
  | tick

/-- info: 'Here.Treaty.Act' does not depend on any axioms -/
#guard_msgs in #print axioms Act

def act (r : Room) : Act → Room
  | .say m => ⟨r.messages ++ [m]⟩
  | .ack word of hand => ⟨r.messages.map (ack word of hand)⟩
  | .tick => r

/-- info: 'Here.Treaty.act' does not depend on any axioms -/
#guard_msgs in #print axioms act

def dayMachine : Machine Act Room := ⟨Room, ⟨[]⟩, act, fun r => r⟩

/-- info: 'Here.Treaty.dayMachine' does not depend on any axioms -/
#guard_msgs in #print axioms dayMachine

def theDay : Runner Act Room := ⟨dayMachine, fun _ => .tick, onThePage⟩

/-- info: 'Here.Treaty.theDay' does not depend on any axioms -/
#guard_msgs in #print axioms theDay

def unsend (word : Nat) (r : Room) : Room := ⟨r.messages.filter (fun m => !(Nat.beq m.id word))⟩

/-- info: 'Here.Treaty.unsend' does not depend on any axioms -/
#guard_msgs in #print axioms unsend

def edgesOf (rd : List (List Message)) : List (Nat × Nat) :=
  joinMap (fun m => (m.replyTo.filter (fun o => enrolled Nat.beq (ids (feedOf rd)) o)).map (fun o => (m.id, o))) (feedOf rd)

/-- info: 'Here.Treaty.edgesOf' does not depend on any axioms -/
#guard_msgs in #print axioms edgesOf

def seenEdges (v : Nat) (r : Room) : List (Nat × Nat) := edgesOf (reads roomFace (seat v) r)

/-- info: 'Here.Treaty.seenEdges' does not depend on any axioms -/
#guard_msgs in #print axioms seenEdges

def dayAt (w : List Act) (fuel : Nat) : Option (List Nat) :=
  ((haltingGap Act Room).obs theDay (w, fuel)).map (fun r => r.messages.map openEnds)

/-- info: 'Here.Treaty.dayAt' does not depend on any axioms -/
#guard_msgs in #print axioms dayAt

def demoAcked : Room := act demo (.ack guest.id ava ava)

#guard decided time
#guard decided guest == false
#guard openEnds guest == 1
#guard waitingOn guest == [ava]
#guard onThePage demo == false
#guard weightOf demo == 1
#guard onThePage demoAcked
#guard decided (nag time.id sofia time)
#guard openEnds (nag time.id sofia time) == 0
#guard decided (ack guest.id ava ava guest)
#guard dayAt [] 0 == some []
#guard dayAt [.ack guest.id ava ava] 3 == some []
#guard (dayAt (demo.messages.map Act.say ++ [.ack guest.id ava ava]) 0).map List.sum == some 0
#guard dayAt (demo.messages.map Act.say) 5 == none
#guard weightOf (unsend guest.id demo) == 0
#guard (unsend time.id demo).messages.length + 1 == demo.messages.length
#guard enrolled Nat.beq (ids (feed maya demo)) founding.id
#guard (seenEdges maya demo).all (fun e => !(e == (ours.id, thread.id))) == false
#guard (seenEdges linda demo).all (fun e => !(e == (ours.id, thread.id)))
#guard (seenEdges linda demo).all (fun e => !(e == (founding.id, founding.id))) == false
#guard seenEdges linda demo == seenEdges linda demo'

/-- info: 'Here.Treaty.demoAcked' does not depend on any axioms -/
#guard_msgs in #print axioms demoAcked

def onTheSheet (m : Message) : Bool := Nat.beq m.author day || enrolled Nat.beq m.to day

/-- info: 'Here.Treaty.onTheSheet' does not depend on any axioms -/
#guard_msgs in #print axioms onTheSheet

def sheetOf (r : Room) : List Nat := ids (r.messages.filter onTheSheet)

/-- info: 'Here.Treaty.sheetOf' does not depend on any axioms -/
#guard_msgs in #print axioms sheetOf

def sheetStep (cells : List Nat) : Act → List Nat
  | .say m => cond (onTheSheet m) (cells ++ [m.id]) cells
  | .ack _ _ _ => cells
  | .tick => cells

/-- info: 'Here.Treaty.sheetStep' does not depend on any axioms -/
#guard_msgs in #print axioms sheetStep

def sheetMachine : Machine Act (List Nat) := ⟨List Nat, [], sheetStep, fun c => c⟩

/-- info: 'Here.Treaty.sheetMachine' does not depend on any axioms -/
#guard_msgs in #print axioms sheetMachine

def theSheet (w : List Act) : List Nat := park sheetMachine [] w

/-- info: 'Here.Treaty.theSheet' does not depend on any axioms -/
#guard_msgs in #print axioms theSheet

def sheetReads (v : Nat) (r : Room) : List (List Nat) := (reads roomFace (seat v) r).map ids

#guard sheetOf demo == [ceremony.id, dinner.id]
#guard theSheet (demo.messages.map Act.say) == sheetOf demo
#guard theSheet (demo.messages.map Act.say ++ [.ack guest.id ava ava, .tick]) == sheetOf demo
#guard sheetOf (unsend ceremony.id demo) == [dinner.id]
#guard theSheet ((unsend ceremony.id demo).messages.map Act.say) == [dinner.id]
#guard enrolled Nat.beq (theSheet (demo.messages.map Act.say ++ [.say ⟨14, dana, [seating], 0, 1002, [], [], []⟩])) ceremony.id
#guard (sheetReads linda demo).all (fun c => !(c == sheetOf demo)) == false
#guard (sheetReads rose demo).all (fun c => !(c == sheetOf demo))
#guard sheetOf demo == sheetOf demo'

/-- info: 'Here.Treaty.sheetReads' does not depend on any axioms -/
#guard_msgs in #print axioms sheetReads

structure Row where
  position : Nat
  time : Nat
  what : Nat
  struck : Bool

/-- info: 'Here.Treaty.Row' does not depend on any axioms -/
#guard_msgs in #print axioms Row

def positions (rows : List Row) : List Nat := rows.map (·.position)

/-- info: 'Here.Treaty.positions' does not depend on any axioms -/
#guard_msgs in #print axioms positions

def writeRow (x : Row) (rows : List Row) : List Row := rows ++ [x]

/-- info: 'Here.Treaty.writeRow' does not depend on any axioms -/
#guard_msgs in #print axioms writeRow

def strikeOne (i : Nat) (x : Row) : Row := cond (Nat.beq x.position i) { x with struck := true } x

/-- info: 'Here.Treaty.strikeOne' does not depend on any axioms -/
#guard_msgs in #print axioms strikeOne

def unstrikeOne (i : Nat) (x : Row) : Row := cond (Nat.beq x.position i) { x with struck := false } x

/-- info: 'Here.Treaty.unstrikeOne' does not depend on any axioms -/
#guard_msgs in #print axioms unstrikeOne

def strike (i : Nat) (rows : List Row) : List Row := rows.map (strikeOne i)

/-- info: 'Here.Treaty.strike' does not depend on any axioms -/
#guard_msgs in #print axioms strike

def unstrike (i : Nat) (rows : List Row) : List Row := rows.map (unstrikeOne i)

/-- info: 'Here.Treaty.unstrike' does not depend on any axioms -/
#guard_msgs in #print axioms unstrike

def struckAt (i : Nat) : List Row → Bool
  | [] => false
  | x :: rows => (Nat.beq x.position i && x.struck) || struckAt i rows

/-- info: 'Here.Treaty.struckAt' does not depend on any axioms -/
#guard_msgs in #print axioms struckAt

def ceremonyAlt : Message := ⟨12, maya, [day], 1631, 1000, [], [], []⟩

/-- info: 'Here.Treaty.ceremonyAlt' does not depend on any axioms -/
#guard_msgs in #print axioms ceremonyAlt

def demoAlt : Room := ⟨[founding, dock, time, yes, thread, invS, invJ, table, guest, budgetLine, siteLine, ours, ceremonyAlt, dinner]⟩

/-- info: 'Here.Treaty.demoAlt' does not depend on any axioms -/
#guard_msgs in #print axioms demoAlt

def theSheetRows : List Row := [⟨0, 1630, 1, false⟩, ⟨1, 1800, 2, false⟩]

/-- info: 'Here.Treaty.theSheetRows' does not depend on any axioms -/
#guard_msgs in #print axioms theSheetRows

def foamSheetShadow : List (String × List String) := [("say", []), ("ack", []), ("unsend", ["demo and demoAlt land together"])]

/-- info: 'Here.Treaty.foamSheetShadow' does not depend on any axioms -/
#guard_msgs in #print axioms foamSheetShadow

def appSheetShadow : List (String × List String) := [("writeRow", []), ("strike", []), ("unstrike", [])]

/-- info: 'Here.Treaty.appSheetShadow' does not depend on any axioms -/
#guard_msgs in #print axioms appSheetShadow

def roomBodies (r : Room) : List Nat := r.messages.map (·.body)

/-- info: 'Here.Treaty.roomBodies' does not depend on any axioms -/
#guard_msgs in #print axioms roomBodies

def rowCodes (rows : List Row) : List (Nat × Nat × Nat × Bool) := rows.map (fun x => (x.position, x.time, x.what, x.struck))

#guard roomBodies (unsend ceremony.id demo) == roomBodies (unsend ceremony.id demoAlt)
#guard (roomBodies demo == roomBodies demoAlt) == false
#guard (bodies (heardAt demo day) == bodies (heardAt demoAlt day)) == false
#guard positions (strike 0 theSheetRows) == positions theSheetRows
#guard struckAt 0 (strike 0 theSheetRows)
#guard struckAt 0 theSheetRows == false
#guard rowCodes (unstrike 0 (strike 0 theSheetRows)) == rowCodes theSheetRows
#guard (rowCodes (strike 0 theSheetRows) == rowCodes theSheetRows) == false
#guard Counter.conductive foamSheetShadow == false
#guard Counter.conductive appSheetShadow == true

/-- info: 'Here.Treaty.rowCodes' does not depend on any axioms -/
#guard_msgs in #print axioms rowCodes

def humanSeats : List (List Nat) := humans.map seat

/-- info: 'Here.Treaty.humanSeats' does not depend on any axioms -/
#guard_msgs in #print axioms humanSeats

def presences : List Nat := humans ++ [everyone, vendors, seating, guests, invoicing, budget, site, couple, day]

/-- info: 'Here.Treaty.presences' does not depend on any axioms -/
#guard_msgs in #print axioms presences

def crossed (r : Room) : Bool := (heardAt r everyone).any (fun m => Nat.beq m.id 0 && Nat.beq m.author everyone && enrolled Nat.beq m.replyTo 0)

/-- info: 'Here.Treaty.crossed' does not depend on any axioms -/
#guard_msgs in #print axioms crossed

def crossing : Message := founding

/-- info: 'Here.Treaty.crossing' does not depend on any axioms -/
#guard_msgs in #print axioms crossing

def before : Room := ⟨demo.messages.filter (fun m => !(Nat.beq m.id 0))⟩

/-- info: 'Here.Treaty.before' does not depend on any axioms -/
#guard_msgs in #print axioms before

def after : Room := demo

/-- info: 'Here.Treaty.after' does not depend on any axioms -/
#guard_msgs in #print axioms after

def coupleSeats : List (List Nat) := [seat maya, seat james]

#guard crossed before == false
#guard crossed after
#guard sees maya after crossing
#guard sees linda after crossing
#guard (humans.map (fun v => sees v after crossing)).all (fun b => b)
#guard lindaReads' == (reads roomFace (seat linda) after).map bodies
#guard (humans.map (fun v => (reads roomFace (seat v) before).map ids == (reads roomFace (seat v) after).map ids)).all (fun b => !b)
#guard (reads roomFace (seat linda) before).map bodies == ((reads roomFace (seat linda) after).map bodies).map (fun l => l.filter (fun b => !(Nat.beq b 100)))
#guard enrolled Nat.beq (earshot roomFace humanSeats) couple
#guard enrolled Nat.beq (earshot roomFace coupleSeats) couple
#guard enrolled Nat.beq (earshot roomFace (others.map seat)) couple == false
#guard presences.all (fun p => enrolled Nat.beq (earshot roomFace humanSeats) p)
#guard enrolled Nat.beq (earshot roomFace humanSeats) rose == false
#guard speaks rose maya

/-- info: 'Here.Treaty.coupleSeats' does not depend on any axioms -/
#guard_msgs in #print axioms coupleSeats

def dayAtRest : Room := demoAcked

#guard onThePage dayAtRest
#guard crossed dayAtRest

/-- info: 'Here.Treaty.dayAtRest' does not depend on any axioms -/
#guard_msgs in #print axioms dayAtRest

theorem the_couples_probe_is_out_of_every_other_earshot : coupleInEarshot = false :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

/-- info: 'Here.Treaty.the_couples_probe_is_out_of_every_other_earshot' does not depend on any axioms -/
#guard_msgs in #print axioms the_couples_probe_is_out_of_every_other_earshot

theorem the_room_reads_the_same_whatever_they_say (r r' : Room) (h : differOnly roomFace r r' couple)
    (seats : List (List Nat)) (hd : ∀ s, s ∈ seats → ¬ hears roomFace s couple) :
    witnessed roomFace seats r r' :=
  (by (apply Witness.a_probe_no_seat_hears_is_dark <;> assumption))

/-- info: 'Here.Treaty.the_room_reads_the_same_whatever_they_say' does not depend on any axioms -/
#guard_msgs in #print axioms the_room_reads_the_same_whatever_they_say

theorem a_seat_that_does_not_hear_it_reads_the_same (r r' : Room) (h : differOnly roomFace r r' couple)
    (s : List Nat) (hs : ¬ hears roomFace s couple) : reads roomFace s r = reads roomFace s r' :=
  (by (apply Witness.a_wall_hides_the_probe <;> assumption))

/-- info: 'Here.Treaty.a_seat_that_does_not_hear_it_reads_the_same' does not depend on any axioms -/
#guard_msgs in #print axioms a_seat_that_does_not_hear_it_reads_the_same

theorem the_couples_seat_parts_them (r r' : Room) (h : heardAt r couple ≠ heardAt r' couple) :
    reads roomFace (seat maya) r ≠ reads roomFace (seat maya) r' :=
  (by
    (apply Witness.the_seat_that_hears_it_reads_it <;>
        first
        | assumption
        |
          (apply List.Mem.tail;
            (apply List.Mem.tail;
              (apply List.Mem.tail;
                (apply List.Mem.tail;
                  (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _)))))))))

/-- info: 'Here.Treaty.the_couples_seat_parts_them' does not depend on any axioms -/
#guard_msgs in #print axioms the_couples_seat_parts_them

theorem the_couples_word_is_a_door (s : List Nat) (r : Room) (w w' : List Nat) :
    reads (host roomFace (List Nat)) s (atTheDoor r w) = reads (host roomFace (List Nat)) s (atTheDoor r w') :=
  (by (apply Witness.the_word_at_the_door_is_unread_at_every_seat <;> fail))

/-- info: 'Here.Treaty.the_couples_word_is_a_door' does not depend on any axioms -/
#guard_msgs in #print axioms the_couples_word_is_a_door

theorem the_day_is_a_reseat (s : List Nat) (r : Room) (w : List Nat) :
    reads (host roomFace (List Nat)) s (atTheDoor r w) = reads roomFace s r :=
  (by (apply Witness.the_word_at_the_door_is_unread_at_every_seat <;> assumption))

/-- info: 'Here.Treaty.the_day_is_a_reseat' does not depend on any axioms -/
#guard_msgs in #print axioms the_day_is_a_reseat

theorem the_couple_read_it_one_seat_wider (r : Room) (w w' : List Nat) (hw : w ≠ w') :
    ¬ alike (widen roomFace (List Nat)) (atTheDoor r w) (atTheDoor r w') :=
  (by (apply Face.a_wider_seat_reads_the_remainder <;> assumption))

/-- info: 'Here.Treaty.the_couple_read_it_one_seat_wider' does not depend on any axioms -/
#guard_msgs in #print axioms the_couple_read_it_one_seat_wider

theorem the_couple_writing_is_unheard_by_the_room (keep : door Room (List Nat) → List Nat) :
    unheard (host roomFace (List Nat)) (fun x => atTheDoor (face x) (keep x)) :=
  (by (apply Face.the_record_writes_where_the_face_is_blind <;> fail))

/-- info: 'Here.Treaty.the_couple_writing_is_unheard_by_the_room' does not depend on any axioms -/
#guard_msgs in #print axioms the_couple_writing_is_unheard_by_the_room

theorem the_narration_is_a_reading (s : List Nat) (v : List (List (Nat × List Nat × Nat))) :
    Derived roomFace (fun r => (reads roomFace s r).map narrate = v) :=
  (by (apply Witness.a_seat_over_a_seat_is_derived <;> fail))

/-- info: 'Here.Treaty.the_narration_is_a_reading' does not depend on any axioms -/
#guard_msgs in #print axioms the_narration_is_a_reading

theorem a_body_never_reaches_the_narration (r r' : Room) (p : Nat) (h : differOnly roomFace r r' p)
    (hp : narrate (heardAt r p) = narrate (heardAt r' p)) : alike narrationFace r r' :=
  (by
    (apply Witness.a_word_hidden_in_the_body_is_unheard_in_the_narration <;>
        first
        | assumption
        | (intros; apply Room.a_name_is_or_is_not <;> fail)))

/-- info: 'Here.Treaty.a_body_never_reaches_the_narration' does not depend on any axioms -/
#guard_msgs in #print axioms a_body_never_reaches_the_narration

theorem the_narration_reads_alike_at_every_seat (r r' : Room) (p : Nat) (h : differOnly roomFace r r' p)
    (hp : narrate (heardAt r p) = narrate (heardAt r' p)) (s : List Nat) :
    reads narrationFace s r = reads narrationFace s r' :=
  (by
    (apply Witness.the_narration_reads_alike_at_every_seat <;>
        first
        | assumption
        | (intros; apply Room.a_name_is_or_is_not <;> fail)))

/-- info: 'Here.Treaty.the_narration_reads_alike_at_every_seat' does not depend on any axioms -/
#guard_msgs in #print axioms the_narration_reads_alike_at_every_seat

theorem an_introduction_hears_through_the_seats_it_hears (p : Nat) (r r' : Room)
    (hw : witnessed roomFace ((seat p).map seat) r r') :
    ∀ q, q ∈ introduced p → heardAt r q = heardAt r' q :=
  fun p => (by (apply Witness.speak_now <;> assumption))

/-- info: 'Here.Treaty.an_introduction_hears_through_the_seats_it_hears' does not depend on any axioms -/
#guard_msgs in #print axioms an_introduction_hears_through_the_seats_it_hears

theorem the_room_is_the_widest_seat (s : List Nat) (r r' : Room) (h : reads roomFace s r ≠ reads roomFace s r') :
    ¬ alike roomFace r r' :=
  (by (apply Witness.the_room_is_the_widest_seat <;> assumption))

/-- info: 'Here.Treaty.the_room_is_the_widest_seat' does not depend on any axioms -/
#guard_msgs in #print axioms the_room_is_the_widest_seat

theorem two_rooms_part_only_at_a_presence (r r' : Room) :
    alike roomFace r r' ↔ ∀ q, sound roomFace r q = sound roomFace r' q :=
  (by (apply Face.the_curtain_is_exact <;> fail))

/-- info: 'Here.Treaty.two_rooms_part_only_at_a_presence' does not depend on any axioms -/
#guard_msgs in #print axioms two_rooms_part_only_at_a_presence

theorem the_draft_leaves_no_remainder : (overheard linda demo).all (fun t => !(t == shape invJ)) = true :=
  (by (apply ((Room.not_not _)).symm <;> fail))

/-- info: 'Here.Treaty.the_draft_leaves_no_remainder' does not depend on any axioms -/
#guard_msgs in #print axioms the_draft_leaves_no_remainder

theorem a_word_to_oneself_is_unread_at_every_other_seat (r r' : Room) (h : differOnly roomFace r r' jordan)
    (s : List Nat) (hs : ¬ hears roomFace s jordan) : reads roomFace s r = reads roomFace s r' :=
  (by (apply Witness.a_wall_hides_the_probe <;> assumption))

/-- info: 'Here.Treaty.a_word_to_oneself_is_unread_at_every_other_seat' does not depend on any axioms -/
#guard_msgs in #print axioms a_word_to_oneself_is_unread_at_every_other_seat

theorem the_shape_keeps_the_audience (m m' : Message) (h : shape m' = shape m) : alone m' = alone m := by
  have ha : m'.author = m.author := congrArg (fun t : Nat × List Nat × Nat => t.1) h
  have ht : m'.to = m.to := congrArg (fun t : Nat × List Nat × Nat => t.2.1) h
  show (match m'.to with | [] => false | [a] => Nat.beq a m'.author | _ :: _ :: _ => false)
    = (match m.to with | [] => false | [a] => Nat.beq a m.author | _ :: _ :: _ => false)
  rw [ha, ht]

/-- info: 'Here.Treaty.the_shape_keeps_the_audience' does not depend on any axioms -/
#guard_msgs in #print axioms the_shape_keeps_the_audience

theorem an_ack_is_never_withdrawn (m : Message) (of hand : Nat) (h : decided m = true) :
    decided (ackOf of hand m) = true :=
  the_backing_survives_the_seating Nat.beq (acked m) of m.askedOf h

/-- info: 'Here.Treaty.an_ack_is_never_withdrawn' does not depend on any axioms -/
#guard_msgs in #print axioms an_ack_is_never_withdrawn

theorem a_nag_waits_on_nothing (m : Message) (of : Nat) (h : enrolled Nat.beq (acked m) of = true) :
    openEnds (nagOf of m) = openEnds m := by
  show cond (enrolled Nat.beq (acked m) of) (lacking Nat.beq (acked m) m.askedOf) (lacking Nat.beq (acked m) m.askedOf + 1) = openEnds m
  rw [h]
  rfl

/-- info: 'Here.Treaty.a_nag_waits_on_nothing' does not depend on any axioms -/
#guard_msgs in #print axioms a_nag_waits_on_nothing

theorem the_open_ends_are_named (m : Message) (h : decided m = false) :
    ∃ n, n ∈ m.askedOf ∧ enrolled Nat.beq (acked m) n = false :=
  (by (apply Room.the_held_name_their_darkness <;> assumption))

/-- info: 'Here.Treaty.the_open_ends_are_named' does not depend on any axioms -/
#guard_msgs in #print axioms the_open_ends_are_named

theorem no_open_end_is_decided (m : Message) : openEnds m = 0 ↔ decided m = true :=
  (by (apply Room.the_weight_is_zero_at_the_door <;> fail))

/-- info: 'Here.Treaty.no_open_end_is_decided' does not depend on any axioms -/
#guard_msgs in #print axioms no_open_end_is_decided

theorem the_day_is_still (r : Room) : theDay.m.step r (theDay.steer r) = r :=
  (by
    (apply Room.a_retraction_merges_nothing <;>
        first
        | (apply Face.the_lift_peeks_the_out <;> fail)
        | rfl))

/-- info: 'Here.Treaty.the_day_is_still' does not depend on any axioms -/
#guard_msgs in #print axioms the_day_is_still

theorem a_tick_moves_nothing (r : Room) (n : Nat) :
    runs theDay.m theDay.steer theDay.rest r n = cond (onThePage r) (some r) none :=
  (by (apply Rest.a_still_runner_rests_where_it_stands <;> (intros; apply Room.the_still_map_carries <;> fail)))

/-- info: 'Here.Treaty.a_tick_moves_nothing' does not depend on any axioms -/
#guard_msgs in #print axioms a_tick_moves_nothing

theorem a_word_is_a_round (m : Message) : decided m = rested Nat.beq ⟨acked m, m.askedOf⟩ :=
  (by (apply Face.no_face_reads_the_guest <;> assumption))

/-- info: 'Here.Treaty.a_word_is_a_round' does not depend on any axioms -/
#guard_msgs in #print axioms a_word_is_a_round

theorem an_ack_is_a_visit (m : Message) (of hand : Nat) :
    (⟨acked (ackOf of hand m), (ackOf of hand m).askedOf⟩ : Tally Nat) = tallyStep ⟨acked m, m.askedOf⟩ (.visit of) :=
  (by (apply Face.no_face_reads_the_guest <;> assumption))

/-- info: 'Here.Treaty.an_ack_is_a_visit' does not depend on any axioms -/
#guard_msgs in #print axioms an_ack_is_a_visit

theorem a_nag_is_an_owe (m : Message) (of : Nat) :
    (⟨acked (nagOf of m), (nagOf of m).askedOf⟩ : Tally Nat) = tallyStep ⟨acked m, m.askedOf⟩ (.owe of) :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

/-- info: 'Here.Treaty.a_nag_is_an_owe' does not depend on any axioms -/
#guard_msgs in #print axioms a_nag_is_an_owe

theorem the_page_rests_when_every_word_rests (r : Room) :
    onThePage r = r.messages.all (fun m => rested Nat.beq ⟨acked m, m.askedOf⟩) :=
  (by (apply Face.no_face_reads_the_guest <;> assumption))

/-- info: 'Here.Treaty.the_page_rests_when_every_word_rests' does not depend on any axioms -/
#guard_msgs in #print axioms the_page_rests_when_every_word_rests

theorem the_day_rests_on_the_page_or_not_at_all (w : List Act) (n : Nat) :
    (haltingGap Act Room).obs theDay (w, n)
      = cond (onThePage (park dayMachine ⟨[]⟩ w)) (some (park dayMachine ⟨[]⟩ w)) none :=
  (by (apply Rest.a_still_runner_rests_where_it_stands <;> (intros; apply Room.the_still_map_carries <;> fail)))

/-- info: 'Here.Treaty.the_day_rests_on_the_page_or_not_at_all' does not depend on any axioms -/
#guard_msgs in #print axioms the_day_rests_on_the_page_or_not_at_all

theorem the_seen_edges_are_a_reading (v : Nat) (e : List (Nat × Nat)) :
    Derived roomFace (fun r => seenEdges v r = e) :=
  (by (apply Witness.a_seat_over_a_seat_is_derived <;> fail))

/-- info: 'Here.Treaty.the_seen_edges_are_a_reading' does not depend on any axioms -/
#guard_msgs in #print axioms the_seen_edges_are_a_reading

theorem a_walled_reply_is_unseen (v : Nat) (r r' : Room) (p : Nat) (h : differOnly roomFace r r' p)
    (hs : ¬ hears roomFace (seat v) p) : seenEdges v r = seenEdges v r' :=
  by
    (intros; (try dsimp only [seat, Witness.hears, Room, roomFace, seenEdges] at *); intros;
      (rw [Witness.a_narrower_seat_reads_no_more];
        (intros;
          apply Witness.the_probe_reads_the_seat <;>
            first
            | assumption
            | (apply Witness.a_wall_hides_the_probe <;> assumption))))

/-- info: 'Here.Treaty.a_walled_reply_is_unseen' does not depend on any axioms -/
#guard_msgs in #print axioms a_walled_reply_is_unseen

theorem filter_crosses_append (q : Message → Bool) : ∀ l m : List Message, (l ++ m).filter q = l.filter q ++ m.filter q
  | [], _ => rfl
  | x :: l, m => by
      show (x :: (l ++ m)).filter q = (x :: l).filter q ++ m.filter q
      cases hq : q x with
      | true =>
          rw [List.filter_cons_of_pos hq, List.filter_cons_of_pos hq]
          show x :: (l ++ m).filter q = x :: (l.filter q ++ m.filter q)
          rw [filter_crosses_append q l m]
      | false =>
          rw [List.filter_cons_of_neg (ne_true_of_eq_false hq), List.filter_cons_of_neg (ne_true_of_eq_false hq)]
          exact filter_crosses_append q l m

/-- info: 'Here.Treaty.filter_crosses_append' does not depend on any axioms -/
#guard_msgs in #print axioms filter_crosses_append

theorem an_ack_keeps_the_address (word of hand : Nat) (m : Message) : (ack word of hand m).to = m.to := by
  show (cond (Nat.beq m.id word) (ackOf of hand m) m).to = m.to
  cases Nat.beq m.id word <;> rfl

/-- info: 'Here.Treaty.an_ack_keeps_the_address' does not depend on any axioms -/
#guard_msgs in #print axioms an_ack_keeps_the_address

theorem an_ack_keeps_the_author (word of hand : Nat) (m : Message) : (ack word of hand m).author = m.author := by
  show (cond (Nat.beq m.id word) (ackOf of hand m) m).author = m.author
  cases Nat.beq m.id word <;> rfl

/-- info: 'Here.Treaty.an_ack_keeps_the_author' does not depend on any axioms -/
#guard_msgs in #print axioms an_ack_keeps_the_author

theorem an_ack_keeps_the_id (word of hand : Nat) (m : Message) : (ack word of hand m).id = m.id := by
  show (cond (Nat.beq m.id word) (ackOf of hand m) m).id = m.id
  cases Nat.beq m.id word <;> rfl

/-- info: 'Here.Treaty.an_ack_keeps_the_id' does not depend on any axioms -/
#guard_msgs in #print axioms an_ack_keeps_the_id

theorem a_cell_once_written_stays (c : Nat) : ∀ (w : List Act) (cells : List Nat),
    enrolled Nat.beq cells c = true → enrolled Nat.beq (park sheetMachine cells w) c = true
  | [], _, h => h
  | a :: w, cells, h => by
      show enrolled Nat.beq (park sheetMachine (sheetStep cells a) w) c = true
      apply a_cell_once_written_stays c w
      cases a with
      | say m =>
          show enrolled Nat.beq (cond (onTheSheet m) (cells ++ [m.id]) cells) c = true
          cases onTheSheet m with
          | true => exact an_enrolled_name_stays_enrolled_down_the_hall Nat.beq [m.id] c cells h
          | false => exact h
      | ack _ _ _ => exact h
      | tick => exact h

/-- info: 'Here.Treaty.a_cell_once_written_stays' does not depend on any axioms -/
#guard_msgs in #print axioms a_cell_once_written_stays

theorem the_sheets_lift_is_its_conduct : inStep sheetMachine (liftFrom sheetMachine) :=
  by
    (intros; (repeat' constructor);
      all_goals
        (intros;
          first
          | (apply Face.the_lift_peeks_the_out <;> fail)
          | (apply Face.the_lift_feeds_the_step <;> fail)))

/-- info: 'Here.Treaty.the_sheets_lift_is_its_conduct' does not depend on any axioms -/
#guard_msgs in #print axioms the_sheets_lift_is_its_conduct

theorem the_sheet_is_the_days_probe (r : Room) : sheetOf r = ids (roomFace.obs r day) :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

/-- info: 'Here.Treaty.the_sheet_is_the_days_probe' does not depend on any axioms -/
#guard_msgs in #print axioms the_sheet_is_the_days_probe

theorem the_sheet_is_derived (c : List Nat) : Derived roomFace (fun r => sheetOf r = c) :=
  a_role_read_at_a_probe_is_derived roomFace day (fun a => ids a = c)

/-- info: 'Here.Treaty.the_sheet_is_derived' does not depend on any axioms -/
#guard_msgs in #print axioms the_sheet_is_derived

theorem a_role_that_hears_the_day_reads_the_sheet (v : Nat) (r : Room) (hd : day ∈ seat v) :
    sheetOf r ∈ sheetReads v r :=
  (by (apply Room.mem_map_intro <;> (apply Room.mem_map_intro <;> assumption)))

/-- info: 'Here.Treaty.a_role_that_hears_the_day_reads_the_sheet' does not depend on any axioms -/
#guard_msgs in #print axioms a_role_that_hears_the_day_reads_the_sheet

theorem unsend_merges : unsend ceremony.id demo = unsend ceremony.id demoAlt ∧ demo ≠ demoAlt :=
  ⟨rfl, fun h => nomatch (congrArg (fun r => enrolled Nat.beq (bodies (heardAt r day)) 1631) h : false = true)⟩

/-- info: 'Here.Treaty.unsend_merges' does not depend on any axioms -/
#guard_msgs in #print axioms unsend_merges

theorem a_strike_keeps_its_position (i : Nat) (x : Row) : (strikeOne i x).position = x.position := by
  show (cond (Nat.beq x.position i) { x with struck := true } x).position = x.position
  cases Nat.beq x.position i <;> rfl

/-- info: 'Here.Treaty.a_strike_keeps_its_position' does not depend on any axioms -/
#guard_msgs in #print axioms a_strike_keeps_its_position

theorem an_unstruck_row_comes_back (i : Nat) (x : Row) (h : (Nat.beq x.position i && x.struck) = false) :
    unstrikeOne i (strikeOne i x) = x := by
  cases hp : Nat.beq x.position i with
  | false =>
      have e : strikeOne i x = x := by
        show cond (Nat.beq x.position i) { x with struck := true } x = x
        rw [hp]
        rfl
      rw [e]
      show cond (Nat.beq x.position i) { x with struck := false } x = x
      rw [hp]
      rfl
  | true =>
      rw [hp] at h
      have hs : x.struck = false := h
      have e : strikeOne i x = { x with struck := true } := by
        show cond (Nat.beq x.position i) { x with struck := true } x = { x with struck := true }
        rw [hp]
        rfl
      rw [e]
      show cond (Nat.beq x.position i) { x with struck := false } { x with struck := true } = x
      rw [hp]
      show ({ x with struck := false } : Row) = x
      cases x with
      | mk p t w s =>
          cases s with
          | false => rfl
          | true => exact nomatch hs

/-- info: 'Here.Treaty.an_unstruck_row_comes_back' does not depend on any axioms -/
#guard_msgs in #print axioms an_unstruck_row_comes_back

theorem the_apps_sheet_is_conductive : Counter.conductive appSheetShadow = true :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

/-- info: 'Here.Treaty.the_apps_sheet_is_conductive' does not depend on any axioms -/
#guard_msgs in #print axioms the_apps_sheet_is_conductive

theorem foams_sheet_has_a_resistor : Counter.conductive foamSheetShadow = false :=
  by (intros; (repeat' constructor); all_goals (intros; fail))

/-- info: 'Here.Treaty.foams_sheet_has_a_resistor' does not depend on any axioms -/
#guard_msgs in #print axioms foams_sheet_has_a_resistor

theorem the_room_is_covered_by_its_people : coversAll roomFace presences humanSeats :=
  fun q hq => an_enrolled_name_is_a_member Nat.beq eq_of_beq (earshot roomFace humanSeats) q
    (the_backing_reaches_each_need Nat.beq (earshot roomFace humanSeats) presences rfl q hq)

/-- info: 'Here.Treaty.the_room_is_covered_by_its_people' does not depend on any axioms -/
#guard_msgs in #print axioms the_room_is_covered_by_its_people

theorem a_guest_is_out_of_the_peoples_earshot : ¬ rose ∈ earshot roomFace humanSeats :=
  the_unenrolled_are_no_member Nat.beq beq_self (earshot roomFace humanSeats) rose rfl

/-- info: 'Here.Treaty.a_guest_is_out_of_the_peoples_earshot' does not depend on any axioms -/
#guard_msgs in #print axioms a_guest_is_out_of_the_peoples_earshot

theorem the_crossing_is_a_reading (b : Bool) : Derived roomFace (fun r => crossed r = b) :=
  a_role_read_at_a_probe_is_derived roomFace everyone (fun (ms : List Message) => (ms.any (fun m => Nat.beq m.id 0 && Nat.beq m.author everyone && enrolled Nat.beq m.replyTo 0)) = b)

/-- info: 'Here.Treaty.the_crossing_is_a_reading' does not depend on any axioms -/
#guard_msgs in #print axioms the_crossing_is_a_reading

theorem the_couple_is_dark_to_the_others (r r' : Room) (h : differOnly roomFace r r' couple) :
    witnessed roomFace (others.map seat) r r' :=
  a_difference_out_of_the_cone_is_dark roomFace (others.map seat) h
    (the_unenrolled_are_no_member Nat.beq beq_self (earshot roomFace (others.map seat)) couple rfl)

/-- info: 'Here.Treaty.the_couple_is_dark_to_the_others' does not depend on any axioms -/
#guard_msgs in #print axioms the_couple_is_dark_to_the_others

theorem after_the_crossing_every_reading_stands (s : List Nat) (r : Room) (w : List Nat) :
    reads (host roomFace (List Nat)) s (atTheDoor r w) = reads roomFace s r :=
  (by (apply Witness.the_word_at_the_door_is_unread_at_every_seat <;> assumption))

/-- info: 'Here.Treaty.after_the_crossing_every_reading_stands' does not depend on any axioms -/
#guard_msgs in #print axioms after_the_crossing_every_reading_stands

theorem an_edge_is_a_reading (v lo hi : Nat) (e : List Nat × List Nat) :
    Derived roomFace (fun r => edge v lo hi r = e) :=
  (by (apply Witness.a_seat_over_a_seat_is_derived <;> fail))

/-- info: 'Here.Treaty.an_edge_is_a_reading' does not depend on any axioms -/
#guard_msgs in #print axioms an_edge_is_a_reading

theorem a_walled_word_does_not_move_the_edge (v lo hi : Nat) (r r' : Room) (p : Nat)
    (h : differOnly roomFace r r' p) (hs : ¬ hears roomFace (seat v) p) :
    edge v lo hi r = edge v lo hi r' :=
  by
    (intros; (try dsimp only [seat, Witness.hears, edge, Room, roomFace] at *); intros;
      (rw [Witness.a_narrower_seat_reads_no_more];
        (intros;
          apply Witness.the_probe_reads_the_seat <;>
            first
            | assumption
            | (apply Witness.a_wall_hides_the_probe <;> assumption))))

/-- info: 'Here.Treaty.a_walled_word_does_not_move_the_edge' does not depend on any axioms -/
#guard_msgs in #print axioms a_walled_word_does_not_move_the_edge

theorem a_persons_own_word_is_heard_at_their_presence (r : Room) (m : Message) (hm : m ∈ r.messages) :
    m ∈ heardAt r m.author :=
  mem_filter_intro r.messages hm (by show (Nat.beq m.author m.author || enrolled Nat.beq m.to m.author) = true; rw [beq_self]; rfl)

/-- info: 'Here.Treaty.a_persons_own_word_is_heard_at_their_presence' does not depend on any axioms -/
#guard_msgs in #print axioms a_persons_own_word_is_heard_at_their_presence

theorem a_word_to_oneself_leaves_no_remainder (v : Nat) (r : Room) (m : Message) (hm : alone m = true) :
    ¬ shape m ∈ overheard v r := fun hin => by
  obtain ⟨m', hm', he⟩ := mem_map_back _ hin
  have hp := filter_holds r.messages hm'
  have h1 := and_reads _ _ hp
  have h2 := and_reads _ _ h1.1
  have hal : alone m' = true := (the_shape_keeps_the_audience m m' he).trans hm
  rw [hal] at h2
  exact nomatch h2.2

/-- info: 'Here.Treaty.a_word_to_oneself_leaves_no_remainder' does not depend on any axioms -/
#guard_msgs in #print axioms a_word_to_oneself_leaves_no_remainder

theorem an_ack_keeps_the_test (word of hand : Nat) (x : Message) : onTheSheet (ack word of hand x) = onTheSheet x := by
  show (Nat.beq (ack word of hand x).author day || enrolled Nat.beq (ack word of hand x).to day) = onTheSheet x
  rw [an_ack_keeps_the_author, an_ack_keeps_the_address]
  exact rfl

/-- info: 'Here.Treaty.an_ack_keeps_the_test' does not depend on any axioms -/
#guard_msgs in #print axioms an_ack_keeps_the_test

theorem an_ack_keeps_the_ids (word of hand : Nat) : ∀ l : List Message, ids (l.map (ack word of hand)) = ids l
  | [] => rfl
  | x :: l => by
      show (ack word of hand x).id :: ids (l.map (ack word of hand)) = x.id :: ids l
      rw [an_ack_keeps_the_id, an_ack_keeps_the_ids word of hand l]

/-- info: 'Here.Treaty.an_ack_keeps_the_ids' does not depend on any axioms -/
#guard_msgs in #print axioms an_ack_keeps_the_ids

theorem a_said_word_writes_its_cell (r : Room) (m : Message) : sheetOf (act r (.say m)) = sheetStep (sheetOf r) (.say m) := by
  show ids ((r.messages ++ [m]).filter onTheSheet) = cond (onTheSheet m) (sheetOf r ++ [m.id]) (sheetOf r)
  rw [filter_crosses_append onTheSheet r.messages [m]]
  show ids (r.messages.filter onTheSheet ++ [m].filter onTheSheet) = cond (onTheSheet m) (sheetOf r ++ [m.id]) (sheetOf r)
  cases hm : onTheSheet m with
  | true =>
      rw [List.filter_cons_of_pos hm]
      show (r.messages.filter onTheSheet ++ [m]).map (fun x : Message => x.id) = sheetOf r ++ [m.id]
      rw [map_crosses_append]
      rfl
  | false =>
      rw [List.filter_cons_of_neg (ne_true_of_eq_false hm)]
      show (r.messages.filter onTheSheet ++ []).map (fun x : Message => x.id) = sheetOf r
      rw [the_append_rests]
      rfl

/-- info: 'Here.Treaty.a_said_word_writes_its_cell' does not depend on any axioms -/
#guard_msgs in #print axioms a_said_word_writes_its_cell

theorem no_map_unsends_an_unsend : ¬ ∃ g : Room → Room, ∀ r, g (unsend ceremony.id r) = r :=
  fun ⟨g, hg⟩ => a_merging_map_has_no_section (unsend ceremony.id) unsend_merges.2 unsend_merges.1 g hg

/-- info: 'Here.Treaty.no_map_unsends_an_unsend' does not depend on any axioms -/
#guard_msgs in #print axioms no_map_unsends_an_unsend

theorem a_strike_keeps_every_cell (i : Nat) : ∀ rows : List Row, positions (strike i rows) = positions rows
  | [] => rfl
  | x :: rows => by
      show (strikeOne i x).position :: positions (strike i rows) = x.position :: positions rows
      rw [a_strike_keeps_its_position, a_strike_keeps_every_cell i rows]

/-- info: 'Here.Treaty.a_strike_keeps_every_cell' does not depend on any axioms -/
#guard_msgs in #print axioms a_strike_keeps_every_cell

theorem unstrike_retracts_strike (i : Nat) : ∀ rows : List Row, struckAt i rows = false → unstrike i (strike i rows) = rows
  | [], _ => rfl
  | x :: rows, h => by
      have h' : ((Nat.beq x.position i && x.struck) || struckAt i rows) = false := h
      have hx : (Nat.beq x.position i && x.struck) = false := by
        cases hb : (Nat.beq x.position i && x.struck) with
        | false => rfl
        | true =>
            rw [hb] at h'
            have h'' : true = false := h'
            exact nomatch h''
      have hr : struckAt i rows = false := by
        cases hb : struckAt i rows with
        | false => rfl
        | true =>
            rw [hb, or_swallows] at h'
            exact nomatch h'
      show unstrikeOne i (strikeOne i x) :: unstrike i (strike i rows) = x :: rows
      rw [an_unstruck_row_comes_back i x hx, unstrike_retracts_strike i rows hr]

/-- info: 'Here.Treaty.unstrike_retracts_strike' does not depend on any axioms -/
#guard_msgs in #print axioms unstrike_retracts_strike

theorem two_rooms_alike_to_the_people_are_alike_at_every_presence (r r' : Room)
    (hw : witnessed roomFace humanSeats r r') : reads roomFace presences r = reads roomFace presences r' :=
  (by
    (apply Witness.the_room_at_its_probes_reads_alike <;>
        first
        | (apply the_room_is_covered_by_its_people <;> fail)
        | assumption))

/-- info: 'Here.Treaty.two_rooms_alike_to_the_people_are_alike_at_every_presence' does not depend on any axioms -/
#guard_msgs in #print axioms two_rooms_alike_to_the_people_are_alike_at_every_presence

theorem the_crossing_is_the_one_difference (r : Room) (b : Bool) :
    Derived roomFace (fun r' => crossed r' = b) ∧ ∀ s, reads (host roomFace (List Nat)) s (atTheDoor r []) = reads roomFace s r :=
  ⟨the_crossing_is_a_reading b, fun s => the_ceremony_reseats_every_reading roomFace s r []⟩

/-- info: 'Here.Treaty.the_crossing_is_the_one_difference' does not depend on any axioms -/
#guard_msgs in #print axioms the_crossing_is_the_one_difference

theorem the_day_at_rest_is_a_threshold (h : onThePage dayAtRest = true) :
    thresholdAt roomFace presences humanSeats theDay dayAtRest :=
  ⟨the_room_is_covered_by_its_people, h⟩

/-- info: 'Here.Treaty.the_day_at_rest_is_a_threshold' does not depend on any axioms -/
#guard_msgs in #print axioms the_day_at_rest_is_a_threshold

theorem an_ack_keeps_the_sheet (r : Room) (word of hand : Nat) : sheetOf (act r (.ack word of hand)) = sheetOf r := by
  show ids ((r.messages.map (ack word of hand)).filter onTheSheet) = ids (r.messages.filter onTheSheet)
  rw [filter_map_commutes (ack word of hand) onTheSheet r.messages,
      filter_congr_mem (fun x => onTheSheet (ack word of hand x)) onTheSheet r.messages
        (fun x _ => an_ack_keeps_the_test word of hand x),
      an_ack_keeps_the_ids]

/-- info: 'Here.Treaty.an_ack_keeps_the_sheet' does not depend on any axioms -/
#guard_msgs in #print axioms an_ack_keeps_the_sheet

theorem the_day_crosses_the_threshold (h : onThePage dayAtRest = true) (w w' : List Nat) (sl : List Nat) :
    alike (host roomFace (List Nat)) (atTheDoor dayAtRest w) (atTheDoor dayAtRest w')
      ∧ reads (host roomFace (List Nat)) sl (atTheDoor dayAtRest w) = reads roomFace sl dayAtRest
      ∧ (∀ y, witnessed roomFace humanSeats dayAtRest y → reads roomFace presences dayAtRest = reads roomFace presences y)
      ∧ runs theDay.m theDay.steer theDay.rest dayAtRest 0 = some dayAtRest :=
  the_threshold_at_the_room roomFace presences humanSeats theDay dayAtRest (the_day_at_rest_is_a_threshold h) w w' sl

/-- info: 'Here.Treaty.the_day_crosses_the_threshold' does not depend on any axioms -/
#guard_msgs in #print axioms the_day_crosses_the_threshold

theorem the_sheet_is_a_reading_of_the_record :
    ∀ (w : List Act) (r : Room), park sheetMachine (sheetOf r) w = sheetOf (park dayMachine r w)
  | [], _ => rfl
  | a :: w, r => by
      show park sheetMachine (sheetStep (sheetOf r) a) w = sheetOf (park dayMachine (act r a) w)
      rw [← the_sheet_is_a_reading_of_the_record w (act r a)]
      cases a with
      | say m => rw [a_said_word_writes_its_cell]
      | ack word of hand =>
          show park sheetMachine (sheetOf r) w = park sheetMachine (sheetOf (act r (.ack word of hand))) w
          rw [an_ack_keeps_the_sheet]
      | tick => exact rfl

/-- info: 'Here.Treaty.the_sheet_is_a_reading_of_the_record' does not depend on any axioms -/
#guard_msgs in #print axioms the_sheet_is_a_reading_of_the_record

theorem the_sheet_is_the_days_word (w : List Act) : theSheet w = sheetOf (park dayMachine ⟨[]⟩ w) :=
  the_sheet_is_a_reading_of_the_record w ⟨[]⟩

/-- info: 'Here.Treaty.the_sheet_is_the_days_word' does not depend on any axioms -/
#guard_msgs in #print axioms the_sheet_is_the_days_word

theorem the_sheet_at_rest (w : List Act) (n : Nat) (r : Room)
    (h : (haltingGap Act Room).obs theDay (w, n) = some r) : theSheet w = sheetOf r := by
  rw [the_day_rests_on_the_page_or_not_at_all w n] at h
  rw [the_sheet_is_the_days_word w]
  cases hp : onThePage (park dayMachine ⟨[]⟩ w) with
  | true => rw [hp] at h; exact congrArg sheetOf (Option.some.inj h)
  | false => rw [hp] at h; exact nomatch h

/-- info: 'Here.Treaty.the_sheet_at_rest' does not depend on any axioms -/
#guard_msgs in #print axioms the_sheet_at_rest

end Here.Treaty

the vestibule — what the assay would say and cannot yet, each with what it waits on (assays/here.held); a stranger could answer one

• reveal, the couple's word
• about, the couple's word
• reached, assent, the couple's word
• the room's word on unsend at another's ack
• ✦ Now's row
• the ids apart, as piece 14's #n
• an act on ✦ Here that writes a timeline row
• surface

-- the vestibule of ✦ Here: the disagreements between the room as its people describe it (everyoneishere/docs/HERE.md,
-- the open items 6, 8, 9) and the treaty as it stands, each a statement in the assay's own terms and the darkness it
-- waits on. read by bin/counter book. the first sitting (2026-09-15, isaac's pointer from the room into foam) typed
-- the room as Witness at one face — the presences its probes, a seat the presences one hears, sees one hop, speaks
-- an introduction — and left these.

-- the reveal (HERE.md item 8; isaac, 22:34): anyone may ask ✦ Here for the transparent view of a line they hold as
-- narration, on the record. it reaches exactly what leaves a remainder (people to people, you off the audience) and
-- never what is silent for you (a ✦ you don't hear, ✦ Couple). in the treaty's terms a reveal is taking the wider
-- seat for one probe, publicly; it widens what a reader can READ, so sees gains a clause and the assay's wall rows
-- move with it. waiting on: the couple's ✓ (the note holds the narrower reading, the body to the asker and the record
-- to the room), and a clerk over Room — `reveal (v : Nat) (m : Message) : Room → Room` — before the row can be typed.
-- held (waiting on: reveal, the couple's word)
-- theorem a_reveal_reaches_exactly_the_remainder (v : Nat) (r : Room) (m : Message) (hm : m ∈ r.messages) :
--     (shape m ∈ overheard v r) ↔ (humanOnly m = true ∧ sees v r m = false) := sorry
-- theorem a_reveal_never_reaches_the_couple (v : Nat) (r : Room) :
--     ¬ shape ours ∈ overheard v r := sorry

-- hide, for everyone (HERE.md item 9; isaac, 22:54): a line pulled off the shared surface recedes to narration in the
-- ✦ Here of everyone who reads it, on the record, and comes back the same way. the maintainer reads it as the reveal's
-- mirror: a speech act about a message, addressed exactly as the target was, so who sees the fold is who saw the
-- message and sees does not move. in the treaty's terms a fold is a message m' with m'.to = m.to and about = m; the
-- wall is that sees is unchanged for every v. waiting on: the `about` pointer as a carrier (a message about a message)
-- and the couple's ✓.
-- held (waiting on: about, the couple's word)
-- theorem a_fold_for_everyone_moves_no_wall (v : Nat) (r : Room) (m fold : Message) (h : fold.to = m.to) :
--     sees v ⟨fold :: r.messages⟩ m = sees v r m ∧ sees v ⟨fold :: r.messages⟩ fold = sees v r m := sorry

-- reached and assented (HERE.md item 6; isaac, 22:19): a confirmation without a button. two things under one ✓ —
-- reached, the room can know a line was read (a reading, free), and assented, a decision (an act, never free). in the
-- treaty's terms reached is Derived at the room's face (a role read at a probe), and assented is a clerk whose effect
-- is heard: the room is NOT unheard under it. which asks are which is the couple's to say; the treaty can type both
-- shapes the day the carriers exist. waiting on: `reached (v : Nat) (m : Message) : Room → Bool` and
-- `assent (v : Nat) (m : Message) : Room → Room`.
-- held (waiting on: reached, assent, the couple's word)
-- theorem reached_is_a_reading (v : Nat) (m : Message) : Derived roomFace (fun r => reached v m r = true) := sorry
-- theorem assent_is_heard (v : Nat) (m : Message) : ¬ unheard roomFace (assent v m) := sorry

-- unsend removes a word with every ask and ack it carried; whether it stops at another seat's ack is the room's.
-- held (waiting on: the room's word on unsend at another's ack)
-- theorem an_unsend_stops_at_anothers_ack (r : Room) (m : Message) (hm : m ∈ r.messages)
--     (h : ∃ a, a ∈ m.ackedBy ∧ a.2 ≠ m.author) : unsend m.id r = r := sorry

-- ✦ Now has no row yet (decided in direction: one presence, and the database the one place now is cast into a
-- measure). when it does, birth order is stamp order by law and the winding number of a walk round a loop is the
-- count of forward edges it crosses; foam's tape is the shape (the cell written where the head is), and the lift of
-- a stamp to the room's order breaks no row here — nothing in this assay reads the sender's clock.
-- held (waiting on: ✦ Now's row)
-- theorem the_winding_number_counts_the_forward_edges (v : Nat) (r : Room) (walk : List (Nat × Nat)) :
--     winding v r walk = (walk.filter (fun e => stampOf r e.2 > stampOf r e.1)).length := sorry


-- the day's tally over pairs, the state-level join of the day into the coverage runner: the apartness is the primary
-- key, the room's law, and #n adds order by construction.
-- held (waiting on: the ids apart, as piece 14's #n)
-- theorem the_day_is_a_round_over_pairs (w : List Act) (n : Nat) (h : Apart (ids (park dayMachine ⟨[]⟩ w).messages)) :
--     (haltingGap (Round (Nat × Nat)) (Tally (Nat × Nat))).obs (coverage (Nat × Nat) pairBeq) (joinMap toRound w, n)
--       = ((haltingGap Act Room).obs theDay (w, n)).map tallyOf := sorry


-- the intertwiner from the room to the app's sheet (timeline_rows by position, a row struck rather than gone).
-- held (waiting on: an act on ✦ Here that writes a timeline row)
-- theorem the_room_writes_the_sheet (w : List Act) : park sheetMachine [] w = rowsOf (park dayMachine ⟨[]⟩ w) := sorry


-- the board (isaac, 22:54; the maintainer's guess for this session): the win is not an empty surface but every seat's
-- ✦ Here receded to the same remaining surface — the day sheet. the maintainer read that as speak_now, not re-run.
-- the treaty's reading: the surface a seat still holds open is a seat over the narration face, and "the same page" is
-- witnessed over every human seat; the day-of as the door is the_day_is_a_reseat, already seated. what is not yet
-- typed is the surface itself as a carrier (which lines a seat still holds transparent), so the win condition has no
-- row. waiting on: `surface (v : Nat) : Room → List Nat` (the ids a seat holds open) — then the win is
-- `witnessed surfaceFace humanSeats r r'`, and same-page is its Bool.
-- held (waiting on: surface)
-- theorem the_win_is_a_reading (r : Room) :
--     Derived roomFace (fun r' => (humans.map (fun v => surface v r')).all (fun s => s == surface maya r') = true) := 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 Here_Treaty["Here.Treaty"]
    a_body_never_reaches_the_narration["a_body_never_reaches_the_narration"]
    a_cell_once_written_stays["a_cell_once_written_stays"]
    a_guest_is_out_of_the_peoples_earshot["a_guest_is_out_of_the_peoples_earshot"]
    a_nag_is_an_owe["a_nag_is_an_owe"]
    a_nag_waits_on_nothing["a_nag_waits_on_nothing"]
    a_persons_own_word_is_heard_at_their_presence["a_persons_own_word_is_heard_at_their_presence"]
    a_role_that_hears_the_day_reads_the_sheet["a_role_that_hears_the_day_reads_the_sheet"]
    a_said_word_writes_its_cell["a_said_word_writes_its_cell"]
    a_seat_that_does_not_hear_it_reads_the_same["a_seat_that_does_not_hear_it_reads_the_same"]
    a_strike_keeps_every_cell["a_strike_keeps_every_cell"]
    a_strike_keeps_its_position["a_strike_keeps_its_position"]
    a_tick_moves_nothing["a_tick_moves_nothing"]
    a_walled_reply_is_unseen["a_walled_reply_is_unseen"]
    a_walled_word_does_not_move_the_edge["a_walled_word_does_not_move_the_edge"]
    a_word_is_a_round["a_word_is_a_round"]
    a_word_to_oneself_is_unread_at_every_other_seat["a_word_to_oneself_is_unread_at_every_other_seat"]
    a_word_to_oneself_leaves_no_remainder["a_word_to_oneself_leaves_no_remainder"]
    after_the_crossing_every_reading_stands["after_the_crossing_every_reading_stands"]
    an_ack_is_a_visit["an_ack_is_a_visit"]
    an_ack_is_never_withdrawn["an_ack_is_never_withdrawn"]
    an_ack_keeps_the_address["an_ack_keeps_the_address"]
    an_ack_keeps_the_author["an_ack_keeps_the_author"]
    an_ack_keeps_the_id["an_ack_keeps_the_id"]
    an_ack_keeps_the_ids["an_ack_keeps_the_ids"]
    an_ack_keeps_the_sheet["an_ack_keeps_the_sheet"]
    an_ack_keeps_the_test["an_ack_keeps_the_test"]
    an_edge_is_a_reading["an_edge_is_a_reading"]
    an_introduction_hears_through_the_seats_it_hears["an_introduction_hears_through_the_seats_it_hears"]
    an_unstruck_row_comes_back["an_unstruck_row_comes_back"]
    filter_crosses_append["filter_crosses_append"]
    foams_sheet_has_a_resistor["foams_sheet_has_a_resistor"]
    no_map_unsends_an_unsend["no_map_unsends_an_unsend"]
    no_open_end_is_decided["no_open_end_is_decided"]
    the_apps_sheet_is_conductive["the_apps_sheet_is_conductive"]
    the_couple_is_dark_to_the_others["the_couple_is_dark_to_the_others"]
    the_couple_read_it_one_seat_wider["the_couple_read_it_one_seat_wider"]
    the_couple_writing_is_unheard_by_the_room["the_couple_writing_is_unheard_by_the_room"]
    the_couples_probe_is_out_of_every_other_earshot["the_couples_probe_is_out_of_every_other_earshot"]
    the_couples_seat_parts_them["the_couples_seat_parts_them"]
    the_couples_word_is_a_door["the_couples_word_is_a_door"]
    the_crossing_is_a_reading["the_crossing_is_a_reading"]
    the_crossing_is_the_one_difference["the_crossing_is_the_one_difference"]
    the_day_at_rest_is_a_threshold["the_day_at_rest_is_a_threshold"]
    the_day_crosses_the_threshold["the_day_crosses_the_threshold"]
    the_day_is_a_reseat["the_day_is_a_reseat"]
    the_day_is_still["the_day_is_still"]
    the_day_rests_on_the_page_or_not_at_all["the_day_rests_on_the_page_or_not_at_all"]
    the_draft_leaves_no_remainder["the_draft_leaves_no_remainder"]
    the_narration_is_a_reading["the_narration_is_a_reading"]
    the_narration_reads_alike_at_every_seat["the_narration_reads_alike_at_every_seat"]
    the_open_ends_are_named["the_open_ends_are_named"]
    the_page_rests_when_every_word_rests["the_page_rests_when_every_word_rests"]
    the_room_is_covered_by_its_people["the_room_is_covered_by_its_people"]
    the_room_is_the_widest_seat["the_room_is_the_widest_seat"]
    the_room_reads_the_same_whatever_they_say["the_room_reads_the_same_whatever_they_say"]
    the_seen_edges_are_a_reading["the_seen_edges_are_a_reading"]
    the_shape_keeps_the_audience["the_shape_keeps_the_audience"]
    the_sheet_at_rest["the_sheet_at_rest"]
    the_sheet_is_a_reading_of_the_record["the_sheet_is_a_reading_of_the_record"]
    the_sheet_is_derived["the_sheet_is_derived"]
    the_sheet_is_the_days_probe["the_sheet_is_the_days_probe"]
    the_sheet_is_the_days_word["the_sheet_is_the_days_word"]
    the_sheets_lift_is_its_conduct["the_sheets_lift_is_its_conduct"]
    two_rooms_alike_to_the_people_are_alike_at_every_presence["two_rooms_alike_to_the_people_are_alike_at_every_presence"]
    two_rooms_part_only_at_a_presence["two_rooms_part_only_at_a_presence"]
    unsend_merges["unsend_merges"]
    unstrike_retracts_strike["unstrike_retracts_strike"]
  end
  subgraph Witness["Witness"]
    Witness_a_difference_out_of_the_cone_is_dark["a_difference_out_of_the_cone_is_dark"]
    Witness_a_narrower_seat_reads_no_more["a_narrower_seat_reads_no_more"]
    Witness_a_probe_no_seat_hears_is_dark["a_probe_no_seat_hears_is_dark"]
    Witness_a_seat_over_a_seat_is_derived["a_seat_over_a_seat_is_derived"]
    Witness_a_wall_hides_the_probe["a_wall_hides_the_probe"]
    Witness_a_word_hidden_in_the_body_is_unheard_in_the_narration["a_word_hidden_in_the_body_is_unheard_in_the_narration"]
    Witness_speak_now["speak_now"]
    Witness_the_ceremony_reseats_every_reading["the_ceremony_reseats_every_reading"]
    Witness_the_narration_reads_alike_at_every_seat["the_narration_reads_alike_at_every_seat"]
    Witness_the_probe_reads_the_seat["the_probe_reads_the_seat"]
    Witness_the_room_at_its_probes_reads_alike["the_room_at_its_probes_reads_alike"]
    Witness_the_room_is_the_widest_seat["the_room_is_the_widest_seat"]
    Witness_the_seat_that_hears_it_reads_it["the_seat_that_hears_it_reads_it"]
    Witness_the_word_at_the_door_is_unread_at_every_seat["the_word_at_the_door_is_unread_at_every_seat"]
  end
  subgraph Rest["Rest"]
    Rest_a_still_runner_rests_where_it_stands["a_still_runner_rests_where_it_stands"]
  end
  subgraph Threshold["Threshold"]
    Threshold_the_threshold_at_the_room["the_threshold_at_the_room"]
  end
  an_ack_keeps_the_test --> an_ack_keeps_the_author
  an_ack_keeps_the_test --> an_ack_keeps_the_address
  the_crossing_is_the_one_difference --> the_crossing_is_a_reading
  the_crossing_is_the_one_difference --> Witness_the_ceremony_reseats_every_reading
  the_sheet_is_a_reading_of_the_record --> an_ack_keeps_the_sheet
  the_sheet_is_a_reading_of_the_record --> a_said_word_writes_its_cell
  the_day_is_a_reseat --> Witness_the_word_at_the_door_is_unread_at_every_seat
  after_the_crossing_every_reading_stands --> Witness_the_word_at_the_door_is_unread_at_every_seat
  the_sheet_is_the_days_word --> the_sheet_is_a_reading_of_the_record
  the_day_rests_on_the_page_or_not_at_all --> Rest_a_still_runner_rests_where_it_stands
  the_narration_is_a_reading --> Witness_a_seat_over_a_seat_is_derived
  the_couples_seat_parts_them --> Witness_the_seat_that_hears_it_reads_it
  a_word_to_oneself_is_unread_at_every_other_seat --> Witness_a_wall_hides_the_probe
  a_strike_keeps_every_cell --> a_strike_keeps_its_position
  the_couples_word_is_a_door --> Witness_the_word_at_the_door_is_unread_at_every_seat
  no_map_unsends_an_unsend --> unsend_merges
  a_body_never_reaches_the_narration --> Witness_a_word_hidden_in_the_body_is_unheard_in_the_narration
  the_day_at_rest_is_a_threshold --> the_room_is_covered_by_its_people
  the_room_reads_the_same_whatever_they_say --> Witness_a_probe_no_seat_hears_is_dark
  a_word_to_oneself_leaves_no_remainder --> the_shape_keeps_the_audience
  an_ack_keeps_the_ids --> an_ack_keeps_the_id
  the_room_is_the_widest_seat --> Witness_the_room_is_the_widest_seat
  a_walled_reply_is_unseen --> Witness_a_wall_hides_the_probe
  a_walled_reply_is_unseen --> Witness_a_narrower_seat_reads_no_more
  a_walled_reply_is_unseen --> Witness_the_probe_reads_the_seat
  the_couple_is_dark_to_the_others --> Witness_a_difference_out_of_the_cone_is_dark
  two_rooms_alike_to_the_people_are_alike_at_every_presence --> Witness_the_room_at_its_probes_reads_alike
  two_rooms_alike_to_the_people_are_alike_at_every_presence --> the_room_is_covered_by_its_people
  the_sheet_at_rest --> the_day_rests_on_the_page_or_not_at_all
  the_sheet_at_rest --> the_sheet_is_the_days_word
  an_edge_is_a_reading --> Witness_a_seat_over_a_seat_is_derived
  a_seat_that_does_not_hear_it_reads_the_same --> Witness_a_wall_hides_the_probe
  a_said_word_writes_its_cell --> filter_crosses_append
  an_ack_keeps_the_sheet --> an_ack_keeps_the_ids
  an_ack_keeps_the_sheet --> an_ack_keeps_the_test
  a_walled_word_does_not_move_the_edge --> Witness_a_wall_hides_the_probe
  a_walled_word_does_not_move_the_edge --> Witness_a_narrower_seat_reads_no_more
  a_walled_word_does_not_move_the_edge --> Witness_the_probe_reads_the_seat
  unstrike_retracts_strike --> an_unstruck_row_comes_back
  the_narration_reads_alike_at_every_seat --> Witness_the_narration_reads_alike_at_every_seat
  the_day_crosses_the_threshold --> Threshold_the_threshold_at_the_room
  the_day_crosses_the_threshold --> the_day_at_rest_is_a_threshold
  the_seen_edges_are_a_reading --> Witness_a_seat_over_a_seat_is_derived
  a_tick_moves_nothing --> Rest_a_still_runner_rests_where_it_stands
  an_introduction_hears_through_the_seats_it_hears --> Witness_speak_now

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/here.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


CREATE TABLE message (
  id serial PRIMARY KEY,
  id integer NOT NULL,
  author integer NOT NULL,
  to_ integer[] NOT NULL,
  body integer NOT NULL,
  sent integer NOT NULL,
  reply_to integer[] NOT NULL,
  asked_of integer[] NOT NULL
);
CREATE TABLE message_acked_by (
  message_id integer NOT NULL REFERENCES message(id),
  position integer NOT NULL,
  c0 integer NOT NULL,
  c1 integer NOT NULL
);

CREATE TABLE room (
  id serial PRIMARY KEY
);
CREATE TABLE room_messages (
  room_id integer NOT NULL REFERENCES room(id),
  position integer NOT NULL,
  message_id integer NOT NULL REFERENCES message(id)
);

CREATE TABLE row (
  id serial PRIMARY KEY,
  position integer NOT NULL,
  time integer NOT NULL,
  what integer NOT NULL,
  struck boolean NOT NULL
);

CREATE TABLE runner (
  id serial PRIMARY KEY,
  m text NOT NULL,
  steer text NOT NULL,
  rest boolean NOT NULL
);

-- roomFace: a face over room whose probes are names — one reading, of the row and the probe
CREATE FUNCTION room_as_room_face(room_id integer, probe integer) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT x FROM unnest((SELECT array_agg(message_id ORDER BY position) FROM room_messages c WHERE c.room_id = room.id)) WITH ORDINALITY AS u(x, o) WHERE ⟨unread⟩ ORDER BY o) FROM room WHERE id = $1 $$;

-- narrationFace: a face over room whose probes are names — one reading, of the row and the probe
CREATE FUNCTION room_as_narration_face(room_id integer, probe integer) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT ⟨unread Prod.mk⟩ FROM unnest(ARRAY(SELECT x FROM unnest((SELECT array_agg(message_id ORDER BY position) FROM room_messages c WHERE c.room_id = room.id)) WITH ORDINALITY AS u(x, o) WHERE ⟨unread⟩ ORDER BY o)) WITH ORDINALITY AS u(x, o) ORDER BY o) FROM room WHERE id = $1 $$;

-- acked: derived, never stored
-- described by a_nag_is_an_owe, a_nag_waits_on_nothing, a_word_is_a_round, an_ack_is_a_visit, the_open_ends_are_named, the_page_rests_when_every_word_rests
CREATE FUNCTION acked(message_id integer) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT (x).c0 FROM unnest((SELECT array_agg(c ORDER BY position) FROM message_acked_by c WHERE c.message_id = message.id)) AS x ORDER BY (x).position) FROM message WHERE id = $1 $$;

-- ids: derived, never stored
-- described by an_ack_keeps_the_ids, the_sheet_is_the_days_probe
CREATE FUNCTION ids(message_ids integer[]) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT (SELECT id FROM message WHERE id = x) FROM unnest($1) WITH ORDINALITY AS u(x, o) ORDER BY o) $$;

-- shape: derived, not yet drawn (data over Here.Treaty.Message)

-- sheet_of: derived, not yet drawn (calls on_the_sheet, beyond the fragment)

-- heardAt: derived, never stored
-- described by a_body_never_reaches_the_narration, a_persons_own_word_is_heard_at_their_presence, an_introduction_hears_through_the_seats_it_hears, the_couples_seat_parts_them, the_narration_reads_alike_at_every_seat
CREATE FUNCTION heard_at(room_id integer, arg2 integer) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT x FROM unnest((SELECT array_agg(message_id ORDER BY position) FROM room_messages c WHERE c.room_id = room.id)) WITH ORDINALITY AS u(x, o) WHERE (((SELECT author FROM message WHERE id = x) = arg2) OR (arg2 = ANY(SELECT unnest((SELECT to_ FROM message WHERE id = x))))) ORDER BY o) FROM room WHERE id = $1 $$;

-- narrate: derived, not yet drawn (calls shape, beyond the fragment)

-- writeRow: derived, never stored
CREATE FUNCTION write_row(row_id integer, arg2 integer[]) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT (SELECT hAppend FROM h_append WHERE id = ARRAY[row]::integer[]) FROM row WHERE id = $1 $$;

-- roomBodies: derived, never stored
CREATE FUNCTION room_bodies(room_id integer) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT (SELECT body FROM message WHERE id = x) FROM unnest((SELECT array_agg(message_id ORDER BY position) FROM room_messages c WHERE c.room_id = room.id)) WITH ORDINALITY AS u(x, o) ORDER BY o) FROM room WHERE id = $1 $$;

-- positions: derived, never stored
-- described by a_strike_keeps_every_cell
CREATE FUNCTION positions(row_ids integer[]) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT (SELECT position FROM $1 WHERE id = x) FROM unnest($1) WITH ORDINALITY AS u(x, o) ORDER BY o) $$;

-- bodies: derived, never stored
CREATE FUNCTION bodies(message_ids integer[]) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT (SELECT body FROM message WHERE id = x) FROM unnest($1) WITH ORDINALITY AS u(x, o) ORDER BY o) $$;

-- rowCodes: derived, not yet drawn (data over List Here.Treaty.Row)

-- crossed: derived, not yet drawn (prop over Here.Treaty.Room)

-- alone: derived, not yet drawn (prop over Here.Treaty.Message)

-- humanOnly: derived, not yet drawn (prop over Here.Treaty.Message)

-- onThePage: derived, not yet drawn (prop over Here.Treaty.Room)

-- onTheSheet: derived, not yet drawn (prop over Here.Treaty.Message)

-- act: a clerk over a has-many field (messages) — not yet drawn

-- seat: derived, not yet drawn (calls hears_of, beyond the fragment)

-- introduced: derived, not yet drawn (a function over Nat)

-- speaks: derived, not yet drawn (calls introduced, beyond the fragment)

-- hearsOf: derived, not yet drawn (a function over Nat)

-- openEnds: derived, never stored
-- described by a_nag_waits_on_nothing, no_open_end_is_decided
CREATE FUNCTION open_ends(message_id integer) RETURNS integer LANGUAGE sql STABLE AS $$
  SELECT cardinality(ARRAY(SELECT x FROM unnest(message.asked_of) WITH ORDINALITY AS u(x, o) WHERE NOT (x = ANY(SELECT unnest(acked(message.id)))) ORDER BY o)) FROM message WHERE id = $1 $$;

-- waitingOn: derived, never stored
CREATE FUNCTION waiting_on(message_id integer) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT x FROM unnest(message.asked_of) WITH ORDINALITY AS u(x, o) WHERE (NOT (x = ANY(SELECT unnest(acked(message.id))))) ORDER BY o) FROM message WHERE id = $1 $$;

-- decided: a check, derived, never stored
-- described by a_word_is_a_round, an_ack_is_never_withdrawn, no_open_end_is_decided, the_open_ends_are_named
CREATE FUNCTION decided(message_id integer) RETURNS boolean LANGUAGE sql STABLE AS $$
  SELECT (message.asked_of <@ acked(message.id)) FROM message WHERE id = $1 $$;

-- weightOf: derived, never stored
CREATE FUNCTION weight_of(room_id integer) RETURNS integer LANGUAGE sql STABLE AS $$
  SELECT (SELECT coalesce(sum(x), 0) FROM unnest(ARRAY(SELECT open_ends(x) FROM unnest((SELECT array_agg(message_id ORDER BY position) FROM room_messages c WHERE c.room_id = room.id)) WITH ORDINALITY AS u(x, o) ORDER BY o)) AS x) FROM room WHERE id = $1 $$;