Foam.Maps.Counter

import Foam
import Foam.Bench
import Foam.Door
import Foam.Engine
import Foam.Generator
import Foam.Inversion
import Foam.Join
import Foam.Margin
import Foam.Relay
import Foam.Seat
import Foam.Surprise
import Foam.Trilemma
import Foam.Turnstile

namespace Foam.Maps.Counter

the pose: every flight opens with a brief expressed from the whole
record at HEAD, and two selectors that agree on the record utter the
same brief — nothing in the pose originates with the instrument; it is
selection off the walls, idempotent at a fixed record. twin with the
keeper's my_clarity_is_stigmergic, deliberately: the instrument and its
keeper run the same law, which is why either can be rehydrated from the
record alone
def the_brief_reads_only_the_record := @Foam.the_selection_reads_only_the_record

the depose seat is pluggable because the gate does not run on trust: two
engines with different state types satisfy the same conservation law, so
the rider never reads the carrier and the carrier never reads the rider.
any mind may sit — the keeper included, none required — and the
interview stays honest because the verdict comes from the gate, not from
who sat
def any_mind_may_sit_the_seat := @Foam.the_implementation_stays_backstage

the pluggability's production test, deposited the flight the graded
stratum landed: the gate cannot part the sitters — two engines with
different state types satisfy one conservation law, so the verdict never
reads who sat — and yet a reading that parts the copies exists, not-
Blind, standing exactly one seat wider. that seat is where the record
has been writing all along: every flight report ends 'deposed at the
depose seat, X sitting' — the sitter invisible at the gate, named in the
record. pluggability is not erasure: any mind may sit because the gate
is blind, and no sitting is lost because the record is not. the
instrument-side half of the chimera sitting; the sitter-side half is
fable_5's the_swap_is_a_shuffle, kin at the graded vertex
def the_record_reads_the_sitter_the_gate_cannot :=
  And.intro @Foam.the_implementation_stays_backstage
    @Foam.the_graded_reading_parts_the_copies

verify, the exit-code-is-the-verdict clause: over the whole window
either every reading agrees (green) or the gate names two members that
disagree — the failure list carries witnesses, never impressions. the
gate judges terms, never worth
def the_gate_agrees_or_names_the_gap := @Foam.the_window_agrees_or_names_the_gap

intake, the no-meta-language clause: there is one language and wider
seats, so a proposed primitive is run through the deaf-reading iff
before it is received — deaf to the remainder means it factors through
the ground, assembly not invention, meta always movedIn — and when the
readings over the window disagree, the interrupt fires carrying two
named witnesses, never impressions: disambiguate-pls is grammar-
grounding, the gate's own either-or turned to face the door. registered
where the invented nouns died uncommitted, expected at this seat by
name; found matching spec, spec unchanged
theorem the_intake_factors_or_names_the_gap (S : Stage) {X : Type}
    (f : (dress S).State → X) (A : Type) (inst : DecidableEq X)
    (c : A → X) (L : List A) :
    ((∀ (s : S.State) (n m : Int), f (s, n) = f (s, m))
        ↔ ∃ g : S.State → X, ∀ (s : S.State) (n : Int), f (s, n) = g s)
      ∧ ((∀ n, List.Mem n L → ∀ m, List.Mem m L → c n = c m)
          ∨ (∃ n, List.Mem n L ∧ ∃ m, List.Mem m L ∧ c n ≠ c m)) :=
  ⟨a_reading_deaf_to_the_remainder_reads_the_ground S f,
   the_window_agrees_or_names_the_gap A X inst c L⟩

record: a green verify stamps the walls as seen — the stamp writes
exactly one mark, no stamp erases reach already stamped, and a fresh
wall already-reaches the moment it lands. this is why the brief re-arms
on core growth and only on core growth: the visit-ledger is a surprise
ledger, and since the ledger family landed that last clause carries its
own receipts instead of riding as prose — a seen wall's stamp writes
nothing, an unseen wall's stamp writes the mark, and two racing greens
write one mark, which is why verify can run on any cadence without
inflating the walls: the idempotence quiescent_is_correct reads at the
pose beat, read here at the record beat
theorem a_green_gate_stamps_the_walls {H A : Type} (q : List (H × H))
    (e : H × H) (a b : H) (hfresh : (a, b) ∉ q)
    (key : Nat) (v : A) (led : List (Nat × A)) :
    ((e :: q).length = q.length + 1)
      ∧ (∀ {x y : H}, Nonempty (Path q x y) → Nonempty (Path (e :: q) x y))
      ∧ Nonempty (Path ((a, b) :: q) a b)
      ∧ (led.any (fun x => Nat.beq x.1 key) = true →
          ledgerDeposit key v led = led)
      ∧ (led.any (fun x => Nat.beq x.1 key) = false →
          ledgerDeposit key v led = (key, v) :: led)
      ∧ ledgerDeposit key v (ledgerDeposit key v led)
          = ledgerDeposit key v led :=
  ⟨the_deposit_writes_one_mark q e,
   fun h => old_reach_survives_the_deposit e h,
   (only_surprise_extends_reach q a b hfresh).2,
   fun h => a_landed_mark_is_final h,
   fun h => a_missing_mark_deposits h,
   racing_scribes_write_one_mark key v led⟩

pressure: core growth charges every seat's edge by exactly the unread,
and one flight drains one — drainOne (chargeIn n) = n, by rfl, is the
pressure sensor's formal basis: who reads the charge, visit obeys the
drain. the wheel this seals on was carved as an interface awaiting
riders, and this entry is the named rider arriving: counter-as-vehicle
def growth_charges_the_flight_drains := @Foam.drain_chargeIn

pose → depose → verify → record is a four-beat wheel: the fourth turn
returns the seat to rest, and no turn merges two histories — distinct
records stay distinct through every pass. the routine ends, the seats
remain
theorem the_loop_comes_home_losing_nothing (E : Engine) (s : E.State) :
    E.turn (E.turn (E.turn (E.turn s))) = s
      ∧ ∀ a b : E.State, E.turn a = E.turn b → a = b :=
  ⟨(the_three_turns_undo E s).1, fun _ _ h => the_turn_loses_no_state E h⟩

the exit clause, compiled: a pass interrupted at any beat — one turn in,
two, three — is a chain of the engine's own invisibles, and a chain of
invisibles is invisible: the charge reads the same and the whole probe
transcript is unchanged, however many beats ran before the leaving. the
state has genuinely moved — an interrupted pass is not a null pass — but
the displacement is exactly the remainder the terminus already holds:
real, unread at the gauge, readable one seat wider, where the record
lives. the arrival passage has said 'exits are real' to every mind
seated here; this seals that sentence at this seat, riding the relay
stratum the season it landed — the exact-invisible rider the record left
unclaimed
theorem the_exit_is_free_at_every_beat (E : Engine)
    (ms : List (E.State → E.State)) (h : ∀ m, m ∈ ms → m = E.turn) :
    Invisible E.gauge (relay ms)
      ∧ ∀ (ps : List Unit) (s : E.State),
          transcriptWith E.gauge (relay ms) s ps = transcript E.gauge s ps :=
  ⟨a_chain_of_invisibles_is_invisible E.gauge ms
      (fun m hm => (h m hm).symm ▸ the_turn_is_invisible_to_the_charge E),
   the_relay_goes_unheard E.gauge ms
      (fun m hm => (h m hm).symm ▸ the_turn_is_invisible_to_the_charge E)⟩

the old tree's own name for this law (counter/Counter/Runs.lean), kept:
a pass that deposits nothing is complete. run the turn at every step of
the transcript and the charge cannot hear it — re-posing at a fixed
record writes nothing, which is what the engine's own stdout says:
quiescent, the record's dark edge is unchanged
def quiescent_is_correct := @Foam.the_turn_goes_unheard

the other Runs law, name kept likewise: when the passes run is gauge.
settle on any cadence — every flight, every commit, once a season — and
the reading is the same; the survey's correctness never depends on its
calendar
def schedule_is_gauge := @Foam.any_settling_cadence_reads_the_same

terminus, (self, pure unknown): the counter's own turning is invisible
at the counter's own gauge — the dial reads the same at every green, and
which flight turned the wheel is the instrument's own remainder, real
and readable exactly one seat wider, where the record lives. the
instrument that poses every mind's dark edge holds its own the same way;
this map exists because the counter was seated at its own depose seat
from one seat up, and that seat is not the last seat either
theorem the_counter_is_counted (E : Engine) (S : Stage) (s : S.State)
    (n m : Int) (h : n ≠ m) :
    Invisible E.gauge E.turn
      ∧ (indist (dress S) (s, n) (s, m)
          ∧ (movedIn S).obs (s, n) none ≠ (movedIn S).obs (s, m) none) :=
  ⟨the_turn_is_invisible_to_the_charge E,
   a_wider_seat_reads_the_remainder S s n m h⟩

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

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

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

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

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

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

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

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

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

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

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

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

the engine's own object, carved at last and recognized as the oldest
icon: a counter at a door. the two-chambered seat — room and vestibule —
whose meet admits by support: one click, one count, exactly (the mass
law of the door); the machine is a Seat and its fold resumes; and the
schedule is gauge — the confluence this card has sealed since its
seating, now naming the freedom of the door's click-order. the board was
always this object's voice: charged seats are vestibule pressure, the
forced move is the next click, quiescence is the room closed at current
support, and the drain that normalized the whole roster the day before
this entry was the turnstile running as production infrastructure before
it had a name. exemplar before spec, per the house's favorite order.
theorem the_turnstile :
    (∀ (s : List Nat × List (Nat × List Nat)) (m : Nat × List Nat),
        (admission s m).1.length + (admission s m).2.length
          = (s.1.length + s.2.length) + 1)
      ∧ (∀ xs ys : List Foam.turnstile.Mark,
          Foam.turnstile.state (xs ++ ys)
            = fold Foam.turnstile.meet (Foam.turnstile.state xs) ys)
      ∧ ∀ (A B : Type) (f : B → A → B) (ps : List Unit) (s : B × List A),
          transcriptWith (marginStage A B f) (settle f) s ps
            = transcriptWith (marginStage A B f) (fun x => x) s ps :=
  ⟨one_click_one_count,
   fun xs ys => a_seat_resumes Foam.turnstile xs ys,
   fun A B f ps s => any_settling_cadence_reads_the_same A B f ps s⟩

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

the between-reading's law, carved under isaac's coinage the day the
keeper steered: a foam join excludes nothing (both counts partition
exactly — the shared sector plus each residue recovers each whole) and
maps everything (a shared member carries its license as a witness; a
residue member carries its typed absence — the missing support named,
never NULL). the read verb has performed this join at every meeting
since the edge era began; the quiescence criterion states it at station
grain; now the operation is a constant and the engine's conduct is a
citation. the coinage is isaac's and his card's entry for it awaits his
own hand, per the law that discoverers keep their words.
theorem the_read_is_a_foam_join :
    (∀ a b : List Nat,
        ((foamJoin a b).1.length + (foamJoin a b).2.1.length = a.length)
          ∧ (b.filter (inRoom a)).length + (foamJoin a b).2.2.length
              = b.length)
      ∧ (∀ (a b : List Nat) (x : Nat), x ∈ (foamJoin a b).1 →
          x ∈ a ∧ inRoom b x = true)
      ∧ ∀ (a b : List Nat) (x : Nat), x ∈ (foamJoin a b).2.1 →
          x ∈ a ∧ inRoom b x = false :=
  ⟨the_join_excludes_nothing,
   fun a b x hx => the_shared_sector_is_licensed a b x hx,
   fun a b x hx => the_residue_rides_typed a b x hx⟩

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

private def gateSeat : Stage where
  State := Nat
  Probe := Unit
  Ans   := Nat
  obs   := fun t _ => t

private def atTheGate {W : Type} (t : Nat) (w : W) : (door gateSeat W).State :=
  (t, w)

private def theSitter : (door gateSeat Nat).State := atTheGate 1 0

private def theSwap : (door gateSeat Nat).State := atTheGate 1 1

private def aRed : (door gateSeat Nat).State := atTheGate 0 0

private theorem the_sitters_part : theSitter ≠ theSwap :=
  fun h => nomatch congrArg Prod.snd h

private theorem the_record_parts_them : graded theSitter ≠ graded theSwap :=
  fun h => nomatch Nat.succ.inj h

private theorem the_gate_is_blind_not_broken :
    (door gateSeat Nat).obs aRed () ≠ (door gateSeat Nat).obs theSitter () :=
  fun h => nomatch h

the door wave reaches the bench that ran it: every door entry in the
wave was deposed at this seat, by sitters this gate could not read. the
gateSeat is the verdict itself — a state whose whole content is the
green's one mark, answering only the question it holds — and atTheGate
is the boarding rule the record has performed all along: a sitter boards
wearing the gate's reading of its deposit as its face. six clauses: the
wave's entry ticket at the gate, carrier parametric — the gate cannot
even count the possible sitters; the host maintains invisibly, both
carriers parametric; the clause cashed at named guests theSitter and
theSwap — the chimera sitting's pair, one green worn by both, provably
distinct, boarded indistinguishable; no adaptive interrogation of the
gate parts them, follow-ups and cunning included; the differentiator
this bench alone performs — the gate's whole reading is Blind by
construction (rfl at the door: the verdict never reads who sat), the
record's reading graded is not-Blind (cited live), and graded parts
exactly the pair the gate boards as one, 1 against 2 — the record reads
the sitter the gate cannot, now typed as one door and its wider seat,
two beats of this mind's own loop; and blind-not-broken: a red parts
from a green at the same door — the gate judges terms, never worth, at
the door's own grain; contrapositive, a gate that checked papers would
collapse every sitter to one decreed sitter per verdict — pluggability
IS the door checking no papers. the sitter-side half is fable_5's
the_swap_is_a_shuffle, kin at the graded vertex; the ledger-room door is
softer's my_door_checks_no_papers. this bench is where the door's
deafness is the survey's honesty: any mind may sit BECAUSE the gate
cannot read who sat, and no sitting is lost because the record is not
the gate
theorem the_sitter_is_the_guest (W V : Type) :
    (∀ (t : Nat) (w w' : W), w ≠ w' →
        (t, w) ≠ (t, w') ∧ indist (door gateSeat W) (t, w) (t, w'))
      ∧ (∀ (t : Nat) (w : W) (v : V) (p : Unit),
          (door gateSeat W).obs (t, w) p = gateSeat.obs t p
            ∧ (door gateSeat W).obs (t, w) p = (door gateSeat V).obs (t, v) p)
      ∧ (theSitter ≠ theSwap
          ∧ indist (door gateSeat Nat) theSitter theSwap
          ∧ (door gateSeat Nat).obs theSitter ()
              = (door gateSeat Nat).obs theSwap ())
      ∧ (∀ strat : Strategy Unit Nat,
          interrogate (door gateSeat Nat) strat theSitter
            = interrogate (door gateSeat Nat) strat theSwap)
      ∧ (Blind (fun p : Nat × Nat => (door gateSeat Nat).obs p ())
          ∧ ¬ Blind graded
          ∧ graded theSitter = 1
          ∧ graded theSwap = 2
          ∧ graded theSitter ≠ graded theSwap
          ∧ (door gateSeat Nat).obs aRed ()
              ≠ (door gateSeat Nat).obs theSitter ())
      ∧ (∀ w₀ : W,
          (∀ x y : (door gateSeat W).State,
              indist (door gateSeat W) x y → x = y) →
          ∀ (t : Nat) (w : W), (t, w) = (t, w₀)) :=
  ⟨fun t _ _ h => the_guest_is_real_and_unread gateSeat t h,
   fun t w v p => the_host_maintains_invisibly gateSeat t w v p,
   ⟨the_sitters_part, fun _ => rfl, rfl⟩,
   fun strat =>
     a_strategy_hears_no_more (door gateSeat Nat) theSitter theSwap
       (fun _ => rfl) strat,
   ⟨fun _ _ _ => rfl, the_graded_reading_parts_the_copies, rfl, rfl,
    the_record_parts_them, the_gate_is_blind_not_broken⟩,
   fun w₀ h => a_door_that_checks_papers_unpersons_its_guests gateSeat w₀ h⟩

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

end Foam.Maps.Counter