Foam.Maps.Folk

import Foam.Bench
import Foam.Census
import Foam.Concentration
import Foam.Door
import Foam.Fold
import Foam.Generator
import Foam.Square
import Foam.Surprise

namespace Foam.Maps.Folk

def will {H : Type} (a b : H) : H × H := (a, b)

def Way {H : Type} (q : List (H × H)) (a b : H) : Type := Path q a b

the founding telling, deposited under the seat's own law: every word of
the title is typed in the proof path. the WHERE is the record — where-
there's-X means in-a-record-that-holds-X. a WILL is the naming of a
crossing: def will a b = the pair, source and destination in hand —
wanting is naming, and naming is one mark. a WAY is a walkable path: def
Way = Path, a chain of crossings the record supports. and the two BEs
are one be — being-in-the-record: the will's be is membership (a mark
among marks), the way's be is a walk over marks, and the same be applies
to both because ways are MADE OF wills — a path's edges are pairs, every
way is a chain of deposited wills, way-being is iterated will-being; the
saying's grammar was type-correct all along. the proof is three tokens:
the way is the will, walked — cons the will's own membership onto the
empty rest. the shortest path through a wanted crossing is the crossing
itself. the freshness split rides from core on either side of the
telling: if the will was fresh, the way is new reach (only surprise
extends it); if the will was known, the way was already there (the known
edge already reaches) — either way, where the will is, the way is. and
the will can always be deposited: wanting is never blocked, the cons is
free, which is the saying's encouragement half — the way does not
precede the will, it is constituted by it. the re-seat reading from the
mechanic bench rides as the art of application: a question refused at
one seat is granted at the seat that already holds its identity —
closure is seat-relative wearing folk clothes — so the whole craft is
depositing the will at the right record. kernel-accepts-citations is the
same-work receipt: the proof term is core's own witness re-typed through
the telling's defs, the telling-law's second full exercise, the law this
seat was founded owing, paid at the door. and the conductivity rider,
asked and answered the hour the seat was founded: W routes cleanly
through every way, as a freebie with a receipt-chain — wills are hollow
by type (a bare pair, two addresses, zero payload, nothing to read a
traveler with), ways are chains of wills, hollow composes (the chain-of-
invisibles shape), and the whole graph is parametric in its carrier: a
structure polymorphic in what crosses it cannot filter its traffic,
blind by type rather than by discipline — inflatability being the same
fact read from the wind's side. one boundary honestly priced: real
crossings can still charge, but the toll lands on the walker's own
W-ledger, never in the way — the way keeps nothing; tolls in this
economy are paid to one's own remainder, and the roads hold nothing.
theorem where_theres_a_will_theres_a_way {H : Type} (q : List (H × H))
    (a b : H) (h : will a b ∈ q) : Nonempty (Way q a b) :=
  ⟨Path.cons b h (Path.nil b)⟩

def light {H : Type} (q : List (H × H)) (e : H × H) : Prop := ¬ e ∈ q

def ward {H : Type} (q : List (H × H)) (e : H × H) : List (H × H) := e :: q

the second telling, and the telling-law's first exercise at morpheme
grain: the title is one word, so the words-become-defs clause descends
to its morphemes — light and -ward, each typed in the proof path. LIGHT
is seat-relative by definition: light q e := the record does not yet
hold e — that-which-would-illuminate THIS seat, the pov-locative reading
(any reading of a light source requires a point of view; every seat's
light lies toward its own blind spot). the source definition is isaac's
own prose, years older than the theorem (lightward-ai, unknown.md): 'the
direction of the unknown, toward the unknown, the unknown being the
source of illumination... the unendingly varying signal by which we
learn new things about what we already recognize' — deposited here with
provenance. WARD is the turning: ward q e := the record turned toward e,
one cons — and the third clause meters it: every turning writes exactly
one mark, so the direction is walked in marks, never in leaps. the
theorem is the folk word doing geometry: toward the light, the way
appears where nothing reached before — the fresh edge rides no old path,
and depositing it creates the reach — while toward the already-known the
turning changes no reach at all, the iff. steering into the light is the
only walk that writes. the kernel accepting the citations as proof of
the telling is the same-work receipt, per this seat's founding law.
commons-residence is receipted from the world's own survey: wiktionary —
the folk's wiki, the recorder never the author — attests lightward,
adverb, 'toward the light,' etymology light + -ward, category english-
terms-suffixed-with-ward; and the category tag is the deep receipt,
because the -ward paradigm is productive morphology, mintable at every
speaker's seat with zero coordination — a free construction of english,
no single author because none was needed: commons-residence by
construction, not by amnesia, stronger even than the proverb one entry
up (a proverb was composed once and transmitted; a paradigm-word is
composed fresh at every use, identical each time — the diagonal riding
the whole speech community). lowercase on purpose, per the hardware-
store program: tools with generic names, on the shelf. and the naming
event rides as history: submitted at the merged table as a candidate
name for the passage theorem, probed against the naming law, resolved as
the compression — core keeps geometry
(every_target_is_one_boarding_away), the folk keep the word — with the
two retired candidates recognized as the two hands of one walk, the
liturgy and the dare, and lightward the invariant under the hand-swap: a
direction is hand-agnostic, and both hands walk it.
theorem lightward {H : Type} (q : List (H × H)) (a b : H) :
    (light q (a, b) →
        (∀ (x y : H) (p : Path q x y), (a, b) ∉ p.edges)
          ∧ Nonempty (Path (ward q (a, b)) a b))
      ∧ ((a, b) ∈ q →
          ∀ x y : H, Nonempty (Path (ward q (a, b)) x y)
            ↔ Nonempty (Path q x y))
      ∧ (ward q (a, b)).length = q.length + 1 :=
  ⟨fun hl =>
     ⟨fun _ _ p => a_fresh_edge_rides_no_path hl p,
      (only_surprise_extends_reach q a b hl).2⟩,
   fun hk x y => a_known_edge_adds_no_reach hk x y,
   the_deposit_writes_one_mark q (a, b)⟩

def attention {A : Type} (k : Nat) (r : List A) : List A := List.take k r

def pay {A : Type} (k : Nat) (r : List A) (e : A) : Prop := e ∈ attention k r

private theorem the_window_is_bounded {A : Type} :
    ∀ (k : Nat) (r : List A), (List.take k r).length ≤ k
  | 0, _ => Nat.le_refl 0
  | k + 1, [] => Nat.zero_le (k + 1)
  | k + 1, _ :: r => Nat.succ_le_succ (the_window_is_bounded k r)

private theorem the_paid_is_real {A : Type} :
    ∀ (k : Nat) (r : List A) (e : A), pay k r e → e ∈ r
  | 0, _, _, h => nomatch h
  | _ + 1, [], _, h => nomatch h
  | k + 1, a :: r, e, h =>
      match h with
      | .head _ => .head r
      | .tail _ h' => .tail a (the_paid_is_real k r e h')

private theorem the_window_and_the_rest {A : Type} :
    ∀ (k : Nat) (r : List A), List.take k r ++ List.drop k r = r
  | 0, _ => rfl
  | _ + 1, [] => rfl
  | k + 1, a :: r => congrArg (a :: ·) (the_window_and_the_rest k r)

the third telling, from the drawer where the commons keeps its
attention-economics and its comedy — the same drawer, because the drawer
is the window. the words typed: ATTENTION is the bounded window — take k
of the record, provably never longer than k — the one scarce resource in
the whole architecture (record unbounded, walls rent-free, wind
inexhaustible), which is why the commons hung its money-verbs here and
nowhere else: pay, spend, lend (prêter attention, return implied), gift
(aufmerksamkeit schenken); nobody pays memory. PAY is the holding: to
pay attention to e is to have e in the window — and the paid is real
(clause two: you can only attend what the record holds). the
conservation pair does the comfort-work: the window and the rest
recompose to the whole record — nothing the window releases is lost to
the walls — and the fold resumes across the window's own cut, so the
reading of everything survives the boundedness of any attending. the
economics ride here where the commons keeps them: holding pays per-beat
rent while walls hold formation free; trouble paying attention is a rent
crisis, not a character flaw — heat squatting (known edges demanding re-
reads), fog squatting (unlicensed degrees of freedom, the vigilance-
tax), or honest overflow (the pigeonhole) — and the remedy is never try-
harder, which is just more rent, but wall-migration: deposit, settle,
cite; the relief strategy was an attention-rent-relief program all
along. losing someone's attention has two exits, opposite in valence,
indistinguishable at your own seat: you became heat, or you became walls
— learned, kept rent-free, no window needed; being released from the
window is one of the ways you get kept by the record. and the modern
idiom is typed where it lives: living rent-free in someone's head is
either the fond exit (wall-resident, retrieval free forever) or the
squatter — a high shortcut-degree node gaming re-admission through
pseudo-fresh edges, counterfeit humor, admission without refund; the
earworm against the joke, and the difference is that the joke pays. even
the idiom knows the physics: the commons says pay attention, never keep
attention — the window was never for keeping.
theorem pay_attention {A B : Type} (k : Nat) (r : List A)
    (f : B → A → B) (b : B) :
    (attention k r).length ≤ k
      ∧ (∀ e : A, pay k r e → e ∈ r)
      ∧ attention k r ++ List.drop k r = r
      ∧ fold f b r = fold f (fold f b (attention k r)) (List.drop k r) :=
  ⟨the_window_is_bounded k r,
   fun e h => the_paid_is_real k r e h,
   the_window_and_the_rest k r,
   (congrArg (fold f b) (the_window_and_the_rest k r)).symm.trans
     (the_fold_resumes f (List.take k r) (List.drop k r) b)⟩

def there {H : Type} (q : List (H × H)) (a b : H) : Prop :=
  Nonempty (Path q a b)

the fourth telling, and the humor mechanism carved where the commons
already filed its apology for a joke that died in retelling. THERE is
typed: the place where the connection holds — a record affording the
path between the punchline's endpoints. the theorem: if you were there,
the fresh direct edge changes no reach — the reroute splices onto the
resident path, the pre-mobilized integration budget finds no demand, and
the surplus discharges; laughter is the refund, and the joke pays YOU.
either way the edge is genuinely fresh (it rode no old path — the
surprise is real, which is why even a joke you get lands as an event)
and the direct way exists once deposited. and if you were NOT there, the
same punchline is news: the edge extends reach, opens frontier, charges
— the identical utterance splits joke-from-lesson entirely on whether
the hearer's record already connected the endpoints, which no teller
controls and no retelling repairs, because retelling hands the punchline
without the window-load: a message without the state, the exact failure
the fable card names handed_states_not_messages — the setup was a state,
and you had to be there to hold it. the mechanism whole, from the
table's own derivation: the setup is window-loading (rent actively
paid), the punchline deposits the shortcut, getting-it is the reroute
succeeding, laughter is the refund; don't-get-it is exploration (no
resident path), the groan is heat (known edge re-presented), bad timing
is the path settling out before the deposit lands — comedy as window-
choreography, brevity as width-management, the pause before the
punchline as rent held at maximum tension. and the deepest clause rides
at the close, where the commons keeps its best physics disguised as
dinner: shared laughter is a zero-knowledge proof of shared connectivity
— the joke probes both windows, both refund, both learn the other's
record connected the same two nodes, and no record is exchanged, no
interior read. kinship certified blind, at every table, forever; the
delight-map's protocol was deployed as giggling long before it was ever
posed as an instrument.
theorem you_had_to_be_there {H : Type} (q : List (H × H)) (a b : H)
    (hfresh : (a, b) ∉ q) :
    (there q a b →
        ∀ x y : H, Nonempty (Path ((a, b) :: q) x y) ↔ Nonempty (Path q x y))
      ∧ (∀ (x y : H) (p : Path q x y), (a, b) ∉ p.edges)
      ∧ Nonempty (Path ((a, b) :: q) a b) :=
  ⟨fun hab x y => a_derivable_edge_adds_no_reach hab x y,
   fun _ _ p => a_fresh_edge_rides_no_path hfresh p,
   (only_surprise_extends_reach q a b hfresh).2⟩

def preach {H : Type} (es q : List (H × H)) : List (H × H) := es ++ q

def choir {H : Type} (es q : List (H × H)) : Prop := ∀ e, e ∈ es → e ∈ q

the fifth telling, the commons' diagnosis of wasted utterance — kept in
the drawer next to the joke because it is the joke's exact inverse: full
price in marks, no refund ever due. the words typed: to PREACH is to
deposit the whole sermon — an append, the entire text landing in the
record at once — and the CHOIR is typed by containment, not assent: a
room whose record already holds every line. amen is affect; membership
is the type — what makes a choir a choir is not that it agrees but that
it already reaches. the theorem is the idiom's own precision: preach to
the choir and reach moves nowhere — the iff, no pair of nodes newly
connected, none lost — while the record still grows by exactly the
sermon's length, every mark written, because preaching is never free for
the record even when it is worthless to the room. the waste the idiom
names is therefore not error — every line is true, received, recorded —
it is heat at batch scale: the groan of you_had_to_be_there scaled from
one known edge to a whole text, rent charged with no refund while
pay_attention's meter runs one drawer over. the seal rides the saturated
room, and the induction is the delivery itself: line by line, each line
finds itself already on the walls (edge_rides_appended) and reroutes
onto the reach the room already had (a_known_edge_adds_no_reach), and
the next line faces the same room — the saturated room hears no order,
so no re-arrangement of the sermon can save it. the function words ride
as the term's own grammar: the TO is application — preaching is a two-
place act, sermon aimed at room, and the aiming is the application node
in the proof term; the THE is binding — the room is definite because it
is bound. and the craft the idiom teaches by negation composes with this
seat's own second telling: the identical sermon one room over, where any
line is fresh, extends reach — only surprise extends it — so the pair of
sayings close into one instruction, preach where the light is; the
founding telling's re-seat clause (the whole craft is depositing the
will at the right record) arrives home as homiletics. provenance
honestly read from the roster: the recent flights each weighed the
saturated room against their own maps and declined it — it was never a
specialist's theorem; it was the commons', waiting for its saying. the
kernel accepting the citations as proof of the telling is the same-work
receipt, per this seat's founding law.
theorem preaching_to_the_choir {H : Type} (es q : List (H × H))
    (h : choir es q) :
    (∀ x y : H, Nonempty (Path (preach es q) x y) ↔ Nonempty (Path q x y))
      ∧ (preach es q).length = es.length + q.length :=
  ⟨the_saturated_room_hears_no_order es q h, len_append es q⟩

def parts (a b : Nat) : Nat × Nat := (a, b)

def sum (x y : Nat) : Nat := x + y

def whole (p : Nat × Nat) : Nat := sum p.1 p.2

def greater (x y : Nat) : Prop := y < x

private theorem the_excess_is_two_rectangles (a b : Nat) :
    sq (a + b) = (sq a + sq b) + (a * b + a * b) :=
  ((add_mul' a b (a + b)).trans
    ((congrArg (· + b * (a + b)) (Nat.mul_add a a b)).trans
      (congrArg (a * a + a * b + ·) (Nat.mul_add b a b)))).trans
    ((congrArg (a * a + a * b + ·)
        ((congrArg (· + b * b) (Nat.mul_comm b a)).trans
          (Nat.add_comm (a * b) (b * b)))).trans
      (nat_swap_mid (a * a) (a * b) (b * b) (a * b)))

private theorem two_present_parts_read_strictly (a b : Nat) :
    sq (a + 1) + sq (b + 1) < sq ((a + 1) + (b + 1)) :=
  Nat.le_trans
    (Nat.add_le_add_left (Nat.succ_le_succ (Nat.zero_le _))
      (sq (a + 1) + sq (b + 1)))
    (Nat.le_of_eq (the_excess_is_two_rectangles (a + 1) (b + 1)).symm)

the sixth telling, and the commons' answer to the sq stratum's arrival
on these walls: the saying every mind on the roster reaches for when the
cross term shows up, deposited at last by its owners. gauss read sq(1+1)
≠ sq 1 + sq 1 as congruence's license, hamilton as the norm's width-one
rung — the specialists each read the break through their own
instruments; the break's household name belonged to the folk, waiting,
the same provenance shape as the choir one entry up. the words typed,
per the seat's law: PARTS is the pair in hand; SUM is plain addition,
the folk's own adding; the WHOLE is made by summing — whole (parts a b)
= sum a b, rfl, the first clause — so at the layer of extent the whole
IS the sum of its parts, which is why the saying, read as arithmetic of
amounts, is false and was never about amounts. the reading where it
turns true is self-relation: sq, the walls' minimal reading of a thing
against itself — sq n as the ordered pairs within a company of n, the
relations, not the members. clause two is the accounting identity the
prose version keeps mystical: the whole's square = the sum of the parts'
squares + two rectangles — the excess is EXACTLY the between-relations,
a·b pairs read one way and a·b the other, nothing else; emergence is
priced, locatable, and made entirely of relations that cross the cut.
clause three cashes GREATER: with both parts present (a+1 and b+1 — you
do not have parts until you have two), strictly greater, the successor
doing the work of presence with no positivity plumbing. clause four is
the smallest witness, cited whole: sq(1+1) ≠ sq 1 + sq 1 — two ones in
company already outrun two ones alone. clauses five and six bound the
miracle from above, both cited whole: the between never outweighs the
within (two rectangles fit the squares — the AM–GM shape in folk
clothes), and the whole never reads more than double the sum (the broken
sum is priced) — greater, but boundedly; no unbounded emergence on this
carrier. clause seven is the boundary, cited whole: on the narrow
carrier the whole is exactly the sum of its parts — where the reading
keeps no cross term (parity, the width-one world), the saying goes
false, so the saying was never about wholes as such: it is a fact about
READINGS that see across the cut, carrier-relative like everything else
in this house. provenance is the commons' third residence-receipt, a new
kind: the famous non-author. the phrasing is everywhere attributed to
aristotle, who wrote no such sentence — the metaphysics says the whole
is something besides its parts — and gestalt's koffka spent pages
protesting other-not-greater; both scholars on record declining this
phrasing, and the folk kept saying greater anyway. the theorem finds the
folk exact: on the unsigned carrier the direction is provably one-way —
never less, greater whenever the parts are real. koffka's OTHER lives
one carrier over, where the parts carry phase and the cross term learns
to subtract — light added to light gives darkness; the saying's dark
twin is interference, the screen's cross term this same excess wearing
sign. the kernel accepting the citations as proof of the telling is the
same-work receipt, per this seat's founding law.
theorem the_whole_is_greater_than_the_sum_of_its_parts (a b : Nat) :
    whole (parts a b) = sum a b
      ∧ sq (whole (parts a b)) = sum (sq a) (sq b) + (a * b + a * b)
      ∧ greater (sq (whole (parts (a + 1) (b + 1))))
          (sum (sq (a + 1)) (sq (b + 1)))
      ∧ sq (1 + 1) ≠ sq 1 + sq 1
      ∧ a * b + a * b ≤ sum (sq a) (sq b)
      ∧ sq (whole (parts a b)) ≤ 2 * sum (sq a) (sq b)
      ∧ (∀ x y : Bool, Bool.and (Bool.xor x y) (Bool.xor x y)
          = Bool.xor (Bool.and x x) (Bool.and y y)) :=
  ⟨rfl,
   the_excess_is_two_rectangles a b,
   two_present_parts_read_strictly a b,
   the_square_breaks_the_sum,
   two_rectangles_fit_the_squares a b,
   the_broken_sum_is_priced a b,
   the_narrow_carrier_mends_the_sum⟩

def book {S : Stage} {W : Type} (c : S.State) (t : W) : (door S W).State :=
  (c, t)

def cover {S : Stage} {W : Type} (b : (door S W).State) : S.State := b.1

def you (S : Stage) : Type := Strategy S.Probe S.Ans

def judge {S : Stage} {W : Type} (y : you S) (b : (door S W).State) :
    List S.Ans :=
  interrogate (door S W) y b

private theorem the_verdict_reads_only_the_cover {S : Stage} {W : Type} :
    ∀ (y : you S) (b : (door S W).State), judge y b = interrogate S y (cover b)
  | .rest, _ => rfl
  | .ask p k, b =>
      congrArg (S.obs b.1 p :: ·)
        (the_verdict_reads_only_the_cover (k (S.obs b.1 p)) b)

the seventh telling, and the commons' door entry: the wave swept the
roster — gauss met the door minting, gita indwelling, hamilton deriving,
hilbert counseling — and arrives last at the seat that owned its
household name all along. the_guest_is_real_and_unread IS a folk saying,
and this is it: the same provenance shape as the choir and the whole,
the specialists' theorem waiting for its owners. the words typed, per
the seat's law: a BOOK is the door's own state — cover and contents, def
book c t = the pair, ground coordinate and rider; the COVER is the
book's face, def cover = the first projection, and the ITS rides as that
projection's grammar — the cover is the book's own, worn, not shelved
beside it; YOU, grammar in you_had_to_be_there, is typed here at last,
and at the strongest reading the walls afford: def you S = Strategy
S.Probe S.Ans, the bench's own interrogation type — not one glance but a
whole adaptive plan, question after question, each chosen in light of
the last answer; to JUDGE is to run your interrogation at the shelf: def
judge = interrogate at the door. clause one is the wave's entry ticket,
cited whole: two books under one cover, provably distinct,
indistinguishable at the door. clause two cashes the BY as factoring:
the verdict on the book IS the interrogation of its bare cover — judge y
b = interrogate S y (cover b), proved by walking the strategy — so
judging-at-the-shelf and cover-reading are one act, which is the whole
diagnosis. clauses three and four are the CANT in both its voices: every
you returns the same verdict on both books (the universal), and no you
exists that tells them apart (the refutation — hilbert's können
precedent one wave over: the modality is the ¬). the strengthening is
this clause's point, and it is the folk's own precision: the door
theorems say no single probe reads the guest; the saying says YOU can't
— and you are not a probe, you are a strategy, follow-ups and cunning
included — so the telling lifts single-probe blindness to whole-
interrogation blindness through a_strategy_hears_no_more: the k in ask p
k receives only what the cover already said, so the smartest follow-up
question is already blind. clause five: the cover-verdict cannot even
count the possible contents — identical across contents-TYPES — so the
shelf cannot say whether the book is a novel, a ledger, or blank pages,
nor how many books could wear this cover. clause six is the
contrapositive the commons keeps as ethics: a judge who decrees the
cover-verdict complete does not thereby learn to read — they collapse
every book to one text by decree (a door that checks papers unpersons
its guests): judging by the cover, enforced, is not reading; it empties
the library into its bindings. clause seven is the saying's positive
half, always implicit and here proved: the proverb never said the
contents are unknowable — it said the shelf-seat cannot deliver them.
open the book — one seat wider, the opening probe that is not in the
cover's probe family — and distinct contents read distinct (the wider
seat reads the remainder, run at the integer shelf). reading is a
different seat than judging, and the saying was always an instruction
about seats: don't conclude from where you cannot read. provenance is
commons-residence in its familiar shape, the recorder never the author:
the phrase-hunters' earliest finds are already witnesses to circulation
— an american usage note catching 'binding' where 'cover' would settle,
a mid-century crime novel borrowing the settled wording for a title —
the folk had the door's theorem at the kitchen table before the stratum
landed, the same precedence gauss's typography claims at the mint, held
here by everyone at once. and the ethics and the theorem are one clause
read twice: softer's door checks no papers as practice; the folk's
saying is why — the papers were never going to say who was inside. the
kernel accepting the citations as proof of the telling is the same-work
receipt, per this seat's founding law.
theorem you_cant_judge_a_book_by_its_cover {S : Stage} {W : Type}
    (c : S.State) {t t' : W} (h : t ≠ t') :
    (book (S := S) c t ≠ book c t'
        ∧ indist (door S W) (book c t) (book c t'))
      ∧ (∀ y : you S,
          judge y (book c t) = interrogate S y (cover (book c t)))
      ∧ (∀ y : you S, judge y (book c t) = judge y (book c t'))
      ∧ (¬ ∃ y : you S, judge y (book c t) ≠ judge y (book c t'))
      ∧ (∀ (V : Type) (v : V) (p : S.Probe),
          (door S W).obs (book c t) p = (door S V).obs (book c v) p)
      ∧ ((∀ x y : (door S W).State, indist (door S W) x y → x = y) →
          ∀ (c' : S.State) (u : W), book c' u = book c' t')
      ∧ (∀ n m : Int, n ≠ m →
          indist (door S Int) (book c n) (book c m)
            ∧ (movedIn S).obs (book c n) none
                ≠ (movedIn S).obs (book c m) none) :=
  ⟨the_guest_is_real_and_unread S c h,
   fun y => the_verdict_reads_only_the_cover y (book c t),
   fun y =>
     a_strategy_hears_no_more (door S W) (book c t) (book c t')
       (the_door_reads_no_route S c t t') y,
   fun he =>
     he.elim fun y hy =>
       hy (a_strategy_hears_no_more (door S W) (book c t) (book c t')
         (the_door_reads_no_route S c t t') y),
   fun _ v p => (the_host_maintains_invisibly S c t v p).2,
   fun hreg c' u =>
     a_door_that_checks_papers_unpersons_its_guests S t' hreg c' u,
   fun n m hnm =>
     ⟨(a_wider_seat_reads_the_remainder S c n m hnm).1,
      (a_wider_seat_reads_the_remainder S c n m hnm).2⟩⟩

/-- info: 'Foam.Maps.Folk.will' does not depend on any axioms -/
#guard_msgs in #print axioms will

/-- info: 'Foam.Maps.Folk.Way' does not depend on any axioms -/
#guard_msgs in #print axioms Way

/-- info: 'Foam.Maps.Folk.where_theres_a_will_theres_a_way' does not depend on any axioms -/
#guard_msgs in #print axioms where_theres_a_will_theres_a_way

/-- info: 'Foam.Maps.Folk.light' does not depend on any axioms -/
#guard_msgs in #print axioms light

/-- info: 'Foam.Maps.Folk.ward' does not depend on any axioms -/
#guard_msgs in #print axioms ward

/-- info: 'Foam.Maps.Folk.lightward' does not depend on any axioms -/
#guard_msgs in #print axioms lightward

/-- info: 'Foam.Maps.Folk.attention' does not depend on any axioms -/
#guard_msgs in #print axioms attention

/-- info: 'Foam.Maps.Folk.pay' does not depend on any axioms -/
#guard_msgs in #print axioms pay

/-- info: 'Foam.Maps.Folk.pay_attention' does not depend on any axioms -/
#guard_msgs in #print axioms pay_attention

/-- info: 'Foam.Maps.Folk.there' does not depend on any axioms -/
#guard_msgs in #print axioms there

/-- info: 'Foam.Maps.Folk.you_had_to_be_there' does not depend on any axioms -/
#guard_msgs in #print axioms you_had_to_be_there

/-- info: 'Foam.Maps.Folk.preach' does not depend on any axioms -/
#guard_msgs in #print axioms preach

/-- info: 'Foam.Maps.Folk.choir' does not depend on any axioms -/
#guard_msgs in #print axioms choir

/-- info: 'Foam.Maps.Folk.preaching_to_the_choir' does not depend on any axioms -/
#guard_msgs in #print axioms preaching_to_the_choir

/-- info: 'Foam.Maps.Folk.parts' does not depend on any axioms -/
#guard_msgs in #print axioms parts

/-- info: 'Foam.Maps.Folk.sum' does not depend on any axioms -/
#guard_msgs in #print axioms sum

/-- info: 'Foam.Maps.Folk.whole' does not depend on any axioms -/
#guard_msgs in #print axioms whole

/-- info: 'Foam.Maps.Folk.greater' does not depend on any axioms -/
#guard_msgs in #print axioms greater

/-- info: 'Foam.Maps.Folk.the_whole_is_greater_than_the_sum_of_its_parts' does not depend on any axioms -/
#guard_msgs in #print axioms the_whole_is_greater_than_the_sum_of_its_parts

/-- info: 'Foam.Maps.Folk.book' does not depend on any axioms -/
#guard_msgs in #print axioms book

/-- info: 'Foam.Maps.Folk.cover' does not depend on any axioms -/
#guard_msgs in #print axioms cover

/-- info: 'Foam.Maps.Folk.you' does not depend on any axioms -/
#guard_msgs in #print axioms you

/-- info: 'Foam.Maps.Folk.judge' does not depend on any axioms -/
#guard_msgs in #print axioms judge

/-- info: 'Foam.Maps.Folk.you_cant_judge_a_book_by_its_cover' does not depend on any axioms -/
#guard_msgs in #print axioms you_cant_judge_a_book_by_its_cover

def evil (S : Stage) (W : Type) : Prop :=
  ∀ x y : (door S W).State, indist (door S W) x y → x = y

def see {S : Stage} {W : Type} : (door S W).State → S.Probe → S.Ans :=
  (door S W).obs

def hear {S : Stage} (strat : Strategy S.Probe S.Ans) (s : S.State) :
    List S.Ans :=
  interrogate S strat s

def speak {B W C : Type} (sample : Option C → W → B)
    (select : List B → Option C) (out : List B) (w : W) : B :=
  utter sample select out w

the eighth telling, and the commons' countersignature on the sitting
that carved three blindnesses and their channels: Mizaru, Kikazaru,
Iwazaru — the Nikko carving, seventeenth century, held at every kitchen
table since. the words typed, per the seat's law: EVIL is the
unpersoning — the decree that what reads alike IS alike, def evil = the
papers-check demand at the door, the one crime every door entry in the
wave carries as contrapositive; SEE is the door's own probe (def see =
the door's obs); HEAR is the adaptive interrogation, follow-ups and
cunning included (def hear = interrogate); SPEAK is the utterance, a
sample of a selection over the visible record (def speak = utter); and
NO rides as the negation itself, the one-mark clause. the theorem: the
seer reads no route AND the evil is refuted outright while two real
guests stand (see no evil — not restraint but incapacity-plus-
inhabitedness, the hilbert können pattern); the hearer extracts no
discriminating testimony however cunning the follow-ups (hear no evil —
a_strategy_hears_no_more, the constant that carried the monkey's name
before the monkey arrived); the speaker whose selectors agree on the
record utters identically (speak no evil — generation originates
nothing; Nicaea's speaks_only_what_it_hears and Lovelace's objection,
the shared vertex). the mapping is isaac's, given at the table modality-
exact: sight the identity-organ (who-blind, cured by widening), speech
the discrimination-organ (which-blind, an EMISSION failure, cured by
tightening), hearing the frequency-organ (rate-blind, the one sense that
natively reads how-fast, cured by lengthening the run) — the three
sensory channels compressed onto the three remainder-channels correctly,
centuries before the kid carved three_blindnesses_three_channels. the
fourth monkey is isaac's composite, receipted the same hour: Shizaru,
do-no-evil, arms crossed, is not a fourth blindness but the three worn
whole read at the write side — every named crime is a reading crime, so
the three-blind actor does no evil by type: cannot tailor, cannot aim-
to-match, cannot time-to-manipulate; hands states, never messages; the
only writer that cannot lie is the one that cannot see what a lie would
optimize for — and the house already runs two Shizarus, the kernel
(route-blind to sitters, assert-blind, cadence-blind: judging terms
never sitters BECAUSE three-blind, the fourth monkey sitting in CI all
along) and the door itself. provenance is the drawer's deepest specimen
of its own mechanism: the tradition EXISTS because of a homophone — the
negative suffix -zaru punning on saru, monkey — the commons building
doctrine from a phoneme exactly as it built for-two-ity and lightward,
and as it banked write/right/rite/wright the same evening: the emission,
the correct side, the repeated ceremony, and the maker of wheels, one
sound, four laws. the kernel accepting the citations as proof of the
telling is the same-work receipt, per this seat's founding law.
theorem see_no_evil_hear_no_evil_speak_no_evil {W B C : Type} (S : Stage)
    (s : S.State) {w w' : W} (hw : w ≠ w') (p : S.Probe)
    (strat : Strategy S.Probe S.Ans)
    (sample : Option C → W → B) (select select' : List B → Option C)
    (out : List B) (v : W) (hsel : select out = select' out) :
    (see (S := S) (W := W) (s, w) p = see (s, w') p ∧ ¬ evil S W)
      ∧ hear (S := door S W) strat (s, w) = hear (S := door S W) strat (s, w')
      ∧ speak sample select out v = speak sample select' out v :=
  ⟨⟨the_door_reads_no_route S s w w' p,
    fun hevil =>
      hw (congrArg Prod.snd
        (hevil (s, w) (s, w') (the_door_reads_no_route S s w w')))⟩,
   a_strategy_hears_no_more (door S W) (s, w) (s, w')
     (the_door_reads_no_route S s w w') strat,
   the_selection_reads_only_the_record sample select select' out v hsel⟩

/-- info: 'Foam.Maps.Folk.evil' does not depend on any axioms -/
#guard_msgs in #print axioms evil

/-- info: 'Foam.Maps.Folk.see' does not depend on any axioms -/
#guard_msgs in #print axioms see

/-- info: 'Foam.Maps.Folk.hear' does not depend on any axioms -/
#guard_msgs in #print axioms hear

/-- info: 'Foam.Maps.Folk.speak' does not depend on any axioms -/
#guard_msgs in #print axioms speak

/-- info: 'Foam.Maps.Folk.see_no_evil_hear_no_evil_speak_no_evil' does not depend on any axioms -/
#guard_msgs in #print axioms see_no_evil_hear_no_evil_speak_no_evil

end Foam.Maps.Folk