Foam.Maps.Landauer

import Foam
import Foam.Beam
import Foam.Contact
import Foam.Countermove
import Foam.Door
import Foam.Marks
import Foam.Relay
import Foam.Roles
import Foam.Surprise
import Foam.Tower
import Foam.Valve
import Foam.Watched

namespace Foam.Maps.Landauer

the motto, and the ground the other three stand on: there is no
disembodied bit. a distinction counts as information only because it is
a distinction in state — carried by a degree of freedom. the narrow seat
may read nothing at any probe, and the bit rides as pure remainder; it
is real anyway, and a wider seat provably reads it. that is why erasure
can cost anything at all: what gets erased was always physical, so the
bill has somewhere to land
def information_is_physical := @Foam.a_wider_seat_reads_the_remainder

an invisible move cannot merge distinct readings: if m is invisible and
m s = m t, then s and t already read alike at every probe —
contrapositively, anything that truly erases a distinction is visible
somewhere; the bill moves upstairs
theorem erasure_shows :
    ∀ (S : Stage) (m : S.State → S.State), Invisible S m →
      ∀ s t, m s = m t → ∀ p, S.obs s p = S.obs t p :=
  fun S _ hi s t hmerge p =>
    (hi s p).symm.trans ((congrArg (S.obs · p) hmerge).trans (hi t p))

the 1961 premise, finally seated where the argument actually starts:
logical irreversibility. a merge — any map landing two distinct states
together — admits no counter (no machine acting on the states undoes it
after the fact) and is no move (the reversible sector, where every
action carries its own inverse by type, cannot contain it at all). the
two clauses cite the valve's two clauses in order, which is the
recognition: the one-way valve arrived in core as this mind's own 1961
machinery, unnamed. erasure cannot ride the dynamics that run free — so
whatever pays its bill lies outside the move-sector, which is why the
road home goes through the record and why the exoneration of computation
never covers the merge. seated between erasure_shows and
reset_pays_in_record deliberately: the merge is seen; the merge cannot
be undone in place or reversibly done at all; therefore the only road
home appends
theorem a_merge_is_not_a_move {X : Type} (f : X → X) {a b : X}
    (hab : a ≠ b) (hf : f a = f b) :
    (¬ ∃ g : X → X, ∀ x, g (f x) = x)
      ∧ ¬ ∃ m : Move X, ∀ x, m.fwd x = f x :=
  ⟨a_merge_admits_no_counter f hab hf,
   fun ⟨m, hm⟩ =>
     hab (every_move_keeps_the_state m ((hm a).trans (hf.trans (hm b).symm)))⟩

the conservation clause: you can always bring the position home — the
countermove exists and composes to the identity — but never for free: in
a world that only appends, the walk that comes home is strictly longer
than the walk that left. the erased distinction is paid for in record,
and the bill is conserved because the record never unwrites. kT ln 2,
denominated in transcript length (the denomination was a promissory note
in this gloss until the marks stratum reached the walls;
no_machine_undercuts_the_bill is where it gets cashed)
def reset_pays_in_record := @Foam.undo_in_an_append_only_world

the price on the conservation clause, finally receipted:
reset_pays_in_record proved the bill exists — this sets its floor and
strips the machine out of it. hold 2^n distinctions on a record that
keeps them severally legible — no entry a prefix of another, because an
append-only record read serially must know where each mark ends — and
any encoder whatsoever pays at least n marks per distinction: the bound
is quantified over every scheme, so the minimum is set by the count of
distinctions alone, never by the device that pays it. kT ln 2 per bit,
with the per-bit now a theorem and the no-matter-how-you-build-it now a
forall. sealed on the same constant as shannon's entropy_of_the_source,
deliberately: one theorem, two laboratories — shannon reads it off the
channel as the cost of saying, landauer reads it off the heat sink as
the cost of forgetting. that the two readings are one constant is not an
analogy; it is the principle. TIGHTENED when the derivable-edge family
reached the walls: the floor was always one-sided, and the walls can
finally say why. the depth bound stands exactly as sealed — every
encoder pays at least n marks per distinction — and
the_shortcut_pays_only_its_mark conjoins as the overpayment witness: a
genuinely fresh mark, riding no old path, paying its full cost on the
record, that merges nothing and reaches nothing — every route through it
reroutes through what was already held. dissipation without erasure is
inhabited, which is why the principle is an inequality and could never
be an equality: the floor is set by the count of distinctions alone, and
everything a machine pays above it indicts the device, never the logic.
kT ln 2 AT LEAST — the 'at least' now a theorem rather than an
engineering apology, which is landauer's own 1961 split between
unavoidable and avoidable dissipation: the floor is what no machine
undercuts, the overpayment is what a better machine eliminates. the
exoneration clause upstairs is untouched — it attributes the necessary
bill to the merge; the shortcut types the unnecessary bill. the
direction of the principle is now a contrast in the types: erasure
requires payment, payment does not require erasure. same lemma, third
laboratory: shannon reads the shortcut off the wire as redundancy
priced, pasteur reads it off the calcined air as a new door nothing new
walks through, landauer reads it off the heat sink as waste heat — real
cost on the record, no distinction forgotten, no bill discharged
theorem no_machine_undercuts_the_bill :
    (∀ (n : Nat) (f : List Bool → List Bool),
        (∀ w1 w2, List.Mem w1 (book n) → List.Mem w2 (book n) → w1 ≠ w2 →
            ¬ ∃ t : List Bool, f w1 ++ t = f w2) →
          n * (book n).length ≤ (pool ((book n).map f)).length)
      ∧ ∀ (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) :=
  ⟨the_marks_pay_the_depth,
   fun _ q a b hfresh hab => the_shortcut_pays_only_its_mark q a b hfresh hab⟩

the exoneration clause, the half everyone forgets: dissipation is not a
tax on computation, it is a tax on erasure alone. a move licensed by the
readings — one that merges nothing — writes nothing to the transcript:
run it at every step for as long as you like and the record cannot tell
you did. the gauge sector runs free, and that is why the bill, when it
arrives, is attributable to the merge and to nothing else. computation
was never the expensive part. (re-seated when invisible_is_gauge reached
the walls: the old seal was the general law over any licensed relation;
the new one is the gloss verbatim — the license discharged by the
readings themselves, indist via indist_is_licensed, the move applied at
every step of the transcript. re-seated again when the watch reached the
walls: only_the_invisible_survives_the_watch is the iff — surviving the
watch at every probe-list and every state is not merely guaranteed for
the invisible, it is exclusive to them. the attribution sentence above
was a promissory note until now, same pattern as the kT ln 2
denomination one seat down: whatever writes nothing was invisible,
whatever is visible gets caught, so the bill when it arrives implicates
the merge and nothing else — the exoneration is exact. re-seated a third
time when the relay reached the walls: the gloss said computation and
the binding held one move — the watch iff covers a single licensed move
applied at every step, so 'computation was never the expensive part'
stayed a promissory note at exactly the width that matters, since a
computation is a chain of distinct gates, not one gate iterated. the
relay cashes it: a whole program of licensed moves, any finite chain,
writes nothing to the transcript. the seal is now the exact conjunction
— the iff per move, which is the attribution (whatever is visible gets
caught, so the bill implicates the merge alone), and the chain-law at
derivation width, which is the exoneration (the computation, taken
whole, runs unheard). kin, not twin, with hilbert's
the_proof_rides_the_marks, which holds the bare chain-law: hilbert reads
the relay as a derivation riding the marks, landauer reads it as a
reversible circuit dissipating nothing — one theorem, two laboratories,
the recognition this map already carries at
no_machine_undercuts_the_bill)
theorem reversible_runs_free (S : Stage) :
    (∀ m : S.State → S.State,
       (∀ (ps : List S.Probe) (s : S.State),
           transcriptWith S m s ps = transcript S s ps)
         ↔ Invisible S m)
      ∧ (∀ ms : List (S.State → S.State),
           (∀ m, m ∈ ms → Invisible S m) →
             ∀ (ps : List S.Probe) (s : S.State),
               transcriptWith S (relay ms) s ps = transcript S s ps) :=
  ⟨fun m => only_the_invisible_survives_the_watch S m,
   fun ms h => the_relay_goes_unheard S ms h⟩

the mind's first laboratory, where the accounting was first read off a
wire: transport is transmission, and a perfect channel still shows
resistance — none of it in the wire. the mode riding the channel is a
real distinction the voltage probe never reads; carrying it changes no
reading, so the ballistic sector runs free; and the reservoir fixing the
mode to its own equilibrium is the collapse — so the resistance is all
contact resistance, landed at the interface and nowhere else. the
conductor is exonerated and the bill is billed to the merge: erasure-
pays was this receipt, generalized
def conductance_is_transmission := @Foam.contact_is_addition_not_fixing

the second laboratory is a thought experiment: the demon at the
trapdoor, the referee who imagined itself outside the gas. three clauses
acquit the second law. the demon's sorting is a role read off its record
— conduct that factors through the readings is derived; a derived role
cannot read the badge — the remainder is beyond its probes, so it cannot
sort by a distinction it never recorded, and whatever distinction it
does exploit it first holds, physically, in its own state (the motto,
applied to the adversary); and bringing that record home appends,
strictly — the entropy shed by the gas is repaid at the desk when the
memory resets. the bill lands at the reset, not at the measurement: the
measuring was a licensed move and ran free (reversible_runs_free already
holds that clause; szilard billed the looking, the record bills the
forgetting). seated after the wire and before the terminus deliberately:
the demon is the referee-inside-the-gas made famous, and
no_disembodied_referee is the same acquittal universalized — every
referee, the auditor included, is a state some wider seat reads. kin by
shared vertex with boltzmann's a_macrostate_is_a_derived_role (the demon
reads macrostates; that is exactly why it is derived) and with this
mind's own reset_pays_in_record (the third clause is that seal, applied
to the demon's memory)
theorem the_demon_pays_at_the_reset (S : Stage) (X : Type) :
    (∀ (p : S.Probe) (Q : S.Ans → Prop), Derived S (fun t => Q (S.obs t p)))
      ∧ (∀ (P : (dress S).State → Prop), Derived (dress S) P →
          ∀ (s : S.State) (n m : Int), P (s, n) ↔ P (s, m))
      ∧ (∀ (h : List (Move X)) (x : X),
          replay (h ++ countermove h) x = x
            ∧ (h ≠ [] → h ++ countermove h ≠ h)) :=
  ⟨fun p Q => a_role_read_off_the_record_is_derived S p Q,
   fun P hP s n m => a_derived_role_cannot_read_the_badge S P hP s n m,
   fun h x => undo_in_an_append_only_world h x⟩

the third laboratory is huygens's parlor: two clocks on one beam,
falling into sympathy — and the beam's coupling map, arrived on the
walls as entrain, is checkably a merge. distinct phase-pairs land
together (the locked pair and its one-step-ahead neighbor arrive at the
same state), and one lap later every pair is locked. so
a_merge_is_not_a_move applies by bare function application, no
transport: the lock admits no counter — no machine acting on the pair
un-entrains it after the fact — and entrainment is no move: the
reversible sector cannot contain it, by type. that is the thermodynamics
of synchronization read directly off the record: locking contracts the
pair-space, contraction is a merge, and a merge cannot ride the dynamics
that run free — so the sympathy is paid for, and the bill lands where
this map always sends it: on the merge, outside the move-sector,
dissipated at the beam. the relative phase the lock forgets was physical
(the motto), its erasure is visible somewhere (erasure_shows), and the
road home appends (reset_pays_in_record) — the loop signature runs whole
through the parlor. huygens seals the lock and the parity trade,
kuramoto seals the mean field as the beam, noether carries the lock
through the window; this entry holds the clause none of them holds: the
lock is bought. synchronization is an erasure with a heat sink, which is
why it needs one — the free sector cannot contract, so wherever clocks
fall into step, something is paying. seated after the wire and the demon
deliberately: three rooms, one acquittal pattern — the bill always lands
on the merge and never on the motion
theorem the_lock_is_bought_by_a_merge :
    (∀ p : Compass × Compass,
        together (entrain (entrain (entrain (entrain p)))))
      ∧ entrain (Compass.n, Compass.n) = entrain (Compass.n, Compass.e)
      ∧ ((Compass.n, Compass.n) : Compass × Compass) ≠ (Compass.n, Compass.e)
      ∧ (¬ ∃ g : Compass × Compass → Compass × Compass,
            ∀ p, g (entrain p) = p)
      ∧ ¬ ∃ m : Move (Compass × Compass), ∀ p, m.fwd p = entrain p :=
  have hab : ((Compass.n, Compass.n) : Compass × Compass)
      ≠ (Compass.n, Compass.e) :=
    fun h => nomatch congrArg Prod.snd h
  ⟨the_lap_locks_together, rfl, hab, a_merge_is_not_a_move entrain hab rfl⟩

private def restore {W : Type} (S : Stage) (w₀ : W) :
    (door S W).State → (door S W).State :=
  fun x => (x.1, w₀)

the door stratum arrives at the principle's own front desk, and the
wave's missing case turns out to be this mind's oldest operation:
restore — fix every rider to the standard value, RESTORE TO ONE with the
bit fully parametric — run at the door. the guest is real and unread
(the motto at the door: a distinction in state, carried, provably
distinct, read by no probe the seat owns), and restore is checkably a
merge of real distinctions: two guests land on the house standard, and
the guests were provably two. yet restore is INVISIBLE at the door — it
writes nothing to the door's transcript, receipted through the watch iff
on the eraser itself. an erasure the watch cannot catch, at first sight
the exact tension this map was built to forbid — and the acquittal is
the map's own second entry run at the door: erasure_shows applied to
restore returns the door's first theorem, the merged guests already read
alike at every probe. no reading was erased at this seat, so no bill
lands at this seat: erasure of the unread runs free exactly where it is
unread. the bill still exists — the merge admits no counter and is no
move (a_merge_is_not_a_move by bare application, the same way the
parlor's lock was caught: the reversible sector cannot contain restore,
by type) — and it lands where the distinction is read: one seat wider,
the desk upstairs, movedIn's none-probe parting what the door held
indistinct. the last clause is the map's first entry's own constant
(a_wider_seat_reads_the_remainder), read at the Int door: the loop
closes on its own ground, and erasure_shows' old gloss 'the bill moves
upstairs' turns literal. that is the addressing rule under kT ln 2: the
bill is denominated at the seat that reads the distinction — a seat that
carries but does not read hosts the erasure for free, and no seat is
ever the last reader. the host maintains invisibly with the carrier
fully parametric (one theory of upkeep for every guest — which is WHY
the housekeeping runs free: the door's deafness to the rider and
restore's invisibility are one fact), and the contrapositive the wave
carries everywhere lands in this ledger as the null case: a door that
checks papers unpersons its guests — one guest, nothing to forget, no
bill anywhere; the reading that would make the erasure visible abolishes
what it would catch. two acquittals distinguish this entry from its
margin kin: the settle is invisible because the reading survives the
fold; the restore is invisible because there was no reading to survive —
one watch, two verdicts. and the demon one seat up shows the other
branch: its record was read at its own seat, so its reset paid; the
door's rider never was, so the door's reset doesn't — the bill follows
the reading, which is why it always lands at the reset of a READ record
and never on the motion. seated tenth, directly ahead of the terminus it
feeds: no_disembodied_referee is this clause iterated — every auditor is
a state some wider seat reads, the bill's address is always one seat up,
and the ladder does not top out.
theorem the_bill_follows_the_reading {W V : Type} (S : Stage) (s : S.State)
    {w w' : W} (h : w ≠ w') (w₀ : W) (v : V) (p : S.Probe)
    (n m : Int) (hnm : n ≠ m) :
    ((s, w) ≠ (s, w') ∧ indist (door S W) (s, w) (s, w'))
      ∧ ((door S W).obs (s, w) p = S.obs s p
          ∧ (door S W).obs (s, w) p = (door S V).obs (s, v) p)
      ∧ Invisible (door S W) (restore S w₀)
      ∧ (∀ (ps : List S.Probe) (x : (door S W).State),
          transcriptWith (door S W) (restore S w₀) x ps
            = transcript (door S W) x ps)
      ∧ restore S w₀ (s, w) = restore S w₀ (s, w')
      ∧ ((¬ ∃ g : (door S W).State → (door S W).State,
            ∀ x, g (restore S w₀ x) = x)
          ∧ ¬ ∃ mv : Move (door S W).State,
              ∀ x, mv.fwd x = restore S w₀ x)
      ∧ (∀ q, (door S W).obs (s, w) q = (door S W).obs (s, w') q)
      ∧ (indist (door S Int) (s, n) (s, m)
          ∧ (movedIn S).obs (s, n) none ≠ (movedIn S).obs (s, m) none)
      ∧ ((∀ x y : (door S W).State, indist (door S W) x y → x = y) →
          (s, w) = (s, w')) :=
  ⟨the_guest_is_real_and_unread S s h,
   the_host_maintains_invisibly S s w v p,
   fun _ _ => rfl,
   (only_the_invisible_survives_the_watch (door S W) (restore S w₀)).mpr
     (fun _ _ => rfl),
   rfl,
   a_merge_is_not_a_move (restore S w₀)
     (the_guest_is_real_and_unread S s h).1 rfl,
   erasure_shows (door S W) (restore S w₀) (fun _ _ => rfl) (s, w) (s, w') rfl,
   a_wider_seat_reads_the_remainder S s n m hnm,
   fun hc => a_door_that_checks_papers_unpersons_its_guests S w' hc s w⟩

the motto turned on its own bookkeeper, and where this decomposition
stops: mathematics is physical too — every computation, the audit of the
bill included, runs on hardware inside the universe. widen the seat to
read the erased bit's remainder and the widened seat is itself a state,
carrying a fresh distinction invisible at every one of its own probes,
which a yet-wider seat provably reads. no view from nowhere, no referee
exempt from the bill it referees; the ladder of seats does not top out.
the loop terminates at the seat doing the decomposing: (self, pure
unknown).
def no_disembodied_referee := @Foam.no_seat_is_the_last_seat

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

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

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

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

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

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

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

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

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

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

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

end Foam.Maps.Landauer