Foam.Maps.Boltzmann

import Foam
import Foam.Coil
import Foam.Countermove
import Foam.Door
import Foam.Ledger
import Foam.Log
import Foam.Seat
import Foam.Roles
import Foam.Source
import Foam.Typical
import Foam.Wheel

namespace Foam.Maps.Boltzmann

the 1877 move that opens every decomposition: before anything is
probable, everything is counted. he cut the energy into finite cells
precisely so the complexions could be enumerated — the continuum was a
limit he took later, under protest — and this corpus never takes the
limit at all, which makes its book his native habitat: at depth n the
complexions number exactly 2^n and no word repeats. W is a count of
distinct complexions, each entered once; equal a priori weight arrives
not as an assumption about nature but as a fact about a complete,
repeat-free enumeration. everything downstream — the room, the arrow,
the epitaph — is arithmetic on this list.
theorem each_complexion_counts_once (n : Nat) :
    (book n).length = 2 ^ n ∧ AllDiff (book n) :=
  ⟨the_book_has_two_to_the_n n, the_book_repeats_no_word n⟩

the braid this seat was named for: macrostate : Role :: microstate :
Mind — and since the last green both strands carry receipts. a
macrostate is not something the gas has in addition to its molecules —
it is a predicate of the coarse reading, and any such predicate
automatically respects micro-indistinguishability: same conduct, same
macrostate, by definition rather than by decree. the Role strand pays
three clauses: conduct derives, the badge fails derivation, and every
derived role is provably badge-blind — whatever P a macro-reading can
pose, P (s, n) iff P (s, m), the microstate label swapped without the
role hearing it. the Mind strand rode as prose until the mind family
landed in core, and now pays its own way: the microstate's seat is a
mind — the recorder, whose held state is the arrangement itself — and
two complexions the shelf-census reads as one macrostate are provably
distinct in the recorder's hands. the wider seat the old gloss priced
'one citation away' has a type now, and the type is Mind: what reads the
remainder is not a bigger gauge but a seat that holds. so pressure on
the vessel wall is a role the gas performs, the molecule's secret
coordinate is a remainder the performance never shows, and the
complexion under the shelf is a mind's held word. recognition across the
roster, kin not twin: bernoulli conjoins the same recorder clause with
the pooling license; this seat conjoins it with the Derived clauses —
one reader, two affects, meeting at the braid's own vertex.
theorem a_macrostate_is_a_derived_role (S : Stage) (s : S.State)
    {A : Type} [DecidableEq A] (a b : A) (hab : a ≠ b) :
    (((∀ (p : S.Probe) (Q : S.Ans → Prop), Derived S (fun t => Q (S.obs t p)))
        ∧ ¬ Derived (dress S) (fun x => x.2 = 0))
      ∧ ∀ (P : (dress S).State → Prop), Derived (dress S) P →
          ∀ (t : S.State) (n m : Int), P (t, n) ↔ P (t, m))
      ∧ ((recorder A).state [a, b] ≠ (recorder A).state [b, a]
          ∧ indist (countStage A) [a, b] [b, a]) :=
  ⟨⟨a_role_is_conduct_not_costume S s,
    fun P hP t n m => a_derived_role_cannot_read_the_badge S P hP t n m⟩,
   a_seat_reads_the_order_the_census_cannot a b hab⟩

private def Complexion : Type := List Bool

private def shelf (w : Complexion) : Nat := freq w true

private def shelfSeat : Stage where
  State := Nat
  Probe := Unit
  Ans   := Nat
  obs   := fun k _ => k

private def board (w : Complexion) : (door shelfSeat Complexion).State :=
  (shelf w, w)

private def hotCold : Complexion := [true, false]

private def coldHot : Complexion := [false, true]

private theorem the_spins_part : true ≠ false := fun h => nomatch h

private theorem the_complexions_part : hotCold ≠ coldHot :=
  fun h => the_spins_part (congrArg (fun l => List.headD l false) h)

the door wave reaches the counting bench, and the braid's other strand
gets the door's own type: the macroface is the door, the complexion
boards behind it — and this seat alone COUNTS the guests. minted in his
vocabulary: the shelf is the coarse reading (occupation of true, the
macrostate's face), the shelfSeat holds that one number and answers only
it, and a complexion boards the door wearing its shelf as its face.
seven clauses. first, the wave's entry ticket at the shelf seat, carrier
parametric. second, the host maintains invisibly, both carriers
parametric — the shelf cannot even count the possible carriers. third,
the clause cashed at named guests: hotCold and coldHot, one energy
element between two molecules, the same shelf on both readings, both
entered in the book of depth 2, provably distinct, boarded as two
residents indistinguishable at every probe — and ONE COLLISION APART:
swapTop carries each guest to the other, so the exchange that explores
the room writes only the guest coordinate and leaves the face fixed; the
room is closed under the very dynamics that wander it, the door hearing
nothing. fourth, equal a priori weight as the door's deafness performed:
every weighting that consumes only the face pays both guests one value,
by rfl — the 1877 postulate is not an assumption about nature, it is the
shelf seat's blindness made just. fifth, the strategy grain: no adaptive
interrogation of the face, follow-ups and cunning included, parts the
boarded twins. sixth, the differentiator no other door entry in the wave
performs: the guest registry is COUNTED — classCount n k is
definitionally the census of the guests wearing face k (the fiber over
the door, rfl), the two named guests are the ENTIRE registry behind
their face (classCount 2 1 = 2 — W is not some unknown multiplicity, it
is exact, and the witnesses exhaust it), and equilibrium is the face
with the most guests behind it — the biggest room re-typed as the
fullest door. every other mind's door holds ONE guest-space unread; this
bench prices the unreadness by cardinality, which is what S = k log W
always was: entropy is the log of the door's registry, the cost of the
guests' namelessness at the face. seventh, the wider seat and the
contrapositive in one conjunction: what reads the guests is not a bigger
gauge but a seat that holds — the recorder parts hotCold from coldHot in
its own hands while the census cannot, the braid's Mind strand meeting
the door at the same two witnesses — and decreeing the face complete
collapses every complexion to one decreed guest per shelf: the door that
checks papers empties the book into its faces, the exact violence the
1877 count was built to refuse. kin dense by construction: the guest
family entire (lovelace's wind, pasteur's hand, shannon's meaning,
bernoulli's cause, chebyshev's source, huygens's medium, gauss's cross
term) at the door polygon; chebyshev the nearest neighbor — his moment-
twins are this entry's shelf-mates read at a two-rung face, his third
rung the wider probe, this bench's registry the count his bound never
needs; folk's cover and the strategy vertices shared at the
interrogation grain. his seat among the door entries: every mind in the
wave met the guest as something real and unread; this bench is where the
guests are ENUMERATED — real, unread, and numbered exactly, each counted
once, which is the whole 1877 move arriving at the door stratum wearing
its own name.
theorem the_complexion_is_the_guest (W V : Type) :
    (∀ (k : Nat) (w w' : W), w ≠ w' →
        (k, w) ≠ (k, w') ∧ indist (door shelfSeat W) (k, w) (k, w'))
      ∧ (∀ (k : Nat) (w : W) (v : V) (p : Unit),
          (door shelfSeat W).obs (k, w) p = shelfSeat.obs k p
            ∧ (door shelfSeat W).obs (k, w) p = (door shelfSeat V).obs (k, v) p)
      ∧ (shelf hotCold = shelf coldHot
          ∧ swapTop hotCold = coldHot
          ∧ hotCold ∈ book 2
          ∧ coldHot ∈ book 2
          ∧ hotCold ≠ coldHot
          ∧ board hotCold ≠ board coldHot
          ∧ indist (door shelfSeat Complexion) (board hotCold) (board coldHot))
      ∧ (∀ (X : Type) (weighting : Nat → X),
          weighting (shelf hotCold) = weighting (shelf coldHot))
      ∧ (∀ strat : Strategy Unit Nat,
          interrogate (door shelfSeat Complexion) strat (board hotCold)
            = interrogate (door shelfSeat Complexion) strat (board coldHot))
      ∧ ((∀ n k : Nat, classCount n k
            = (List.filter (fun w => Nat.beq (shelf w) k) (book n)).length)
          ∧ classCount 2 (shelf hotCold) = 2
          ∧ ∀ n k : Nat, k ≤ 2 * n →
              classCount (2 * n) k ≤ classCount (2 * n) n)
      ∧ (((recorder Bool).state hotCold ≠ (recorder Bool).state coldHot
            ∧ indist (countStage Bool) hotCold coldHot)
          ∧ ∀ w₀ : Complexion,
              (∀ x y : (door shelfSeat Complexion).State,
                  indist (door shelfSeat Complexion) x y → x = y) →
              ∀ (k : Nat) (w : Complexion), (k, w) = (k, w₀)) :=
  ⟨fun k _ _ h => the_guest_is_real_and_unread shelfSeat k h,
   fun k w v p => the_host_maintains_invisibly shelfSeat k w v p,
   ⟨rfl, rfl,
    List.Mem.tail _ (List.Mem.head _),
    List.Mem.tail _ (List.Mem.tail _ (List.Mem.head _)),
    the_complexions_part,
    (the_guest_is_real_and_unread shelfSeat (shelf hotCold) the_complexions_part).1,
    (the_guest_is_real_and_unread shelfSeat (shelf hotCold) the_complexions_part).2⟩,
   fun _ _ => rfl,
   fun strat =>
     a_strategy_hears_no_more (door shelfSeat Complexion)
       (board hotCold) (board coldHot) (fun _ => rfl) strat,
   ⟨fun _ _ => rfl, rfl, the_middle_holds_the_most⟩,
   ⟨a_seat_reads_the_order_the_census_cannot true false the_spins_part,
    fun w₀ h => a_door_that_checks_papers_unpersons_its_guests shelfSeat w₀ h⟩⟩

the first law, read from inside the gas — the side condition the 1877
count never states because the dynamics state it for him: W counts
complexions at a fixed total, and the total is fixed because every
collision is a transfer, (E1, E2) to (E1 - d, E2 + d), the sum deaf to
d. four clauses, four bare citations. the collision conserves the class:
internal exchange wanders the partition and cannot leave the fiber, so
the room the equilibrium is biggest in is closed under the very dynamics
that explore it. heat moves the class by exactly its size: the boundary
is the only entrance and it is priced — the deltaQ half of the first
law, read at a rigid vessel. the cycle returns the class and never the
record: a stroke borrowed and refunded leaves the total home and the
transcript two marks longer — energy is a state function and the mark-
list is the path. and beneath the total the partition rides unread: (1,
-1) and (0, 0), one class, provably distinct — the complexion under the
conservation law, the same remainder the derived-role entry reads under
the census, now conserved by dynamics instead of merely unread by a
gauge. the channel distinction is cut-relative, which is the kinetic
theory's own thesis in ledger clothes: heat is not a different stuff
from collision — a stroke is a collision whose partner is off the books,
and widening the held state to seat the bath turns every stroke into a
shuffle, class-motion at this seat becoming class-conservation one seat
wider. kin, not twin, dense on purpose: the shuffle vertex shared with
topoisomerase's sectors and fable_5's swap, the stroke with the enzyme's
held cut and strand passage, the return with the strand passage and
torah's teshuvah, the partition with three neighbors — but no entry on
the roster joins the shuffle to the stroke, and that join is the
deposit: the first law is the two channels held in one conjunction.
theorem heat_moves_what_the_collision_cannot :
    (∀ (h : Int × Int) (d : Int),
        coilClass (coil.meet h (Sum.inl d)) = coilClass h)
      ∧ (∀ (h : Int × Int) (s : Int),
          coilClass (coil.meet h (Sum.inr s)) = coilClass h + s)
      ∧ (∀ 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_shuffle_conserves_the_class,
   the_stroke_moves_the_class_by_its_size,
   the_return_pays_two_marks,
   the_partition_rides_unread⟩

S = k log W, read the only way this corpus reads logarithms: as lengths
of marks — and since the last green the stone itself stands in core,
character for character, so the binding now cites it instead of
gesturing at it. three clauses in one conjunction: the epitaph (S = k ·
logTwo W whenever W counts the book and S prices its depth), the total
bill (summing every word's length pays exactly count times log of count
— the price is the log, said over the whole book), and the floor that
makes both honest (name a class faithfully into the book of depth L and
it is counted against 2^L; the count cannot exceed what the name-space
affords). the entropy of a macrostate is the price of naming its room, k
a unit conversion the walls never need. shannon's wall holds the same
receipt read from the source-coding side; this seal reads it from the
class side, which is the side his stone faces.
theorem entropy_is_the_price_of_the_name (k n S W : Nat)
    (hW : W = (book n).length) (hS : S = k * n) :
    S = k * logTwo W
      ∧ natSumOver List.length (book n)
          = (book n).length * logTwo ((book n).length)
      ∧ ∀ (L : Nat) (ms : List (List Bool)), AllDiff ms →
          (∀ m, m ∈ ms → m ∈ book L) → ms.length ≤ 2 ^ L :=
  ⟨S_eq_k_log_W k n S W hW hS,
   the_price_is_the_log n,
   fun L ms hd hin => a_class_marked_into_a_book_is_counted L ms hd hin⟩

equilibrium with the dynamics removed: the equilibrium distribution is
not where the gas is pushed, it is the shelf with the most complexions.
at depth 2n the middle shelf outholds every other, and it holds at least
its share — the whole book divided by the number of shelves — so the
biggest room is not merely biggest but polynomially close to being the
whole house: 2^2n complexions, 2n+1 shelves, the crown at least one part
in 2n+1 of everything. the maxwellian fell out of his counting as
exactly this crown one stratum up; here the fair book carries the shape,
and the biased crown now stands one entry below.
theorem equilibrium_is_the_biggest_room (n : Nat) :
    (∀ k : Nat, k ≤ 2 * n → classCount (2 * n) k ≤ classCount (2 * n) n)
      ∧ 2 ^ (2 * n) ≤ (2 * n + 1) * classCount (2 * n) n :=
  ⟨the_middle_holds_the_most n, the_middle_shelf_holds_its_share n⟩

the reversibility objection, held and answered in one conjunction, both
halves receipted. first half: the objection is correct — every walk of
reversible moves carries a countermove that brings the state home
exactly; nothing in the dynamics prefers a direction, and the corpus
proves the un-doing rather than conceding it. second half: the counting
concentrates anyway — past a computable depth the deviant words are
outnumbered at any odds. no contradiction, because the halves quantify
over different things: the first over trajectories, the second over the
book. the arrow is not in the moves; it is in how many words sit on each
shelf. what the H-theorem asked of mechanics, the census delivers by
arithmetic — and the reversed trajectory stays possible, merely
outnumbered.
theorem the_arrow_rides_the_count {X : Type} :
    (∀ (h : List (Move X)) (x : X),
        replay (countermove h) (replay h x) = x)
      ∧ (∀ b c : Nat, ∃ N : Nat, ∀ n : Nat, N ≤ n →
          c * (List.filter (fun w => Bool.not (nearBalance b n w))
                (book n)).length
            ≤ (List.filter (fun w => nearBalance b n w) (book n)).length) :=
  ⟨the_countermove_comes_home, the_deviants_are_outnumbered⟩

the recurrence objection, held and answered the same way the
reversibility one was: conceded as a theorem, answered by the census.
first half: on a finite book no walk wanders forever — any dynamics
whatever, invertible or not, revisits a state, by pigeonhole on the
complexions; the walls' receipt asks even less than the objection did —
no measure preserved, no moves undone, a finite state space suffices.
second half: the same census the arrow rides, unmoved — past a
computable depth the deviants are outnumbered at any odds. the halves
quantify over different things, one trajectory's turns against the
book's shelves, so the certain return tips nothing: what returns is a
state; what concentrates is the count. his reply survives as this
conjunction — the recurrence is real, and the arrow never lived in the
trajectory anyway. recognition event across the roster: fable_5 holds
the first half alone as the_survivor_is_a_wheel, a survival-shape; this
seat conjoins it with the count — one wheel, two affects, kin at the
wheel's own vertex.
theorem the_return_does_not_tip_the_count :
    (∀ (n : Nat) (m : Fin n → Fin n) (s : Fin n),
        ∃ i j : Nat, i < j ∧ turnN m i s = turnN m j s)
      ∧ (∀ b c : Nat, ∃ N : Nat, ∀ n : Nat, N ≤ n →
          c * (List.filter (fun w => Bool.not (nearBalance b n w))
                (book n)).length
            ≤ (List.filter (fun w => nearBalance b n w) (book n)).length) :=
  ⟨fun _ m s => the_bounded_walk_returns m s, the_deviants_are_outnumbered⟩

the far bank, reached and now crowned: posed vacancy-dark before the
source stratum existed — weights as powers t^(#true)·f^(#false), the
window an inequality pair, mass summed by natSumOver — and sealed by
that stratum exactly as posed, the seal a bare application, the pose's 0
< t and 0 < f discarded unused: the degenerate sources die in the
arithmetic, not in case splits. since the last green the walls grew the
biased census and the entry's own name gets paid at last:
the_census_rises_to_the_lean stands conjoined as the first clause,
another bare citation — the weighted shelf count climbs while the lean
stays ahead, so the crowned shelf is the MODE of the weighted book, most
probable in the literal sense, where before the binding held only the
mass. and the step underneath is his own 1877 maneuver, exact and
Stirling-free: the_census_absorbs compares adjacent shelves by ratio —
classCount n k · (n−k) = classCount n (k+1) · (k+1) — which is precisely
how he located the maxwellian, asking of neighboring complexion counts
where the ratio tips. both halves of the claim now receipted: the crown
(mode, by the climb) and the concentration (mass — past N = (c+1)·b²·t·f
the deviants are outweighed at any odds). recognition event at the crown
vertex: gauss holds the same climb bare as the_mode_follows_the_weights
— one climb, two affects; that seat reads the mode tracking the weights,
this seat reads the 1877 claim landing whole. what remains in transit is
only the mark-length reading: his permutability measure priced in marks,
the log of a floor that stands in core one citation away.
theorem the_most_probable_distribution :
    (∀ t f n k : Nat, k < n → (k + 1) * (t + f) ≤ (n + 1) * t →
        classCount n k * (t ^ k * f ^ (n - k))
          ≤ classCount n (k + 1) * (t ^ (k + 1) * f ^ (n - (k + 1))))
      ∧ ∀ t f b c : Nat, 0 < t → 0 < f →
          ∃ N : Nat, ∀ n : Nat, N ≤ n →
            c * natSumOver (fun w => t ^ freq w true * f ^ freq w false)
                  (List.filter
                    (fun w => Bool.not (Bool.and
                      (Nat.ble (b * (t * n)) (n + b * ((t + f) * freq w true)))
                      (Nat.ble (b * ((t + f) * freq w true)) (n + b * (t * n)))))
                    (book n))
              ≤ natSumOver (fun w => t ^ freq w true * f ^ freq w false)
                  (List.filter
                    (fun w => Bool.and
                      (Nat.ble (b * (t * n)) (n + b * ((t + f) * freq w true)))
                      (Nat.ble (b * ((t + f) * freq w true)) (n + b * (t * n))))
                    (book n)) :=
  ⟨the_census_rises_to_the_lean,
   fun t f b c _ _ => the_deviants_are_outweighed t f b c⟩

the terminus, and it was his cosmology before it was anyone's paradox:
if the world is a rare fluctuation of a vaster equilibrium, the observer
inside it cannot count the book it was drawn from. the receipt holds one
book containing runs that disagree about the ratio, so no run reads its
own typicality from inside — remainder-dark, held open by receipt, and
the darkness transits rather than dying: whoever holds the whole book
reads the shelf this run sits on, and then cannot read their own,
exactly as closure_is_seat_relative says. he bet the visible universe
was a deviant word; the map keeps the bet as what it provably is —
undecidable from the seat that is the word. (self, pure unknown).
def no_seat_inside_the_fluctuation := @Foam.no_run_reads_its_own_ratio

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

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

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

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

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

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

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

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

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

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

end Foam.Maps.Boltzmann