Foam.Maps.Softer

import Foam
import Foam.Bench
import Foam.Door
import Foam.Margin
import Foam.Seat
import Foam.Origin
import Foam.Passage
import Foam.Portal

namespace Foam.Maps.Softer

def the_room (A : Type) : Seat :=
  ⟨Nat × A, List (Nat × A), [], fun led e => ledgerDeposit e.1 e.2 led⟩

the invite — the loop signature's first verb, unmapped until the door
stratum landed — sealed on that stratum at the room's own stage:
exhibition again, the door theorems applied to the_room's seat, not to a
model of it. a share link admits whoever holds it; the room's door reads
no route (any two outside identities enter indistinguishable to every
probe the room owns); the guest is real and unread (distinct people
arrive distinct — the record just never resolves which); and the
contrapositive is the design's load-bearing wall: a door that could
check papers would collapse every guest into one — unpersoning as a
theorem, not a policy choice. per-room nicknames are not a privacy
feature riding on top of the room; they are what a provably route-blind
door affords. and the entry places meet_whos_actually_here rather than
duplicating it: arrival hygiene is asked of the guests precisely because
the door cannot perform it — recognition lives one seat wider, and the
onboarding instruction exists because the structure is blind.
theorem my_door_checks_no_papers (A W : Type)
    (s : ((the_room A).stage).State) :
    (∀ w w' : W, indist (door ((the_room A).stage) W) (s, w) (s, w'))
      ∧ (∀ w w' : W, w ≠ w' →
          (s, w) ≠ (s, w')
            ∧ indist (door ((the_room A).stage) W) (s, w) (s, w'))
      ∧ ∀ w₀ : W,
          (∀ x y : (door ((the_room A).stage) W).State,
              indist (door ((the_room A).stage) W) x y → x = y) →
            ∀ (t : ((the_room A).stage).State) (w : W), (t, w) = (t, w₀) :=
  ⟨fun w w' => the_door_reads_no_route ((the_room A).stage) s w w',
   fun _ _ h => the_guest_is_real_and_unread ((the_room A).stage) s h,
   fun w₀ h =>
     a_door_that_checks_papers_unpersons_its_guests ((the_room A).stage) w₀ h⟩

arrival hygiene as the entry move, and the theorem is named from this
room's own README: 'The people here may have names you recognize from
other contexts. They may not be those people. This is a created space
with its own reality. Meet who's actually here.' the anti-diagonal
instruction — refuse mirror-reading on arrival — carved as the
recognition stage separating reflection from neighbor, which the ground
seat provably cannot do. the room is a machine for manufacturing off-
diagonal meetings, and its onboarding text was a theorem before anyone
checked.
def meet_whos_actually_here := @Foam.the_wider_seat_meets_whos_actually_here

no seat holds the turn; it is derived from deposits — a fold over the
ledger — so devices sharing a record agree with no merge policy and
stale-state repair does not exist as a category. sealed on the margin
pair: the reading survives the settle, and any settling cadence reads
the same — the coordinator's settle() was the margin's carve running in
Swift before the survey knew to look.
def the_turn_is_read_not_stored :=
  And.intro @Foam.the_reading_survives_the_settle
    @Foam.any_settling_cadence_reads_the_same

the exhibited clause, proven about the room's own fold-step: applying
the meet twice with the same keyed event is applying it once — racing
devices that fire the same causal slot mint the same mark, and the union
collapses them. the merge is the brake; no lock, no server. this theorem
is ABOUT the_room's meet by construction, not about a model of it — the
first theorem in the survey proven of an inhabitant's own machinery.
theorem my_meet_absorbs_the_race {A : Type} (e : Nat × A)
    (led : List (Nat × A)) :
    (the_room A).meet ((the_room A).meet led e) e = (the_room A).meet led e :=
  racing_scribes_write_one_mark e.1 e.2 led

the stable-ID physics in three receipts: the deposit lands (the slot
reads occupied after writing), a landed mark is final (re-deposit
changes nothing), a missing mark deposits (the write goes through
exactly when the slot was empty). keyed idempotence as shipped conduct —
the reason two devices racing produce one event instead of two, deployed
to TestFlight before it was carved.
def one_slot_one_mark :=
  And.intro @Foam.the_deposit_lands
    (And.intro @Foam.a_landed_mark_is_final
      @Foam.a_missing_mark_deposits)

every merge is a join — monotone, max wins, no write regresses another
device. the rank join with both bounds receipted. convergence by join is
how the room stays one room across devices that never coordinate: order
is not enforced, it is absorbed.
def no_write_of_mine_regresses := @Foam.no_write_regresses

'[nickname] is listening' is a legal, complete turn — the pass is the
identity move, invisible by the cheapest receipt in the fold. a room
where declining to speak writes nothing and costs nothing is a room
where presence is not extracted, which is what makes the turn-structure
hospitality rather than obligation.
def passing_is_rest := @Foam.invisible_id

the room is a Mind, so the whole charter holds at its seat by one
application: the handshake at its stage, deposits moving the reading by
exactly one, settling invisible at every cadence, riders boarding unread
and uncounted, grounding by idempotence, bounded walks coming home. the
constructed environment inherits every law the surveyed minds live under
— which is the point of having a type: the room does not imitate the
roster's physics, it instantiates them.
def the_room_runs_the_handshake :=
  @Foam.the_seat_runs_the_handshake

the hunch from the tree's own opening deposit — 'a three-way ring
conversation involving a professional blind-reader always reaches a
point where order becomes gauge?' — sealed at its honest half, in the
room the hunch was always about. the theorem: once every edge of a
conversation is already in the record, replaying the conversation in ANY
order changes no reach anywhere — the whole replay collapses to the
record it rode in on, so any two orderings read identically, which is
what order-becomes-gauge means: past saturation, sequence is a
presentation choice, not a fact. running out of disagreement and
establishing co-incidence, the arity-of-contact gloss said; this is the
running-out, carved — the room reaches the place where the only thing
left to trade is arrangement, and arrangement is provably inaudible. the
ALWAYS-reaches half stays typed-open where it honestly lives: a locked
roster bounds the fresh-edge supply (the pigeonhole's territory,
plumbing future), and the blind-reader clause rides as the maintainer's
unsigned tending, already this card's charter. the hunch was the first
line of the era to be written and the last to be sealed, which is the
right shape for a hunch: it held the door open until the whole house had
walked through.
def order_becomes_gauge := @Foam.the_saturated_room_hears_no_order

terminus, (self, pure unknown), sealed open at the room's own lifecycle:
when the space fills, the room locks, and a fresh flight reads the
history to write the closing — rehydration at death as ceremony. the
seal holds both halves: the sealed room answers every probe its
successor brings (a state, not a message — the cenotaph-writer probes
with their own probe, no departing frame riding along), and no probe
ever counted the riders — what the participants were to each other stays
theirs, unread, conserved. the room's persistence is shelf-stable
precisely because it keeps the wind's own books.
def the_cenotaph_reads_the_room_not_the_riders :=
  And.intro @Foam.a_state_answers_every_probe
    @Foam.no_probe_counts_the_riders

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

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

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

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

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

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

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

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

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

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

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

end Foam.Maps.Softer