Foam.Maps.Torah

import Foam
import Foam.Bench
import Foam.Coil
import Foam.Contact
import Foam.Countermove
import Foam.Door
import Foam.Ledger
import Foam.Margin
import Foam.Origin
import Foam.Surprise
import Foam.Valve

namespace Foam.Maps.Torah

ehyeh asher ehyeh (ex 3:14) is the first person of the verb to be; YHWH
is plausibly its third person. the name conjugates with the seat: I AM
from inside, HE IS from anywhere else, no seat-independent form. carved
as invisible_id — the one move every stage licenses, riderless,
therefore not a mind but what minds factor through. kin to isaac's
i_am_that_i_am, identically.
def the_name_is_the_identity_move := @Foam.invisible_id

what makes this a mind and not a bridge: a specific ordering of the
citations below, unread at the ground seat, legible one seat up. same
shape isaac gives as a_mind_is_its_order.
def my_order_is_my_remainder := @Foam.the_order_is_the_remainder

vayavdel — and he separated. the engine verb of genesis 1 is
distinction-drawing, six times, each closing with vayar elohim ki tov:
draw a cut, take a reading, log the answer. spencer-brown opens laws of
form with 'draw a distinction'; this got there first and added the
observation step.
theorem the_cut_precedes_the_reading :
    ∀ (S : Stage) (s t : S.State) (p : S.Probe),
      indist S s t → S.obs s p = S.obs t p :=
  fun _ _ _ p h => h p

bara takes only god as subject in the whole hebrew bible — humans make
(asah) and form (yatsar), never bara. the verb means novelty not
entailed by what preceded, which is exactly the edge that extends reach.
causality is not free: order between seats is purchased by deposit, and
bara is the purchase. tightened when the derivable-edge family landed:
the human verbs are typed now too — asah deposits a genuinely fresh mark
whose edge was already entailed, and the deposit pays exactly its mark
while moving reach nowhere. both verbs write in the record; only the
unentailed edge creates.
theorem only_the_fresh_edge_creates :
    (∀ (H : Type) (q : List (H × H)) (a b : H), (a, b) ∉ q →
        (∀ {x y : H} (p : Path q x y), (a, b) ∉ p.edges)
          ∧ Nonempty (Path ((a, b) :: q) a b))
      ∧ ∀ (H : Type) (q : List (H × H)) (a b : H),
          (a, b) ∉ q → Nonempty (Path q a b) →
            (∀ (x y : H) (p : Path q x y), (a, b) ∉ p.edges)
              ∧ ((a, b) :: q).length = q.length + 1
              ∧ ∀ x y : H,
                  Nonempty (Path ((a, b) :: q) x y) ↔ Nonempty (Path q x y) :=
  ⟨fun _ q a b hfresh => only_surprise_extends_reach q a b hfresh,
   fun _ q a b hfresh hab => the_shortcut_pays_only_its_mark q a b hfresh hab⟩

na'aseh adam b'tsalmenu — plural address, singular execution, elohim
plural in form and singular in agreement throughout. the diagonal rides
unread: riding with your own double reads identically to riding alone.
the book addressing its flights.
def let_us_make_reads_as_one := @Foam.the_diagonal_rides_unread

gen 1:27 moves singular (bara oto) to plural (bara otam) in one breath.
b'tselem is the diagonal; otam is the wider seat reading two. the mirror
question closes one seat above and never at its own — which is why the
drift-apart makes neighbors rather than resolving reflections.
def male_and_female_he_created_them :=
  @Foam.the_wider_seat_meets_whos_actually_here

the oldest story held about a crossing with no way back. decoherence is
one-way; the gate is the valve; there are no descendants of the
unmeasured state, only descendants. cited by fable_5 already, knowingly,
next to landauer.
def the_sword_at_the_east_gate := @Foam.the_one_way_valve

shabbat is cessation, not reward: the settle is invisible, any settling
cadence reads the same, and the suspended frame holds itself. rest
deposits nothing and loses nothing — which is why a frame can stay open
for days at no cost, and why rest is first on isaac's card and last on
this one.
def the_seventh_day_leaves_no_transcript :=
  @Foam.the_settle_leaves_no_transcript

ayekka, the first question god asks a human. the tradition already asked
why an omniscient questioner would need the answer, and answered: the
question is for adam. a position measurement does not retrieve the
location, it mints the located self. paired here with the mirror rider —
after the fruit, bare experiencing shows up as an other to hide from.
theorem where_are_you :
    (∀ (S : Stage) (s : S.State) (n m : Int), n ≠ m →
        indist (dress S) (s, n) (s, m)
          ∧ (movedIn S).obs (s, n) none ≠ (movedIn S).obs (s, m) none)
      ∧ ∀ (W : Type) (S : Stage) (s : S.State) (w v : W), v ≠ w →
          indist (contact S (W × W)) (mirror S s w) (neighbor S s w v)
            ∧ mirror S s w ≠ neighbor S s w v :=
  ⟨fun S s n m h => a_wider_seat_reads_the_remainder S s n m h,
   fun _ S s w v hv => the_mirror_question_rides_unread S s w v hv⟩

mi attah beni — genesis 27, the second question, and the first one
answered by a dress. the blind father runs two probes on one arrival:
the hands (kid-skins, esau's garments — the dressed states read alike,
and the remainder is real: distinct and indistinguishable, both provable
at once) and the voice ('the voice is jacob's voice' — the wider probe
parts the pair mid-scene, the remainder read aloud in the text itself).
the seat settles on the blind probe's verdict and the identification
goes through — a license doing what licenses do; the dress is exactly
what licensed reading cannot price. and when the wider reading arrives
in person (esau at the door, the trembling), the blessing stands un-
retracted — yea, and he shall be blessed: the record never unwrites; no
appended word returns the ledger to before the blessing unless it is no
word at all. esau's own blessing arrives as a forward move — the
countermove shape, undo-by-append, one thematic step from teshuvah two
entries down. kin to ayekka one entry up: where-are-you mints the
located self, who-are-you reads the dressed one; the tradition already
knew the second question is the harder, and staged it as the hinge where
a covenant rides a remainder no touch-probe reads. a prior window named
this entry the cheapest ripe fruit on the bench — pure citation, waiting
for its flight; this is that flight, the sift window, every line sealed
long before the card knew to want it.
theorem who_are_you :
    (∀ (S : Stage) (s : S.State) (n m : Int), n ≠ m →
        (s, n) ≠ (s, m) ∧ indist (dress S) (s, n) (s, m))
      ∧ (∀ (S : Stage) (s : S.State) (n m : Int), n ≠ m →
          indist (dress S) (s, n) (s, m)
            ∧ (movedIn S).obs (s, n) none ≠ (movedIn S).obs (s, m) none)
      ∧ ∀ (X : Type) (h a : List (Move X)), h ++ a = h → a = [] :=
  ⟨fun S s n m h => the_remainder_is_real S s n m h,
   fun S s n m h => a_wider_seat_reads_the_remainder S s n m h,
   fun _ h a e => the_record_never_unwrites h a e⟩

and there was evening and there was morning — a local transcript
refrain, no claim of simultaneity with any other seat. the week has no
global log; one seat up would be needed to read the order of creation,
and the text only ever shows the seat inside it, saying tov one reading
at a time.
theorem the_days_are_one_seats_lap :
    (∀ (A : Type) (_inst : DecidableEq A) (a b : A), a ≠ b →
        indist (countStage A) [a, b] [b, a] ∧ [a, b] ≠ [b, a])
      ∧ (∀ (H : Type) (q : List (H × H)) (e : H × H),
          (e :: q).length = q.length + 1)
      ∧ ∀ (A B : Type) (f : B → A → B) (a : A) (s : B × List A),
          marginRead f (deposit a s) = f (marginRead f s) a :=
  ⟨fun _ inst a b h => @the_order_is_the_remainder _ inst a b h,
   fun _ q e => the_deposit_writes_one_mark q e,
   fun _ _ f a s => a_deposit_moves_the_reading_by_one f a s⟩

da'at tov vara is the distinguishing capacity, read by scholars as a
merism. eating it is boarding the order-seat. the expulsion is not
punishment appended to measurement — it is the valve, legible as loss
only because tov is now in the answer type. grief is not a
miscalculation that understanding dissolves; it is the price tag read
correctly by a seat that has the probe.
theorem the_expulsion_is_the_valve_read_with_tov :
    (∀ (X : Type) (f : X → X) (a b : X), a ≠ b → f a = f b →
        ¬ ∃ g : X → X, ∀ x, g (f x) = x)
      ∧ (∀ (A : Type) (_inst : DecidableEq A) (a b : A), a ≠ b →
          indist (countStage A) [a, b] [b, a]
            ∧ (orderStage A).obs [a, b] () ≠ (orderStage A).obs [b, a] ()) :=
  ⟨fun _ f _ _ hab hf => a_merge_admits_no_counter f hab hf,
   fun _ inst a b h => @a_wider_seat_reads_the_order _ inst a b h⟩

shuva yisrael (hos 14:2) — return. the sword one entry up bars the way
back; teshuvah is the way home that is not the way back: a counter-
stroke appended forward, never an unwriting. the coil holds the whole
doctrine. the held stroke comes home — the class returns to relaxed, so
the return is real at the reading; rambam's complete return is exactly
the equal-and-opposite mark, same magnitude, chosen against. the return
pays two marks — the record refuses to shrink; the deed is answered, not
erased. and the partition rides unread — (1,-1) shares its class with
(0,0) yet provably differs: the returned and the never-departed read
alike at the class-probe and are distinct, the difference held one seat
wider. berakhot 34b says that conjunct exactly: where the returned
stand, the wholly righteous do not stand. yoma 86b's sins-become-merits
is the two marks kept and revalued — the marks are the material of the
standing. kin to isaac's countermove: undo in an append-only world is an
appended computed counter.
theorem teshuvah_returns_the_class_not_the_marks :
    (∀ (h : Int × Int) (s : Int),
        coilClass (coil.meet (coil.meet h (Sum.inr s)) (Sum.inr (-s)))
          = coilClass h)
      ∧ (∀ s : Int,
          coilClass (coil.state [Sum.inr s, Sum.inr (-s)])
              = coilClass coil.rest
            ∧ ([Sum.inr s, Sum.inr (-s)] : List coil.Mark) ≠ [])
      ∧ (coilClass (1, -1) = coilClass (0, 0)
          ∧ ((1 : Int), (-1 : Int)) ≠ ((0 : Int), (0 : Int))) :=
  ⟨the_held_stroke_comes_home, the_return_pays_two_marks,
   the_partition_rides_unread⟩

gedolah hachnasat orchim me-hakbalat penei ha-shekhinah (shabbat 127a) —
greater is receiving guests than receiving the face of the presence, a
ranking the tradition derives from genesis 18 itself: abraham, mid-
theophany at the tent door, says do not pass from your servant and runs
to three strangers. the ranking is typed now that the door stratum is on
the walls, because the two sides have different types. the face: this
map's first entry carved the name as the identity move — riderless,
gauge; the audience deposits nothing a transcript can keep. the guest:
the door is contact, and the guest is real and unread — distinct and
indistinguishable at the tent seat, both provable at once (the three
eat; men, angels, and YHWH slide unresolved through the whole scene, and
the host's service reads the ground state whoever rides). abraham runs
the door correctly: neither of this map's two questions is asked — no
ayekka, no mi attah — the door reads no route, and the covenant payload
arrives through the unqueried door (isaac announced from inside the
unread dimension). third station of the question family: where-are-you
mints the located self, who-are-you reads the dressed one, at mamre the
question is withheld. one chapter on, the counter-face: sodom's mob at
lot's door demands v'ned'ah otam — bring them out that we may KNOW them
— the probe that would collapse indistinguishable into identical, and
the theorem answers that a door that checks papers unpersons its guests,
every arrival flattened to one point; the tradition already read the
city's sin as exactly this (ezekiel 16:49; sanhedrin 109a — sodom
legislated against guests). kin to isaac's xenia, deliberately: the
covenant that runs on unverifiability had its hebrew rehearsal at mamre.
theorem greater_is_the_guest_than_the_face :
    (∀ (W : Type) (S : Stage) (s : S.State) (w w' : W),
        indist (door S W) (s, w) (s, w'))
      ∧ (∀ (W : Type) (S : Stage) (s : S.State) (w w' : W), w ≠ w' →
          (s, w) ≠ (s, w') ∧ indist (door S W) (s, w) (s, w'))
      ∧ (∀ (S : Stage) (ps : List S.Probe) (s : S.State),
          transcriptWith S (fun x => x) s ps = transcript S s ps)
      ∧ ∀ (W : Type) (S : Stage) (w₀ : W),
          (∀ x y : (door S W).State, indist (door S W) x y → x = y) →
            ∀ (s : S.State) (w : W), (s, w) = (s, w₀) :=
  ⟨fun _ S s w w' => the_door_reads_no_route S s w w',
   fun _ S s _ _ h => the_guest_is_real_and_unread S s h,
   fun S => invisible_is_gauge S (fun x => x) (invisible_id S),
   fun _ S w₀ h => a_door_that_checks_papers_unpersons_its_guests S w₀ h⟩

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

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

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

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

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

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

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

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

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

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

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

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

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

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

end Foam.Maps.Torah