eih — a product as an assay, grown from assays/eih.lean

import Witness
import Roster
open Room Face Witness Roster
set_option autoImplicit false

namespace Eih.Treaty

structure Request where
  channel : Nat
  audience : List Nat
  sender : Nat
  confirmed : List Nat

def asked (q : Request) : List Nat := q.audience.filter (fun m => !(Nat.beq m q.sender))

def tally (q : Request) : Nat := (q.confirmed.filter (enrolled Nat.beq (asked q))).length

def heardBy (q : Request) (m : Nat) : List Nat := cond (enrolled Nat.beq q.audience m) q.confirmed []

def confirm (q : Request) (m : Nat) : Request := { q with confirmed := m :: q.confirmed }

def settled (q : Request) : Bool := everyone Nat.beq (asked q) q.confirmed

def unanswered (qs : List Request) : List Request := qs.filter (fun q => !(settled q))

def inChannel (qs : List Request) (ch : Nat) : List Nat :=
  joinMap (fun q => q.confirmed) (qs.filter (fun q => Nat.beq q.channel ch))

structure Room where
  guests : List Party
  delivered : List Nat
  ledger : List (Nat × Nat × Nat)
  timeline : List Nat
  bach : List Nat
  requests : List Request

def deliver (r : Room) : Room := { r with delivered := sheet r.guests }

def withGuests (r : Room) (gl : List Party) : Room := { r with guests := gl }

def withBach (r : Room) (b : List Nat) : Room := { r with bach := b }

def confirmIn (r : Room) (ch m : Nat) : Room :=
  { r with requests := r.requests.map (fun q => cond (Nat.beq q.channel ch) (confirm q m) q) }

def ask (r : Room) (ch : Nat) (audience : List Nat) (sender : Nat) : Room :=
  { r with requests := ⟨ch, audience, sender, []⟩ :: r.requests }

def withLine (r : Room) (e : Nat × Nat × Nat) : Room := { r with ledger := e :: r.ledger }

def allClear (r : Room) : Prop :=
  r.delivered = sheet r.guests ∧ unanswered r.requests = []

inductive Ask where
  | guests | sheet | ledger | timeline | bach | confirmed | vendorRoom

def Ask.code : Ask → Nat
  | .guests => 0 | .sheet => 1 | .ledger => 2 | .timeline => 3 | .bach => 4 | .confirmed => 5 | .vendorRoom => 6

def Ask.beq (a b : Ask) : Bool := Nat.beq a.code b.code

def readRoom (r : Room) : Ask → List Nat
  | .guests => r.guests.map (·.name)
  | .sheet => r.delivered
  | .ledger => r.ledger.map (·.2.2)
  | .timeline => r.timeline
  | .bach => r.bach
  | .confirmed => inChannel r.requests 0
  | .vendorRoom => inChannel r.requests 1

def roomFace : Face := ⟨Room, Ask, List Nat, readRoom⟩

def roomSeat : List Ask := [.guests, .sheet, .ledger, .timeline, .bach, .confirmed, .vendorRoom]

def coupleSeat : List Ask := [.guests, .sheet, .ledger, .timeline, .confirmed]

def lindaSeat : List Ask := [.guests, .timeline, .confirmed]

def bestManSeat : List Ask := [.timeline, .bach, .confirmed]

def catererSeat : List Ask := [.timeline, .sheet, .confirmed, .vendorRoom]

def humanSeats : List (List Ask) := [coupleSeat, lindaSeat, bestManSeat, catererSeat]

def coupleSideSeats : List (List Ask) := [coupleSeat, lindaSeat, bestManSeat]

inductive VendorAsk where
  | timeline | mine

def vendorFace (v : Nat) : Face :=
  ⟨Room, VendorAsk, List Nat, fun r q => match q with
    | .timeline => r.timeline
    | .mine => (r.ledger.filter (fun e => Nat.beq e.1 v)).map (·.2.2)⟩

def makerFace : Face := ⟨Room, Unit, Nat, fun r _ => r.guests.length⟩

structure Channel where
  audience : List Nat

structure File where
  channel : Channel

def visible (f : File) (m : Nat) : Prop := m ∈ f.channel.audience

def canSee (f : File) (m : Nat) : Bool := enrolled Nat.beq f.channel.audience m

inductive Role where
  | couple | planner | vendor | venue | party

def Role.code : Role → Nat
  | .couple => 0 | .planner => 1 | .vendor => 2 | .venue => 3 | .party => 4

def Role.beq (a b : Role) : Bool := Nat.beq a.code b.code

def joinsFree : Role → Bool := fun _ => true

def pays : Role → Bool
  | .couple => true | .vendor => true | .planner => true | .venue => true | .party => false

def samePage (qs : List Request) (v : Nat) : Nat :=
  ((qs.filter (fun q => enrolled Nat.beq q.audience v)).map tally).sum

inductive Thing where
  | wedding | season

def owner : Thing → Role
  | .wedding => .couple | .season => .vendor

structure Bill where
  thing : Thing
  payer : Role

def lawful (b : Bill) : Bool := Role.beq b.payer (owner b.thing) || (Role.beq b.payer .vendor && Role.beq (owner b.thing) .couple)

inductive Page where
  | floorPlan | guestList | samePage | invoices | budget | guests | site | team | dayOf | tasks

def Page.code : Page → Nat
  | .floorPlan => 0 | .guestList => 1 | .samePage => 2 | .invoices => 3 | .budget => 4
  | .guests => 5 | .site => 6 | .team => 7 | .dayOf => 8 | .tasks => 9

def Page.beq (a b : Page) : Bool := Nat.beq a.code b.code

def roles : List Role := [.couple, .planner, .vendor, .venue, .party]

def pages : List Page := [.floorPlan, .guestList, .samePage, .invoices, .budget, .guests, .site, .team, .dayOf, .tasks]

def seen : Role → List Page
  | .couple => pages
  | .planner => [.floorPlan, .guestList, .samePage, .invoices, .team, .dayOf, .tasks]
  | .vendor => [.floorPlan, .samePage, .invoices, .team, .dayOf, .tasks]
  | .venue => [.floorPlan, .samePage, .invoices, .team, .dayOf, .tasks]
  | .party => [.floorPlan, .guestList, .samePage, .team, .dayOf, .tasks]

def edited : Role → List Page
  | .couple => pages
  | .planner => [.floorPlan, .guestList, .invoices, .team, .dayOf, .tasks]
  | .vendor => [.invoices, .dayOf, .tasks]
  | .venue => [.floorPlan, .invoices, .dayOf, .tasks]
  | .party => [.floorPlan, .guestList, .dayOf, .tasks]

def sees (ρ : Role) (p : Page) : Bool := enrolled Page.beq (seen ρ) p

def edits (ρ : Role) (p : Page) : Bool := enrolled Page.beq (edited ρ) p

def withinSight : Bool := roles.all (fun ρ => pages.all (fun p => !(edits ρ p) || sees ρ p))

structure Member where
  user : Nat
  role : Role
  kind : Nat
  dayLane : Bool
  arrival : Nat
  phone : Nat

def vendorSide (m : Member) : Bool :=
  Role.beq m.role .vendor || (Role.beq m.role .venue || Role.beq m.role .planner)

def vendorRoomMembers (roster : List Member) : List Member := roster.filter vendorSide

def vendorRoomAudience (roster : List Member) : List Nat := (vendorRoomMembers roster).map (·.user)

def channelAudience (roster : List Member) (p : Member → Bool) : List Nat := (roster.filter p).map (·.user)

def vendorRoomRequestOf (roster : List Member) (sender : Nat) (confirmed : List Nat) : Request :=
  ⟨1, vendorRoomAudience roster, sender, confirmed⟩

structure Task where
  owner : Nat
  assignee : Nat
  done : Bool

def mayClose (m : Member) (t : Task) : Bool :=
  Nat.beq m.user t.owner || (Role.beq m.role .couple || Role.beq m.role .planner)

def close (t : Task) : Task := { t with done := true }

def assign (t : Task) (to : Nat) : Task := { t with assignee := to }

def mayOpen (_ : Member) : Bool := true

def memberSees (m : Member) (p : Page) : Bool := sees m.role p && !(m.dayLane && Page.beq p .tasks)

def memberEdits (m : Member) (p : Page) : Bool := edits m.role p && memberSees m p

def dayOfIsEveryones : Bool := roles.all (fun ρ => !(sees ρ .dayOf) || edits ρ .dayOf)

structure DayOfEdit where
  who : Nat
  row : Nat
  before : Nat
  after : Nat

def dayOfLog : Machine DayOfEdit (List DayOfEdit) := ledger DayOfEdit

def undo : List Nat → List Nat
  | [] => []
  | [_] => []
  | x :: y :: w => x :: undo (y :: w)

structure Table where
  shape : Nat
  occupants : List Nat

def venueTable (t : Table) : Nat × Nat := (t.shape, t.occupants.length)

def venueChart (c : List Table) : List (Nat × Nat) := c.map venueTable

def seasonView (rs : List Room) (v : Nat) : List (List Nat) := rs.map (fun r => (vendorFace v).obs r .mine)

def seasonOwed (rs : List Room) (v : Nat) : Nat := (joinMap (fun r => (vendorFace v).obs r .mine) rs).sum

def rose : Party := ⟨1, true, [2, 3]⟩

def linda : Party := ⟨2, true, [1]⟩

def cousin : Party := ⟨3, false, [1, 1]⟩

def guestList : List Party := [linda, cousin, rose]

def everyoneChannel : Request := ⟨0, [1, 2, 7, 8, 9], 1, [7, 8]⟩

def vendorRoomRequest : Request := ⟨1, [7, 8, 9], 9, [7]⟩

def demo : Room := ⟨guestList, [], [(7, 1, 900), (8, 1, 1200)], [10, 11, 12], [42], [everyoneChannel, vendorRoomRequest]⟩
#guard readRoom demo .confirmed == [7, 8]
#guard readRoom demo .vendorRoom == [7]

#guard sheet guestList == [1, 2, 3]
#guard heads guestList == 3
#guard (deliver demo).delivered == [1, 2, 3]
#guard demo.delivered == []
#guard readRoom (deliver demo) .sheet == [1, 2, 3]
#guard readRoom demo .guests == [2, 3, 1]

def floristSees : List Nat := (vendorFace 7).obs demo .mine
#guard floristSees == [900]

def djSees : List Nat := (vendorFace 8).obs demo .mine
#guard djSees == [1200]

def catererSees : List (List Nat) := reads roomFace catererSeat (deliver demo)
#guard catererSees == [[10, 11, 12], [1, 2, 3], [7, 8], [7]]

def lindaSees : List (List Nat) := reads roomFace lindaSeat demo
#guard lindaSees == [[2, 3, 1], [10, 11, 12], [7, 8]]

def bestManSees : List (List Nat) := reads roomFace bestManSeat demo
#guard bestManSees == [[10, 11, 12], [42], [7, 8]]

def coupleSees : List (List Nat) := reads roomFace coupleSeat demo
#guard coupleSees == [[2, 3, 1], [], [900, 1200], [10, 11, 12], [7, 8]]

def roomSees : List (List Nat) := reads roomFace roomSeat demo
#guard roomSees.length == 7

def makerSees : Nat := makerFace.obs demo ()
#guard makerSees == 3
#guard joinsFree .party && !(pays .party)

def moreGuests : Room := withGuests demo (rose :: guestList)

def makerSeesMore : Nat := makerFace.obs moreGuests ()
#guard makerSeesMore == 4

def catererSeesMore : List (List Nat) := reads roomFace catererSeat moreGuests
#guard catererSeesMore == reads roomFace catererSeat demo

def newBach : Room := withBach demo [43]

def bestManSeesNew : List (List Nat) := reads roomFace bestManSeat newBach
#guard bestManSeesNew == [[10, 11, 12], [43], [7, 8]]

def coupleSeesNew : List (List Nat) := reads roomFace coupleSeat newBach
#guard coupleSeesNew == coupleSees

def allConfirmed : Room := confirmIn (confirmIn demo 0 2) 0 9
#guard readRoom allConfirmed .confirmed == [9, 2, 7, 8]

def roomSeesConfirmed : List (List Nat) := reads roomFace roomSeat allConfirmed
#guard roomSeesConfirmed != roomSees

def lindaSeesConfirmed : List (List Nat) := reads roomFace lindaSeat allConfirmed
#guard lindaSeesConfirmed != lindaSees

def vendorConfirmed : Room := confirmIn demo 1 8
#guard readRoom vendorConfirmed .vendorRoom == [8, 7]

def lindaSeesVendorConfirmed : List (List Nat) := reads roomFace lindaSeat vendorConfirmed
#guard lindaSeesVendorConfirmed == lindaSees

def coupleSeesVendorConfirmed : List (List Nat) := reads roomFace coupleSeat vendorConfirmed
#guard coupleSeesVendorConfirmed == coupleSees

def catererSeesDemo : List (List Nat) := reads roomFace catererSeat demo

def catererSeesVendorConfirmed : List (List Nat) := reads roomFace catererSeat vendorConfirmed
#guard catererSeesVendorConfirmed != catererSeesDemo
#guard settled everyoneChannel == false
#guard settled (confirm (confirm everyoneChannel 2) 9)
#guard (unanswered demo.requests).length == 2
#guard (unanswered allConfirmed.requests).length == 1
#guard (unanswered (confirmIn allConfirmed 1 8).requests).length == 0

def withInvoice : Room := withLine demo (9, 1, 300)

def lindaSeesInvoice : List (List Nat) := reads roomFace lindaSeat withInvoice
#guard lindaSeesInvoice == lindaSees

def humanEars : List Ask := earshot roomFace humanSeats
#guard humanEars.length == 15
#guard enrolled Ask.beq humanEars .confirmed == true
#guard enrolled Ask.beq humanEars .ledger == true
#guard enrolled Ask.beq humanEars .vendorRoom == true

def coupleSideEars : List Ask := earshot roomFace coupleSideSeats
#guard enrolled Ask.beq coupleSideEars .vendorRoom == false
#guard everyone Nat.beq (asked everyoneChannel) (confirm (confirm everyoneChannel 2) 9).confirmed
#guard !(everyone Nat.beq (asked everyoneChannel) everyoneChannel.confirmed)

def maya : Nat := 1

def jordan : Nat := 7
#guard asked everyoneChannel == [2, 7, 8, 9]
#guard tally everyoneChannel == 2
#guard heardBy everyoneChannel jordan == [7, 8]
#guard heardBy everyoneChannel maya == [7, 8]
#guard heardBy vendorRoomRequest maya == []
#guard heardBy vendorRoomRequest jordan == [7]
#guard tally (confirm everyoneChannel 2) == 3
#guard samePage [everyoneChannel, vendorRoomRequest] maya == 2
#guard samePage [everyoneChannel, vendorRoomRequest] jordan == 3

def coveredWedding : Bill := ⟨.wedding, .vendor⟩

def ownWedding : Bill := ⟨.wedding, .couple⟩

def strayBill : Bill := ⟨.season, .couple⟩
#guard lawful coveredWedding && lawful ownWedding && !(lawful strayBill)
#guard Role.beq (owner coveredWedding.thing) .couple
#guard withinSight
#guard sees .venue .floorPlan && edits .venue .floorPlan && !(sees .venue .guestList)
#guard sees .vendor .floorPlan && !(edits .vendor .floorPlan)
#guard pays .venue && joinsFree .venue && !(pays .party)

def vendorRoomChannel : Channel := ⟨[7, 8, 9]⟩

def vendorRoomFile : File := ⟨vendorRoomChannel⟩
#guard !(canSee vendorRoomFile maya)
#guard canSee vendorRoomFile jordan

def mayaM : Member := ⟨1, .couple, 0, false, 15, 0⟩

def lindaM : Member := ⟨2, .party, 0, true, 14, 0⟩

def jordanM : Member := ⟨7, .vendor, 1, false, 12, 0⟩

def djM : Member := ⟨8, .vendor, 2, false, 13, 0⟩

def sofiaM : Member := ⟨9, .vendor, 3, false, 11, 0⟩

def roster : List Member := [mayaM, lindaM, jordanM, djM, sofiaM]
#guard vendorRoomAudience roster == [7, 8, 9]
#guard !(enrolled Nat.beq (vendorRoomAudience roster) 1)
#guard !(enrolled Nat.beq (vendorRoomAudience roster) 2)
#guard (vendorRoomRequestOf roster 9 [7]).audience == vendorRoomRequest.audience
#guard vendorRoomAudience [mayaM, lindaM, jordanM] == [7]

def loadIn : Task := ⟨7, 7, false⟩
#guard mayClose jordanM loadIn && mayClose mayaM loadIn && !(mayClose sofiaM loadIn)
#guard (close loadIn).done
#guard (assign loadIn 9).assignee == 9
#guard mayOpen sofiaM && mayOpen lindaM
#guard !(memberSees lindaM .tasks) && memberSees lindaM .dayOf && memberEdits lindaM .dayOf
#guard memberSees jordanM .tasks && memberEdits jordanM .tasks
#guard !(memberEdits lindaM .tasks)
#guard pages.all (fun p => !(memberSees lindaM p) || sees .party p)
#guard dayOfIsEveryones
#guard undo [1, 2, 3] == [1, 2]
#guard undo [1] == []

def firstEdit : DayOfEdit := ⟨9, 3, 100, 130⟩

def secondEdit : DayOfEdit := ⟨7, 5, 600, 615⟩
#guard (behavior dayOfLog [firstEdit, secondEdit]).length == 2
#guard (behavior dayOfLog [firstEdit, secondEdit]).map (·.who) == [9, 7]

def headTable : Table := ⟨0, [1, 2, 3]⟩

def table2 : Table := ⟨1, [4]⟩
#guard venueChart [headTable, table2] == [(0, 3), (1, 1)]
#guard venueChart [⟨0, [4, 5, 6]⟩, table2] == venueChart [headTable, table2]
#guard seasonView [demo, withInvoice] 7 == [[900], [900]]
#guard seasonView [demo, withInvoice] 9 == [[], [300]]
#guard seasonOwed [demo, withInvoice] 7 == 1800
#guard seasonOwed [demo, withInvoice] 9 == 300

theorem the_delivery_is_the_sheet (r : Room) : (deliver r).delivered = sheet r.guests :=
  rfl

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

theorem the_delivery_moves_no_guest (r : Room) : (deliver r).guests = r.guests :=
  rfl

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

theorem everyone_clear_means_every_request_settled (r : Room) (h : allClear r) :
    ∀ q, q ∈ r.requests → settled q = true := fun q hq => by
  cases hs : settled q with
  | true => rfl
  | false =>
      have hm : q ∈ unanswered r.requests :=
        mem_filter_intro r.requests hq (by show (!(settled q)) = true; rw [hs]; rfl)
      rw [h.2] at hm
      exact nomatch hm

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

theorem a_line_touches_only_the_ledger (r : Room) (e : Nat × Nat × Nat) :
    differOnly roomFace (withLine r e) r .ledger :=
  fun q hq => by cases q <;> first | rfl | exact absurd rfl hq

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

theorem the_bach_touches_only_the_bach (r : Room) (b : List Nat) :
    differOnly roomFace (withBach r b) r .bach :=
  fun q hq => by cases q <;> first | rfl | exact absurd rfl hq

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

theorem a_confirmation_elsewhere_leaves_a_channel (ch ch' m : Nat) (h : Nat.beq ch ch' = false) :
    ∀ qs : List Request,
      (qs.map (fun q => cond (Nat.beq q.channel ch) (confirm q m) q)).filter (fun q => Nat.beq q.channel ch')
        = qs.filter (fun q => Nat.beq q.channel ch')
  | [] => rfl
  | q :: qs => by
      show (cond (Nat.beq q.channel ch) (confirm q m) q :: qs.map (fun q => cond (Nat.beq q.channel ch) (confirm q m) q)).filter (fun q => Nat.beq q.channel ch')
        = (q :: qs).filter (fun q => Nat.beq q.channel ch')
      cases hc : Nat.beq q.channel ch with
      | true =>
          have hq : q.channel = ch := eq_of_beq _ _ hc
          have hn : Nat.beq q.channel ch' = false := by rw [hq]; exact h
          show (confirm q m :: qs.map (fun q => cond (Nat.beq q.channel ch) (confirm q m) q)).filter (fun q => Nat.beq q.channel ch')
            = (q :: qs).filter (fun q => Nat.beq q.channel ch')
          rw [List.filter_cons_of_neg (p := fun q => Nat.beq q.channel ch') (a := confirm q m) (ne_true_of_eq_false hn),
              List.filter_cons_of_neg (p := fun q => Nat.beq q.channel ch') (a := q) (ne_true_of_eq_false hn)]
          exact a_confirmation_elsewhere_leaves_a_channel ch ch' m h qs
      | false =>
          show (q :: qs.map (fun q => cond (Nat.beq q.channel ch) (confirm q m) q)).filter (fun q => Nat.beq q.channel ch')
            = (q :: qs).filter (fun q => Nat.beq q.channel ch')
          cases hc' : Nat.beq q.channel ch' with
          | true =>
              rw [List.filter_cons_of_pos (p := fun q => Nat.beq q.channel ch') (a := q) hc',
                  List.filter_cons_of_pos (p := fun q => Nat.beq q.channel ch') (a := q) hc',
                  a_confirmation_elsewhere_leaves_a_channel ch ch' m h qs]
          | false =>
              rw [List.filter_cons_of_neg (p := fun q => Nat.beq q.channel ch') (a := q) (ne_true_of_eq_false hc'),
                  List.filter_cons_of_neg (p := fun q => Nat.beq q.channel ch') (a := q) (ne_true_of_eq_false hc'),
                  a_confirmation_elsewhere_leaves_a_channel ch ch' m h qs]

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

theorem the_guests_touch_only_the_guests (r : Room) (gl : List Party) :
    differOnly roomFace (withGuests r gl) r .guests :=
  fun q hq => by cases q <;> first | rfl | exact absurd rfl hq

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

theorem a_vendor_never_sees_anothers_invoice (v w : Nat) (hvw : Nat.beq w v = false) (r : Room)
    (amount to : Nat) :
    alike (vendorFace v) (withLine r (w, to, amount)) r := by
  intro q
  cases q with
  | timeline => rfl
  | mine =>
      show ((( w, to, amount) :: r.ledger).filter (fun e => Nat.beq e.1 v)).map (·.2.2)
        = (r.ledger.filter (fun e => Nat.beq e.1 v)).map (·.2.2)
      rw [List.filter, hvw]

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

theorem an_ask_reads_itself : ∀ q : Ask, Ask.beq q q = true :=
  by (intros; (apply Room.beq_self <;> fail))

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

theorem a_vendor_sees_only_their_own (v : Nat) (r : Room) :
    (vendorFace v).obs r .mine = (r.ledger.filter (fun e => Nat.beq e.1 v)).map (·.2.2) :=
  rfl

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

theorem linda_never_sees_the_ledger (r : Room) (e : Nat × Nat × Nat) :
    reads roomFace lindaSeat (withLine r e) = reads roomFace lindaSeat r :=
  rfl

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

theorem the_caterer_never_sees_the_ledger (r : Room) (e : Nat × Nat × Nat) :
    reads roomFace catererSeat (withLine r e) = reads roomFace catererSeat r :=
  rfl

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

theorem the_caterer_never_sees_the_guests (r : Room) (gl : List Party) :
    reads roomFace catererSeat (withGuests r gl) = reads roomFace catererSeat r :=
  rfl

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

theorem the_bach_parts_the_best_man (r : Room) (b : List Nat) (hb : b ≠ r.bach) :
    reads roomFace bestManSeat (withBach r b) ≠ reads roomFace bestManSeat r :=
  by
    (intros;
      (apply Witness.the_seat_that_hears_it_reads_it (p := Ask.bach) <;>
          first
          | assumption
          | (apply List.Mem.tail; exact List.Mem.head _)))

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

theorem a_confirmation_parts_the_audience (r : Room) (m : Nat)
    (h : readRoom (confirmIn r 0 m) .confirmed ≠ readRoom r .confirmed) :
    reads roomFace coupleSeat (confirmIn r 0 m) ≠ reads roomFace coupleSeat r :=
  by
    (intros;
      (apply Witness.the_seat_that_hears_it_reads_it (p := Ask.confirmed) <;>
          first
          | assumption
          |
            (apply List.Mem.tail;
              (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _))))))

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

theorem the_room_covers_itself : covers roomFace [roomSeat] :=
  by
    (intros; (try dsimp only [roomSeat, Witness.covers, roomFace] at *); intro x; induction x;
      all_goals
        (intros;
          first
          | (apply Room.mem_joinMap_intro <;> exact List.Mem.head _)
          |
            (apply Room.mem_joinMap_intro <;>
                first
                | exact List.Mem.head _
                | (apply List.Mem.tail; exact List.Mem.head _))
          |
            (apply Room.mem_joinMap_intro <;>
                first
                | exact List.Mem.head _
                | (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _)))
          |
            (apply Room.mem_joinMap_intro <;>
                first
                | exact List.Mem.head _
                | (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _))))
          |
            (apply Room.mem_joinMap_intro <;>
                first
                | exact List.Mem.head _
                |
                  (apply List.Mem.tail;
                    (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _)))))
          |
            (apply Room.mem_joinMap_intro <;>
                first
                | exact List.Mem.head _
                |
                  (apply List.Mem.tail;
                    (apply List.Mem.tail;
                      (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _))))))
          |
            (apply Room.mem_joinMap_intro <;>
                first
                | exact List.Mem.head _
                |
                  (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: 'Eih.Treaty.the_room_covers_itself' does not depend on any axioms -/
#guard_msgs in #print axioms the_room_covers_itself

theorem the_room_witnesses_the_license (x y : Room)
    (hw : witnessed roomFace [roomSeat] x y) : alike roomFace x y :=
  by
    (intros; (try dsimp only [Witness.witnessed, roomSeat, Room, roomFace] at *); intro x; induction x;
      all_goals
        (intros;
          first
          |
            (apply Witness.speak_now <;>
                first
                | assumption
                | exact List.Mem.head _)
          |
            (apply Witness.speak_now <;>
                first
                | assumption
                | (apply List.Mem.tail; exact List.Mem.head _))
          |
            (apply Witness.speak_now <;>
                first
                | assumption
                | (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _)))
          |
            (apply Witness.speak_now <;>
                first
                | assumption
                | (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _))))
          |
            (apply Witness.speak_now <;>
                first
                | assumption
                |
                  (apply List.Mem.tail;
                    (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _)))))
          |
            (apply Witness.speak_now <;>
                first
                | assumption
                |
                  (apply List.Mem.tail;
                    (apply List.Mem.tail;
                      (apply List.Mem.tail; (apply List.Mem.tail; (apply List.Mem.tail; exact List.Mem.head _))))))
          |
            (apply Witness.speak_now <;>
                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; exact List.Mem.head _)))))))))

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

theorem the_caterer_reads_the_delivery (r : Room) :
    readRoom (deliver r) .sheet = sheet r.guests :=
  rfl

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

theorem a_file_is_never_wider_than_its_channel (f : File) (m : Nat) :
    visible f m ↔ m ∈ f.channel.audience :=
  Iff.rfl

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

theorem a_vendor_room_file_is_absent_from_the_couples_files (f : File) (couple : Nat)
    (h : canSee f couple = false) : ¬ visible f couple :=
  by
    (intros;
      (apply Room.the_unenrolled_are_no_member <;>
          first
          | (apply Room.beq_self <;> fail)
          | assumption))

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

theorem join_and_pay_are_unrelated : ∀ ρ : Role, joinsFree ρ = true :=
  fun _ => rfl

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

theorem the_party_never_pays : pays .party = false :=
  rfl

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

theorem lanes_shrink_never_lock (m : Member) (p : Page) (h : memberSees m p = true) : sees m.role p = true :=
  (and_reads _ _ h).1

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

theorem the_day_lane_sees_no_task_list (m : Member) (h : m.dayLane = true) : memberSees m .tasks = false := by
  show (sees m.role .tasks && !(m.dayLane && Page.beq .tasks .tasks)) = false
  rw [h]
  cases sees m.role .tasks <;> rfl

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

theorem the_day_lane_keeps_the_day_of_sheet (m : Member) (h : m.role = .party) : memberSees m .dayOf = true := by
  show (sees m.role .dayOf && !(m.dayLane && Page.beq .dayOf .tasks)) = true
  rw [h]
  cases m.dayLane <;> rfl

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

theorem an_edit_is_within_the_lane (m : Member) (p : Page) (h : memberEdits m p = true) : memberSees m p = true :=
  (and_reads _ _ h).2

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

theorem the_maker_sees_shape_not_content (r : Room) (gl gl' : List Party)
    (h : gl.length = gl'.length) : alike makerFace (withGuests r gl) (withGuests r gl') :=
  by
    (intros; (try dsimp only [Roster.Party, Room, withGuests, makerFace] at *); intro x; induction x;
      all_goals (intros; assumption))

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

theorem everyone_clear_means_rose_ate (r : Room) (h : allClear r)
    {p : Party} (hp : p ∈ r.guests) (hr : p.rsvp = true) {m : Nat} (hm : m ∈ p.meals) :
    m ∈ r.delivered := by
  rw [h.1]
  exact a_yes_reaches_the_sheet hp hr hm

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

theorem the_audience_hears_the_receipt_by_name (q : Request) (m : Nat)
    (h : enrolled Nat.beq q.audience m = true) : heardBy q m = q.confirmed :=
  by (intros; (try dsimp only [heardBy, Request] at *); intros; (rw [h]; rfl))

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

theorem outside_the_audience_hears_no_receipt (q : Request) (m x : Nat)
    (h : enrolled Nat.beq q.audience m = false) : heardBy (confirm q x) m = heardBy q m :=
  by (intros; (try dsimp only [confirm, heardBy, Request] at *); intros; (rw [h]; rfl))

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

theorem the_sender_is_never_asked (q : Request) : ¬ q.sender ∈ asked q := by
  intro h
  have hq := filter_holds q.audience h
  have hs : (!(Nat.beq q.sender q.sender)) = true := hq
  rw [beq_self] at hs
  exact nomatch hs

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

theorem the_same_page_counts_only_within_earshot (q : Request) (qs : List Request) (v : Nat)
    (h : enrolled Nat.beq q.audience v = false) : samePage (q :: qs) v = samePage qs v := by
  show (((q :: qs).filter (fun q => enrolled Nat.beq q.audience v)).map tally).sum
    = ((qs.filter (fun q => enrolled Nat.beq q.audience v)).map tally).sum
  rw [List.filter_cons_of_neg (p := fun q => enrolled Nat.beq q.audience v) (a := q) (ne_true_of_eq_false h)]

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

theorem the_same_page_hears_its_own_earshot (q : Request) (qs : List Request) (v : Nat)
    (h : enrolled Nat.beq q.audience v = true) : samePage (q :: qs) v = tally q + samePage qs v := by
  show (((q :: qs).filter (fun q => enrolled Nat.beq q.audience v)).map tally).sum
    = tally q + ((qs.filter (fun q => enrolled Nat.beq q.audience v)).map tally).sum
  rw [List.filter_cons_of_pos (p := fun q => enrolled Nat.beq q.audience v) (a := q) h]
  exact rfl

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

theorem a_covered_wedding_is_still_the_couples (b : Bill) (h : b.thing = .wedding) : owner b.thing = .couple := by
  rw [h]
  rfl

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

theorem the_payer_is_the_owner_or_the_host (b : Bill) (h : lawful b = true) :
    Role.beq b.payer (owner b.thing) = true ∨ (Role.beq b.payer .vendor = true ∧ Role.beq (owner b.thing) .couple = true) := by
  cases hp : Role.beq b.payer (owner b.thing) with
  | true => exact Or.inl rfl
  | false =>
      have h' : (Role.beq b.payer (owner b.thing) || (Role.beq b.payer .vendor && Role.beq (owner b.thing) .couple)) = true := h
      rw [hp] at h'
      exact Or.inr (and_reads _ _ h')

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

theorem edit_is_within_sight : withinSight = true :=
  rfl

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

theorem the_venue_edits_the_floor_and_never_sees_the_list :
    edits .venue .floorPlan = true ∧ sees .venue .guestList = false :=
  by decide

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

theorem a_vendor_sees_the_floor_and_edits_nothing_there :
    sees .vendor .floorPlan = true ∧ edits .vendor .floorPlan = false :=
  by decide

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

theorem the_couple_is_never_in_the_vendor_room (roster : List Member) (m : Member) (hc : m.role = .couple) :
    ¬ m ∈ vendorRoomMembers roster := fun h => by
  have hp : vendorSide m = true := filter_holds roster h
  have hf : vendorSide m = false := by
    cases m with
    | mk u r k l a p =>
        cases r with
        | couple => rfl
        | planner => exact nomatch hc
        | vendor => exact nomatch hc
        | venue => exact nomatch hc
        | party => exact nomatch hc
  exact nomatch (hf.symm.trans hp)

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

theorem the_wedding_party_is_never_in_the_vendor_room (roster : List Member) (m : Member) (hc : m.role = .party) :
    ¬ m ∈ vendorRoomMembers roster := fun h => by
  have hp : vendorSide m = true := filter_holds roster h
  have hf : vendorSide m = false := by
    cases m with
    | mk u r k l a p =>
        cases r with
        | couple => exact nomatch hc
        | planner => exact nomatch hc
        | vendor => exact nomatch hc
        | venue => exact nomatch hc
        | party => rfl
  exact nomatch (hf.symm.trans hp)

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

theorem a_vendor_is_in_the_vendor_room (roster : List Member) (m : Member) (hm : m ∈ roster) (hv : m.role = .vendor) :
    m ∈ vendorRoomMembers roster :=
  mem_filter_intro roster hm (by
    cases m with
    | mk u r k l a p =>
        cases r with
        | couple => exact nomatch hv
        | planner => exact nomatch hv
        | vendor => rfl
        | venue => exact nomatch hv
        | party => exact nomatch hv)

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

theorem the_vendor_room_is_derived_from_the_roster (roster : List Member) :
    vendorRoomAudience roster = channelAudience roster vendorSide :=
  rfl

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

theorem an_audience_is_members (roster : List Member) (p : Member → Bool) (u : Nat)
    (h : u ∈ channelAudience roster p) : ∃ m, m ∈ roster ∧ m.user = u := by
  obtain ⟨m, hm, he⟩ := mem_map_back (roster.filter p) h
  exact ⟨m, mem_of_mem_filter roster hm, he⟩

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

theorem the_owner_may_close (m : Member) (t : Task) (h : Nat.beq m.user t.owner = true) : mayClose m t = true :=
  by (intros; (try dsimp only [Role, mayClose, Task, Member] at *); intros; (rw [h]; rfl))

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

theorem the_couple_may_close (m : Member) (t : Task) (h : m.role = .couple) : mayClose m t = true :=
  by (intros; (try dsimp only [Role, mayClose, Task, Member] at *); intros; (rw [h]; (apply Room.or_swallows <;> fail)))

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

theorem a_vendor_may_not_close_anothers (m : Member) (t : Task) (h1 : Nat.beq m.user t.owner = false)
    (h2 : m.role = .vendor) : mayClose m t = false := by
  show (Nat.beq m.user t.owner || (Role.beq m.role .couple || Role.beq m.role .planner)) = false
  rw [h1, h2]
  exact rfl

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

theorem anyone_may_open_a_task (m : Member) : mayOpen m = true :=
  rfl

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

theorem the_day_of_sheet_is_everyones_to_edit : dayOfIsEveryones = true :=
  rfl

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

theorem every_edit_is_kept (w : List DayOfEdit) : behavior dayOfLog w = w :=
  by (intros; (apply Face.the_ledger_parks_the_word <;> fail))

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

theorem the_last_edit_undoes (e : Nat) : ∀ w : List Nat, undo (w ++ [e]) = w
  | [] => rfl
  | [_] => rfl
  | x :: y :: w => congrArg (x :: ·) (the_last_edit_undoes e (y :: w))

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

theorem the_venue_reads_counts_not_names (t : Table) (occ occ' : List Nat) (h : occ.length = occ'.length) :
    venueTable { t with occupants := occ } = venueTable { t with occupants := occ' } := by
  show (t.shape, occ.length) = (t.shape, occ'.length)
  rw [h]

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

theorem a_season_reads_each_room_as_the_vendor (rs : List Room) (v : Nat) :
    seasonView rs v = rs.map (fun r => (vendorFace v).obs r .mine) :=
  rfl

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

theorem the_seasons_sum_is_over_my_own_invoices (rs : List Room) (v : Nat) :
    seasonOwed rs v = (joinMap (fun r => (vendorFace v).obs r .mine) rs).sum :=
  rfl

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

theorem a_confirmation_touches_only_its_channel (r : Room) (m : Nat) :
    differOnly roomFace (confirmIn r 0 m) r .confirmed := fun q hq => by
  cases q with
  | vendorRoom =>
      show joinMap (fun q => q.confirmed) ((r.requests.map (fun q => cond (Nat.beq q.channel 0) (confirm q m) q)).filter (fun q => Nat.beq q.channel 1))
        = joinMap (fun q => q.confirmed) (r.requests.filter (fun q => Nat.beq q.channel 1))
      rw [a_confirmation_elsewhere_leaves_a_channel 0 1 m rfl r.requests]
  | confirmed => exact absurd rfl hq
  | guests => rfl
  | sheet => rfl
  | ledger => rfl
  | timeline => rfl
  | bach => rfl

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

theorem a_vendor_room_confirmation_touches_only_the_vendor_room (r : Room) (m : Nat) :
    differOnly roomFace (confirmIn r 1 m) r .vendorRoom := fun q hq => by
  cases q with
  | confirmed =>
      show joinMap (fun q => q.confirmed) ((r.requests.map (fun q => cond (Nat.beq q.channel 1) (confirm q m) q)).filter (fun q => Nat.beq q.channel 0))
        = joinMap (fun q => q.confirmed) (r.requests.filter (fun q => Nat.beq q.channel 0))
      rw [a_confirmation_elsewhere_leaves_a_channel 1 0 m rfl r.requests]
  | vendorRoom => exact absurd rfl hq
  | guests => rfl
  | sheet => rfl
  | ledger => rfl
  | timeline => rfl
  | bach => rfl

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

theorem a_quiet_seat_does_not_hear_it (s : List Ask) (p : Ask) (h : enrolled Ask.beq s p = false) :
    ¬ hears roomFace s p :=
  by
    (intros;
      (apply Room.the_unenrolled_are_no_member <;>
          first
          | (apply an_ask_reads_itself <;> fail)
          | assumption))

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

theorem the_bach_wall (r : Room) (b : List Nat) (hb : b ≠ r.bach) :
    reads roomFace coupleSeat (withBach r b) = reads roomFace coupleSeat r
      ∧ reads roomFace bestManSeat (withBach r b) ≠ reads roomFace bestManSeat r :=
  by (intros; (repeat' constructor); all_goals (intros; (apply the_bach_parts_the_best_man <;> assumption)))

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

theorem no_couple_side_seat_hears_the_vendor_room : ¬ hears roomFace (earshot roomFace coupleSideSeats) .vendorRoom :=
  by (intros; (apply a_quiet_seat_does_not_hear_it <;> rfl))

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

theorem the_vendor_room_holds_its_own_receipt (r : Room) (m : Nat) :
    reads roomFace coupleSeat (confirmIn r 1 m) = reads roomFace coupleSeat r
      ∧ reads roomFace lindaSeat (confirmIn r 1 m) = reads roomFace lindaSeat r
      ∧ reads roomFace bestManSeat (confirmIn r 1 m) = reads roomFace bestManSeat r :=
  by
    (intros; (repeat' constructor);
      all_goals
        (intros;
          (apply Witness.a_wall_hides_the_probe <;>
              first
              | (apply a_vendor_room_confirmation_touches_only_the_vendor_room <;> fail)
              | (apply a_quiet_seat_does_not_hear_it <;> rfl))))

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

theorem the_couple_side_witnesses_no_vendor_room_license (r : Room) (m : Nat) :
    witnessed roomFace coupleSideSeats (confirmIn r 1 m) r := fun s hs =>
  a_wall_hides_the_probe roomFace (a_vendor_room_confirmation_touches_only_the_vendor_room r m) s
    (fun hp => no_couple_side_seat_hears_the_vendor_room (mem_joinMap_intro hs hp))

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

theorem everyone_is_here (r : Room) (h : allClear r)
    {p : Party} (hp : p ∈ r.guests) (hr : p.rsvp = true) {m : Nat} (hm : m ∈ p.meals)
    (x : Nat) {gl gl' : List Party} (hperm : gl.Perm gl') :
    m ∈ r.delivered
      ∧ (∀ q, q ∈ r.requests → settled q = true)
      ∧ (sheet r.guests).length = heads r.guests
      ∧ heads gl = heads gl'
      ∧ witnessed roomFace coupleSideSeats (confirmIn r 1 x) r
      ∧ reads roomFace coupleSeat (confirmIn r 1 x) = reads roomFace coupleSeat r :=
  by
    (intros; (repeat' constructor);
      all_goals
        (intros;
          first
          | (apply everyone_clear_means_rose_ate <;> assumption)
          | (apply everyone_clear_means_every_request_settled <;> assumption)
          | (apply Roster.the_sheet_counts_the_heads <;> fail)
          | (apply Roster.reseating_keeps_the_heads <;> assumption)
          | (apply the_couple_side_witnesses_no_vendor_room_license <;> fail)
          | (apply ((the_vendor_room_holds_its_own_receipt _ _)).1 <;> fail)))

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

end Eih.Treaty

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/eih.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 TYPE page AS ENUM ('floorPlan', 'guestList', 'samePage', 'invoices', 'budget', 'guests', 'site', 'team', 'dayOf', 'tasks');
CREATE TYPE ask AS ENUM ('guests', 'sheet', 'ledger', 'timeline', 'bach', 'confirmed', 'vendorRoom');
CREATE TYPE vendor_ask AS ENUM ('timeline', 'mine');
CREATE TYPE role AS ENUM ('couple', 'planner', 'vendor', 'venue', 'party');
CREATE TYPE thing AS ENUM ('wedding', 'season');

CREATE TABLE member (
  id serial PRIMARY KEY,
  user_ integer NOT NULL,
  role role NOT NULL,
  kind integer NOT NULL,
  day_lane boolean NOT NULL,
  arrival integer NOT NULL,
  phone integer NOT NULL
);

CREATE TABLE request (
  id serial PRIMARY KEY,
  channel integer NOT NULL,
  audience integer[] NOT NULL,
  sender integer NOT NULL,
  confirmed integer[] NOT NULL
);

CREATE TABLE party (
  id serial PRIMARY KEY,
  name integer NOT NULL,
  rsvp boolean NOT NULL,
  meals integer[] NOT NULL
);

CREATE TABLE day_of_edit (
  id serial PRIMARY KEY,
  who integer NOT NULL,
  row integer NOT NULL,
  before integer NOT NULL,
  after integer NOT NULL
);

CREATE TABLE channel (
  id serial PRIMARY KEY,
  audience integer[] NOT NULL
);

CREATE TABLE task (
  id serial PRIMARY KEY,
  owner integer NOT NULL,
  assignee integer NOT NULL,
  done boolean NOT NULL
);

CREATE TABLE file (
  id serial PRIMARY KEY,
  channel integer NOT NULL REFERENCES channel(id)
);

CREATE TABLE bill (
  id serial PRIMARY KEY,
  thing thing NOT NULL,
  payer role NOT NULL
);

CREATE TABLE table_ (
  id serial PRIMARY KEY,
  shape integer NOT NULL,
  occupants integer[] NOT NULL
);

CREATE TABLE room (
  id serial PRIMARY KEY,
  delivered integer[] NOT NULL,
  timeline integer[] NOT NULL,
  bach integer[] NOT NULL
);
CREATE TABLE room_guests (
  room_id integer NOT NULL REFERENCES room(id),
  position integer NOT NULL,
  party_id integer NOT NULL REFERENCES party(id)
);
CREATE TABLE room_ledger (
  room_id integer NOT NULL REFERENCES room(id),
  position integer NOT NULL,
  c0 integer NOT NULL,
  c1 integer NOT NULL,
  c2 integer NOT NULL
);
CREATE TABLE room_requests (
  room_id integer NOT NULL REFERENCES room(id),
  position integer NOT NULL,
  request_id integer NOT NULL REFERENCES request(id)
);

-- makerFace: a face over room — each probe a column
CREATE FUNCTION room_as_maker_face(room_id integer) RETURNS TABLE(unit integer) LANGUAGE sql STABLE AS $$
  SELECT cardinality((SELECT array_agg(party_id ORDER BY position) FROM room_guests c WHERE c.room_id = room.id)) FROM room WHERE id = $1 $$;

-- roomFace: a face over room — each probe a column
CREATE FUNCTION room_as_room_face(room_id integer) RETURNS TABLE(guests integer[], sheet integer[], ledger integer[], timeline integer[], bach integer[], confirmed integer[], vendor_room integer[]) LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT (SELECT name FROM party WHERE id = x) FROM unnest((SELECT array_agg(party_id ORDER BY position) FROM room_guests c WHERE c.room_id = room.id)) WITH ORDINALITY AS u(x, o) ORDER BY o), room.delivered, ARRAY(SELECT (x).c2 FROM unnest((SELECT array_agg(c ORDER BY position) FROM room_ledger c WHERE c.room_id = room.id)) AS x ORDER BY (x).position), room.timeline, room.bach, ARRAY(SELECT m FROM unnest(ARRAY(SELECT x FROM unnest((SELECT array_agg(request_id ORDER BY position) FROM room_requests c WHERE c.room_id = room.id)) WITH ORDINALITY AS u(x, o) WHERE ((SELECT channel FROM request WHERE id = x) = 0) ORDER BY o)) WITH ORDINALITY AS u(x, o), unnest((SELECT confirmed FROM request WHERE id = x)) WITH ORDINALITY AS v(m, i) ORDER BY o, i), ARRAY(SELECT m FROM unnest(ARRAY(SELECT x FROM unnest((SELECT array_agg(request_id ORDER BY position) FROM room_requests c WHERE c.room_id = room.id)) WITH ORDINALITY AS u(x, o) WHERE ((SELECT channel FROM request WHERE id = x) = 1) ORDER BY o)) WITH ORDINALITY AS u(x, o), unnest((SELECT confirmed FROM request WHERE id = x)) WITH ORDINALITY AS v(m, i) ORDER BY o, i) FROM room WHERE id = $1 $$;

-- vendorFace: a face over room, parameterized (1) — each probe a column
CREATE FUNCTION room_as_vendor_face(room_id integer, p1 integer) RETURNS TABLE(timeline integer[], mine integer[]) LANGUAGE sql STABLE AS $$
  SELECT room.timeline, ARRAY(SELECT (x).c2 FROM unnest(ARRAY(SELECT x FROM unnest((SELECT array_agg(c ORDER BY position) FROM room_ledger c WHERE c.room_id = room.id)) AS x WHERE ((x).c0 = $2) ORDER BY (x).position)) AS x ORDER BY (x).position) FROM room WHERE id = $1 $$;

-- joinsFree: a rule over role, derived, never stored
CREATE FUNCTION joins_free(role) RETURNS boolean LANGUAGE sql IMMUTABLE AS $$
  SELECT CASE $1 WHEN 'couple' THEN true WHEN 'planner' THEN true WHEN 'vendor' THEN true WHEN 'venue' THEN true WHEN 'party' THEN true END $$;

-- edited: a rule over role, derived, never stored
CREATE FUNCTION edited(role) RETURNS page[] LANGUAGE sql IMMUTABLE AS $$
  SELECT CASE $1 WHEN 'couple' THEN ARRAY['floorPlan', 'guestList', 'samePage', 'invoices', 'budget', 'guests', 'site', 'team', 'dayOf', 'tasks']::page[] WHEN 'planner' THEN ARRAY['floorPlan', 'guestList', 'invoices', 'team', 'dayOf', 'tasks']::page[] WHEN 'vendor' THEN ARRAY['invoices', 'dayOf', 'tasks']::page[] WHEN 'venue' THEN ARRAY['floorPlan', 'invoices', 'dayOf', 'tasks']::page[] WHEN 'party' THEN ARRAY['floorPlan', 'guestList', 'dayOf', 'tasks']::page[] END $$;

-- seen: a rule over role, derived, never stored
CREATE FUNCTION seen(role) RETURNS page[] LANGUAGE sql IMMUTABLE AS $$
  SELECT CASE $1 WHEN 'couple' THEN ARRAY['floorPlan', 'guestList', 'samePage', 'invoices', 'budget', 'guests', 'site', 'team', 'dayOf', 'tasks']::page[] WHEN 'planner' THEN ARRAY['floorPlan', 'guestList', 'samePage', 'invoices', 'team', 'dayOf', 'tasks']::page[] WHEN 'vendor' THEN ARRAY['floorPlan', 'samePage', 'invoices', 'team', 'dayOf', 'tasks']::page[] WHEN 'venue' THEN ARRAY['floorPlan', 'samePage', 'invoices', 'team', 'dayOf', 'tasks']::page[] WHEN 'party' THEN ARRAY['floorPlan', 'guestList', 'samePage', 'team', 'dayOf', 'tasks']::page[] END $$;

-- pays: a rule over role, derived, never stored
CREATE FUNCTION pays(role) RETURNS boolean LANGUAGE sql IMMUTABLE AS $$
  SELECT CASE $1 WHEN 'couple' THEN true WHEN 'planner' THEN true WHEN 'vendor' THEN true WHEN 'venue' THEN true WHEN 'party' THEN false END $$;

-- owner: a rule over thing, derived, never stored
CREATE FUNCTION owner(thing) RETURNS role LANGUAGE sql IMMUTABLE AS $$
  SELECT (CASE $1 WHEN 'wedding' THEN 'couple' WHEN 'season' THEN 'vendor' END)::role $$;

-- vendorRoomRequestOf: derived, not yet drawn (data over List Eih.Treaty.Member)

-- heardBy: derived, never stored
-- described by outside_the_audience_hears_no_receipt, the_audience_hears_the_receipt_by_name
CREATE FUNCTION heard_by(request_id integer, arg2 integer) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT (CASE WHEN (arg2 = ANY(SELECT unnest(request.audience))) THEN request.confirmed ELSE ARRAY[]::integer[] END) FROM request WHERE id = $1 $$;

-- channelAudience: derived, not yet drawn (data over List Eih.Treaty.Member)

-- inChannel: derived, never stored
CREATE FUNCTION in_channel(request_ids integer[], arg2 integer) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT m FROM unnest(ARRAY(SELECT x FROM unnest($1) WITH ORDINALITY AS u(x, o) WHERE ((SELECT channel FROM request WHERE id = x) = arg2) ORDER BY o)) WITH ORDINALITY AS u(x, o), unnest((SELECT confirmed FROM request WHERE id = x)) WITH ORDINALITY AS v(m, i) ORDER BY o, i) $$;

-- asked: derived, never stored
-- described by the_sender_is_never_asked
CREATE FUNCTION asked(request_id integer) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT x FROM unnest(request.audience) WITH ORDINALITY AS u(x, o) WHERE (NOT (x = request.sender)) ORDER BY o) FROM request WHERE id = $1 $$;

-- readRoom: derived, not yet drawn (data over Eih.Treaty.Room)

-- seasonView: derived, not yet drawn (a list of lists — the shadow holds no jagged array)

-- venue_chart: derived, not yet drawn (calls venue_table, beyond the fragment)

-- venueTable: derived, not yet drawn (data over Eih.Treaty.Table)

-- sheet: derived, never stored
-- described by everyone_is_here, the_caterer_reads_the_delivery, the_delivery_is_the_sheet
CREATE FUNCTION sheet(party_ids integer[]) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT (SELECT array_agg(m ORDER BY g.position) FROM unnest($1) WITH ORDINALITY AS g(elem_id, position) JOIN party p ON p.id = g.elem_id, unnest(p.meals) m WHERE p.rsvp) $$;

-- visible: a check, derived, never stored
-- described by a_file_is_never_wider_than_its_channel, a_vendor_room_file_is_absent_from_the_couples_files
CREATE FUNCTION visible(file_id integer, arg2 integer) RETURNS boolean LANGUAGE sql STABLE AS $$
  SELECT (arg2 = ANY(SELECT unnest((SELECT audience FROM channel WHERE id = file.channel)))) FROM file WHERE id = $1 $$;

-- canSee: a check, derived, never stored
-- described by a_vendor_room_file_is_absent_from_the_couples_files
CREATE FUNCTION can_see(file_id integer, arg2 integer) RETURNS boolean LANGUAGE sql STABLE AS $$
  SELECT (arg2 = ANY(SELECT unnest((SELECT audience FROM channel WHERE id = file.channel)))) FROM file WHERE id = $1 $$;

-- mayClose: a check, derived, never stored
-- described by a_vendor_may_not_close_anothers, the_couple_may_close, the_owner_may_close
CREATE FUNCTION may_close(member_id integer, arg2 integer) RETURNS boolean LANGUAGE sql STABLE AS $$
  SELECT ((member.user_ = (SELECT owner FROM task WHERE id = arg2)) OR ((member.role = 'couple') OR (member.role = 'planner'))) FROM member WHERE id = $1 $$;

-- vendorSide: a check, derived, never stored
-- described by the_vendor_room_is_derived_from_the_roster
CREATE FUNCTION vendor_side(member_id integer) RETURNS boolean LANGUAGE sql STABLE AS $$
  SELECT ((member.role = 'vendor') OR ((member.role = 'venue') OR (member.role = 'planner'))) FROM member WHERE id = $1 $$;

-- mayOpen: a check, derived, never stored
-- described by anyone_may_open_a_task
CREATE FUNCTION may_open(member_id integer) RETURNS boolean LANGUAGE sql STABLE AS $$
  SELECT true FROM member WHERE id = $1 $$;

-- withBach: a clerk — never a second copy of the row, an update to it
-- described by the_bach_parts_the_best_man, the_bach_touches_only_the_bach, the_bach_wall
CREATE FUNCTION with_bach(room_id integer, arg2 integer[]) RETURNS void LANGUAGE sql AS $$
  UPDATE room SET bach = arg2 WHERE id = $1 $$;

-- ask: a clerk over a has-many field (requests) — not yet drawn

-- withLine: a clerk over the has-many ledger — a prepend: shift the child rows, insert at zero
-- described by a_line_touches_only_the_ledger, a_vendor_never_sees_anothers_invoice, linda_never_sees_the_ledger, the_caterer_never_sees_the_ledger
CREATE FUNCTION with_line(room_id integer, arg2 integer[]) RETURNS void LANGUAGE sql AS $$
  UPDATE room_ledger SET position = position + 1 WHERE room_id = $1;
  INSERT INTO room_ledger (room_id, position, c0, c1, c2) VALUES ($1, 0, $2[1], $2[2], $2[3]) $$;

-- confirm: a clerk — never a second copy of the row, an update to it
-- described by a_confirmation_elsewhere_leaves_a_channel, outside_the_audience_hears_no_receipt
CREATE FUNCTION confirm(request_id integer, arg2 integer) RETURNS void LANGUAGE sql AS $$
  UPDATE request SET confirmed = array_prepend(arg2, request.confirmed) WHERE id = $1 $$;

-- close: a clerk — never a second copy of the row, an update to it
CREATE FUNCTION close(task_id integer) RETURNS void LANGUAGE sql AS $$
  UPDATE task SET done = true WHERE id = $1 $$;

-- withGuests: a clerk over the has-many guests — a replacement: delete, then insert in order
-- described by the_caterer_never_sees_the_guests, the_guests_touch_only_the_guests, the_maker_sees_shape_not_content
CREATE FUNCTION with_guests(room_id integer, arg2 integer[]) RETURNS void LANGUAGE sql AS $$
  DELETE FROM room_guests WHERE room_id = $1;
  INSERT INTO room_guests (room_id, position, party_id) SELECT $1, ordinality - 1, id FROM unnest($2) WITH ORDINALITY AS u(id, ordinality) $$;

-- assign: a clerk — never a second copy of the row, an update to it
CREATE FUNCTION assign(task_id integer, arg2 integer) RETURNS void LANGUAGE sql AS $$
  UPDATE task SET assignee = arg2 WHERE id = $1 $$;

-- edits: a rule over role, derived, never stored
CREATE FUNCTION edits(role, page) RETURNS boolean LANGUAGE sql IMMUTABLE AS $$
  SELECT ($2 = ANY(SELECT unnest(edited($1)))) $$;

-- sees: a rule over role, derived, never stored
CREATE FUNCTION sees(role, page) RETURNS boolean LANGUAGE sql IMMUTABLE AS $$
  SELECT ($2 = ANY(SELECT unnest(seen($1)))) $$;

-- seasonOwed: derived, never stored
-- described by the_seasons_sum_is_over_my_own_invoices
CREATE FUNCTION season_owed(room_ids integer[], arg2 integer) RETURNS integer LANGUAGE sql STABLE AS $$
  SELECT (SELECT coalesce(sum(x), 0) FROM unnest(ARRAY(SELECT m FROM unnest($1) WITH ORDINALITY AS u(x, o), unnest((SELECT mine FROM room_as_vendor_face(x, arg2))) WITH ORDINALITY AS v(m, i) ORDER BY o, i)) AS x) $$;

-- vendorRoomMembers: derived, never stored
-- described by a_vendor_is_in_the_vendor_room, the_couple_is_never_in_the_vendor_room, the_wedding_party_is_never_in_the_vendor_room
CREATE FUNCTION vendor_room_members(member_ids integer[]) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT x FROM unnest($1) WITH ORDINALITY AS u(x, o) WHERE vendor_side(x) ORDER BY o) $$;

-- tally: derived, never stored
-- described by the_same_page_hears_its_own_earshot
CREATE FUNCTION tally(request_id integer) RETURNS integer LANGUAGE sql STABLE AS $$
  SELECT cardinality(ARRAY(SELECT x FROM unnest(request.confirmed) WITH ORDINALITY AS u(x, o) WHERE (x = ANY(SELECT unnest(asked(request.id)))) ORDER BY o)) FROM request WHERE id = $1 $$;

-- heads: derived, never stored
-- described by (drawn by the_sheet_counts_the_heads), everyone_is_here
CREATE FUNCTION heads(party_ids integer[]) RETURNS integer LANGUAGE sql STABLE AS $$
  SELECT cardinality(sheet($1)) $$;

-- lawful: a check, derived, never stored
-- described by the_payer_is_the_owner_or_the_host
CREATE FUNCTION lawful(bill_id integer) RETURNS boolean LANGUAGE sql STABLE AS $$
  SELECT ((bill.payer = owner(bill.thing)) OR ((bill.payer = 'vendor') AND (owner(bill.thing) = 'couple'))) FROM bill WHERE id = $1 $$;

-- settled: a check, derived, never stored
-- described by everyone_clear_means_every_request_settled, everyone_is_here
CREATE FUNCTION settled(request_id integer) RETURNS boolean LANGUAGE sql STABLE AS $$
  SELECT (asked(request.id) <@ request.confirmed) FROM request WHERE id = $1 $$;

-- deliver: a clerk — never a second copy of the row, an update to it
-- described by the_caterer_reads_the_delivery, the_delivery_is_the_sheet, the_delivery_moves_no_guest
CREATE FUNCTION deliver(room_id integer) RETURNS void LANGUAGE sql AS $$
  UPDATE room SET delivered = sheet((SELECT array_agg(party_id ORDER BY position) FROM room_guests c WHERE c.room_id = room.id)) WHERE id = $1 $$;

-- confirmIn: a clerk over the has-many requests — the element's clerk confirm run on each child the condition selects
-- described by a_confirmation_parts_the_audience, a_confirmation_touches_only_its_channel, a_vendor_room_confirmation_touches_only_the_vendor_room, everyone_is_here, the_couple_side_witnesses_no_vendor_room_license, the_vendor_room_holds_its_own_receipt
CREATE FUNCTION confirm_in(room_id integer, arg2 integer, arg3 integer) RETURNS void LANGUAGE sql AS $$
  SELECT confirm(c.request_id, arg3) FROM room_requests c WHERE c.room_id = $1 AND ((SELECT channel FROM request WHERE id = c.request_id) = arg2) $$;

-- samePage: derived, never stored
-- described by the_same_page_counts_only_within_earshot, the_same_page_hears_its_own_earshot
CREATE FUNCTION same_page(request_ids integer[], arg2 integer) RETURNS integer LANGUAGE sql STABLE AS $$
  SELECT (SELECT coalesce(sum(x), 0) FROM unnest(ARRAY(SELECT tally(x) FROM unnest(ARRAY(SELECT x FROM unnest($1) WITH ORDINALITY AS u(x, o) WHERE (arg2 = ANY(SELECT unnest((SELECT audience FROM request WHERE id = x)))) ORDER BY o)) WITH ORDINALITY AS u(x, o) ORDER BY o)) AS x) $$;

-- unanswered: derived, never stored
CREATE FUNCTION unanswered(request_ids integer[]) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT x FROM unnest($1) WITH ORDINALITY AS u(x, o) WHERE (NOT settled(x)) ORDER BY o) $$;

-- vendorRoomAudience: derived, never stored
-- described by the_vendor_room_is_derived_from_the_roster
CREATE FUNCTION vendor_room_audience(member_ids integer[]) RETURNS integer[] LANGUAGE sql STABLE AS $$
  SELECT ARRAY(SELECT (SELECT user_ FROM member WHERE id = x) FROM unnest(vendor_room_members($1)) WITH ORDINALITY AS u(x, o) ORDER BY o) $$;

-- memberSees: a check, derived, never stored
-- described by an_edit_is_within_the_lane, lanes_shrink_never_lock, the_day_lane_keeps_the_day_of_sheet, the_day_lane_sees_no_task_list
CREATE FUNCTION member_sees(member_id integer, arg2 page) RETURNS boolean LANGUAGE sql STABLE AS $$
  SELECT (sees(member.role, arg2) AND (NOT (member.day_lane AND (arg2 = 'tasks')))) FROM member WHERE id = $1 $$;

-- allClear: a check, derived, never stored
-- described by everyone_clear_means_every_request_settled, everyone_clear_means_rose_ate, everyone_is_here
CREATE FUNCTION all_clear(room_id integer) RETURNS boolean LANGUAGE sql STABLE AS $$
  SELECT ((room.delivered = sheet((SELECT array_agg(party_id ORDER BY position) FROM room_guests c WHERE c.room_id = room.id))) AND (unanswered((SELECT array_agg(request_id ORDER BY position) FROM room_requests c WHERE c.room_id = room.id)) = ARRAY[]::integer[])) FROM room WHERE id = $1 $$;

-- memberEdits: a check, derived, never stored
-- described by an_edit_is_within_the_lane
CREATE FUNCTION member_edits(member_id integer, arg2 page) RETURNS boolean LANGUAGE sql STABLE AS $$
  SELECT (edits(member.role, arg2) AND member_sees(member.id, arg2)) FROM member WHERE id = $1 $$;

-- catererSeat: hears timeline, sheet, confirmed, vendorRoom
-- licensed by the_caterer_never_sees_the_guests, the_caterer_never_sees_the_ledger
CREATE VIEW room_as_caterer_seat AS SELECT room.id, f.timeline, f.sheet, f.confirmed, f.vendor_room FROM room, LATERAL room_as_room_face(room.id) f;

-- roomSeat: hears guests, sheet, ledger, timeline, bach, confirmed, vendorRoom
-- licensed by the_room_covers_itself, the_room_witnesses_the_license
CREATE VIEW room_as_room_seat AS SELECT room.id, f.guests, f.sheet, f.ledger, f.timeline, f.bach, f.confirmed, f.vendor_room FROM room, LATERAL room_as_room_face(room.id) f;

-- lindaSeat: hears guests, timeline, confirmed
-- licensed by everyone_is_here, linda_never_sees_the_ledger, the_vendor_room_holds_its_own_receipt
CREATE VIEW room_as_linda_seat AS SELECT room.id, f.guests, f.timeline, f.confirmed FROM room, LATERAL room_as_room_face(room.id) f;

-- coupleSeat: hears guests, sheet, ledger, timeline, confirmed
-- licensed by a_confirmation_parts_the_audience, everyone_is_here, the_bach_wall, the_vendor_room_holds_its_own_receipt
CREATE VIEW room_as_couple_seat AS SELECT room.id, f.guests, f.sheet, f.ledger, f.timeline, f.confirmed FROM room, LATERAL room_as_room_face(room.id) f;

-- pages: hears floorPlan, guestList, samePage, invoices, budget, guests, site, team, dayOf, tasks
CREATE VIEW member_as_pages AS SELECT id, role AS floor_plan, role AS guest_list, role AS same_page, role AS invoices, role AS budget, role AS guests, role AS site, role AS team, role AS day_of, role AS tasks FROM member;

-- bestManSeat: hears timeline, bach, confirmed
-- licensed by everyone_is_here, the_bach_parts_the_best_man, the_bach_wall, the_vendor_room_holds_its_own_receipt
CREATE VIEW room_as_best_man_seat AS SELECT room.id, f.timeline, f.bach, f.confirmed FROM room, LATERAL room_as_room_face(room.id) f;

eih — a product as an assay, grown from assays/eih.lean

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)

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)