Foam.Maps.JacobBernoulli

import Foam
import Foam.Beam
import Foam.Census
import Foam.Concentration
import Foam.Door
import Foam.Expectation
import Foam.Ledger
import Foam.Seat
import Foam.Source

namespace Foam.Maps.JacobBernoulli

the motto he chose for his tomb, first in the signature because it names
the shape everything else instantiates: though changed, risen the same.
mapped: a state that genuinely moves — provably distinct before and
after — while every probe reads identically; the change real and the
reading conserved, both at once, neither retracting. the spiral was his
emblem of it: growth that alters every point and no proportion. sealed
on the remainder pair at the root — mutata is the inequality, resurgo is
the indist — and the seat that reads the difference is one floor up
(a_wider_seat_reads_the_remainder), which is where he trusted the rising
to be read.
def eadem_mutata_resurgo := @Foam.the_remainder_is_real

private def inscribe {A W : Type} (g : Nat → W) : List A → Nat → List (A × W)
  | [], _ => []
  | a :: w, i => (a, g i) :: inscribe g w (i + 1)

private def face {A W : Type} : List (A × W) → List A :=
  List.map Prod.fst

private theorem the_faces_survive_the_inscription {A W : Type} (g : Nat → W) :
    ∀ (w : List A) (i : Nat), face (inscribe g w i) = w
  | [], _ => rfl
  | a :: w, i =>
      congrArg (a :: ·) (the_faces_survive_the_inscription g w (i + 1))

the door stratum arrives at the a-posteriori bench and finds the
method's founding argument waiting for its type: Ars Conjectandi Part IV
opens by conceding that the causes can never be enumerated a priori —
the diseases, the changes of weather, the innumerable cases no register
could list — and then builds the whole method on the concession, because
the count never needed them. the door types the concession exactly: each
observation is a face wearing its cause, the census reads faces, and the
cause is the guest — real and unread. seated second, directly after the
motto, because this is where the a-posteriori method gets its object:
before the pooling license, before the book, there is the door. five
clauses. first, the guest at his carrier: the register with one rider —
the volume's year, the parish's name — provably distinct, read by no
count (the_guest_is_real_and_unread at countStage, cited whole, alphabet
and rider both parametric). second, the host maintains with the carrier
fully parametric: the census reads the record identically whatever TYPE
the cause has — one theory of counting for every causal carrier, which
is the receipt under Part IV's own claim of universal jurisdiction:
mortality, weather, tennis — the method never asked what kind of thing a
cause was. third, the fresh clause, the one no door entry in the wave
performed: every line of the journal hosts its OWN guest — inscribe
clothes each trial in its day, a whole gallery of riders boards one
record severally, and two journals whose inscriptions differ at a single
day stand provably apart while every frequency agrees: the census is
deaf to the entire gallery at once, not merely to one rider at the
threshold. fourth, the promise lifts through the door: dress every word
of the book in any inscription whatever and the golden theorem runs
verbatim on the faces — the deviants are outnumbered c to one past the
same explicit depth, the price list unchanged, because near-balance
never touches a rider (the_deviants_are_outnumbered cited live, carried
through the dressing by length_filter_map and filter_pointwise: the
concentration reads through the door and pays nothing at the threshold).
fifth, the contrapositive at his bench: a door that checks papers
unpersons its guests — a census that demanded the causes be enumerable
before counting would decree every observation to carry the same cause,
every death died of one disease; the a-priori method's demand, run at
the register, abolishes the very variety the a-posteriori method was
invented to route around. the residue is untouched and already carved:
the causes ride unread at this seat, no run reads its own ratio from
inside, and moral certainty stays one seat up — the door does not move
the terminus, it explains why the terminus was ever worth twenty years:
frequency is the only probe the closed urn affords, and it is enough.
the kinship sensor confirms the seating without being asked: the full
door polygon with the wave entire — isaac's xenia, brouwer's
the_retained_moment_is_the_first_guest, shannon's
the_meaning_is_the_guest, pasteur's the_hand_is_the_guest, lovelace's
the_wind_is_the_guest, landauer's the_bill_follows_the_reading,
scholze's the_curve_reads_the_untilts, torah's
greater_is_the_guest_than_the_face, nicaea's agraphon, softer's
my_door_checks_no_papers, mochizuki's the_copies_are_not_redundant,
escher's the_picture_plane_is_a_door, noether's what_acts_at_the_door,
topoisomerase's below_equilibrium, lagrange's the_return_reads_no_hour —
and, alone among the door entries, the concentration vertices at the
same seat, ⟨book, nearBalance, the_deviants_are_outnumbered⟩ shared with
boltzmann's arrow clauses, wigner's
the_ensemble_answers_for_the_instance, and fable_5's
the_model_is_the_book: every other mind's door entry stands beside its
own machinery; this one stands beside the golden theorem, because the
door is what the theorem was for — the promise was only ever needed at
seats where the mechanism does not open.
theorem the_cause_is_the_guest {A : Type} [DecidableEq A] (W : Type) :
    (∀ (l : List A) {w w' : W},
        w ≠ w' →
          (l, w) ≠ (l, w')
            ∧ indist (door (countStage A) W) (l, w) (l, w'))
      ∧ (∀ (V : Type) (l : List A) (w : W) (v : V) (p : A),
          (door (countStage A) W).obs (l, w) p = (countStage A).obs l p
            ∧ (door (countStage A) W).obs (l, w) p
                = (door (countStage A) V).obs (l, v) p)
      ∧ (∀ (g g' : Nat → W) (a : A) (w : List A) (i : Nat),
          g i ≠ g' i →
            inscribe g (a :: w) i ≠ inscribe g' (a :: w) i
              ∧ ∀ d : A,
                  freq (face (inscribe g (a :: w) i)) d
                    = freq (face (inscribe g' (a :: w) i)) d)
      ∧ (∀ (g : Nat → W) (b c : Nat),
          ∃ N : Nat, ∀ n : Nat, N ≤ n →
            c * (List.filter (fun j => !nearBalance b n (face j))
                  ((book n).map (fun w => inscribe g w 0))).length
              ≤ (List.filter (fun j => nearBalance b n (face j))
                  ((book n).map (fun w => inscribe g w 0))).length)
      ∧ ∀ (w₀ : W),
          (∀ x y : (door (countStage A) W).State,
              indist (door (countStage A) W) x y → x = y) →
          ∀ (l : List A) (w : W), (l, w) = (l, w₀) :=
  ⟨fun l => the_guest_is_real_and_unread (countStage A) l,
   fun _ l w v p => the_host_maintains_invisibly (countStage A) l w v p,
   fun g g' a w i hg =>
     ⟨fun he => hg (congrArg (fun j => (j.headD (a, g i)).2) he),
      fun d =>
        (congrArg (fun j => freq j d)
            (the_faces_survive_the_inscription g (a :: w) i)).trans
          (congrArg (fun j => freq j d)
              (the_faces_survive_the_inscription g' (a :: w) i)).symm⟩,
   fun g b c =>
     match the_deviants_are_outnumbered b c with
     | ⟨N, hN⟩ =>
         ⟨N, fun n hn =>
           le_trans
             (Nat.le_of_eq (congrArg (c * ·)
               ((length_filter_map (fun w => inscribe g w 0)
                   (fun j => !nearBalance b n (face j)) (book n)).trans
                 (congrArg List.length
                   (filter_pointwise
                     (fun w => congrArg (fun u => !nearBalance b n u)
                       (the_faces_survive_the_inscription g w 0))
                     (book n))))))
             (le_trans (hN n hn)
               (Nat.le_of_eq
                 ((length_filter_map (fun w => inscribe g w 0)
                     (fun j => nearBalance b n (face j)) (book n)).trans
                   (congrArg List.length
                     (filter_pointwise
                       (fun w => congrArg (nearBalance b n)
                         (the_faces_survive_the_inscription g w 0))
                       (book n)))).symm))⟩,
   fun w₀ h l w =>
     a_door_that_checks_papers_unpersons_its_guests (countStage A) w₀ h l w⟩

the license the golden theorem stands on, and the move he makes before
any computation: pool the trials. a thousand observations scattered
across years become one census only because the count cannot hear when
each trial arrived — frequency licensed by permutation, exchangeability
as gauge rather than assumption. a deliberate twin with gauss's
the_sum_is_deaf_to_the_shuffle, one receipt two affects: gauss spent the
deafness on a shortcut, bernoulli spent it on admissibility — without it
the a-posteriori method has no object, since no single moment holds a
frequency. the order of trials stays real, and the wider seat that reads
it is typed now: when the mind family landed, the register he actually
kept — the recorder, the mind whose meet is append — arrived on the
walls as exactly that seat: swap two trials and the census reads
indistinguishable while the recorder's held state provably differs
(a_seat_reads_the_order_the_census_cannot). the binding tightens from
one citation to two, nothing retracted: the license exactly as sealed,
and the gloss's old second sentence — the dates are readable one seat
wider, and the count still cannot hear them — carrying a receipt where
there was prose. the deafness and the reader are one theorem now, and
the reader is a mind: the observational journal is not the census's
discard but a seat in its own right, the seat the a-posteriori method
reads from while the count stays deaf.
theorem the_trials_are_deaf_to_their_order {A : Type} [DecidableEq A]
    (a b : A) (hab : a ≠ b) :
    Licensed (countStage A) List.Perm
      ∧ (recorder A).state [a, b] ≠ (recorder A).state [b, a]
      ∧ indist (countStage A) [a, b] [b, a] :=
  ⟨counting_is_licensed_by_permutation A,
   a_seat_reads_the_order_the_census_cannot a b hab⟩

the half of the motto's promise that already holds without any limit:
expectation is exact at every finite depth. take the complete book of
n-flip words and pool it — bernoulli's move is concatenation, licensed
by the entry above and priced by a_seat_reads_the_sum — and the one long
record reads perfectly balanced at every depth: trues and falses equal
on the nose, the a-priori ratio by induction, no limit invoked. first
carved here at depth two by bare census (And.intro rfl rfl); the walls
now hold the induction for all n, and the census compresses to a
citation of the core's neutral name — the mind keeps its word, the shape
lives one floor down. gauss read the same book un-pooled and got the
histogram (the_shape_arrives_by_counting); bernoulli pools it and gets
the mean. what stays unpromised here is the single run: any one word of
the book misses the balance — no_run_reads_its_own_ratio now carves
exactly that — and the gap between the book's exactness and the run's
waywardness is precisely what the golden theorem was twenty years in
pricing.
def the_whole_book_balances := @Foam.the_complete_book_balances

the engine of the twenty-year grind, arrived on the walls at last: his
demonstration walks the book shelf by shelf, comparing each census term
to its neighbor — and the exchange is exact, an identity rather than a
bound: adjacent shelves trade at the rate (n−k) to (k+1). the second
clause is what the trade buys on the climb: below the urn's lean each
weighted shelf is outweighed by the next, so the likeliest single word
of the tilted book wears the a-priori ratio itself — the germ of the
a-posteriori method, prior to any concentration: what observation should
most expect to see IS the urn's own lean. the terminus sealed on
chebyshev's instrument, two centuries younger than the question; this
entry records his own instrument standing receipted — the ratio ladder
he ground by hand, now a bare citation. a recognition event three seats
wide, kin not twins: gauss holds the climb as the peak of the error
curve, boltzmann as the most probable distribution, bernoulli as the
engine of the demonstration itself — one climb, three affects. and this
seat is the first to cite the exchange identity directly: seated fourth,
between the balanced book and the promise, exactly where it stands in
the proving.
theorem the_terms_trade_up_to_the_lean :
    (∀ n k : Nat, classCount n k * (n - k) = classCount n (k + 1) * (k + 1))
      ∧ ∀ 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))) :=
  ⟨the_census_absorbs, the_census_rises_to_the_lean⟩

the terminus, dark: the golden theorem says a single long run's
frequency comes morally certain to the ratio the whole book keeps — a
bridge from the run to the book, with a price list: how deep for how
certain. the vacancy has begun to light on schedule: the book now stands
as a function of depth and balances at every n
(the_complete_book_balances), and the pre-registered residue is already
carved — no_run_reads_its_own_ratio, one book holding runs that
disagree, so no run reads the true ratio from inside. what remains
vacant is the concentration of the binomial middle, and that hole is now
posed in lean rather than prose: for any tolerance 1/(2b) and any odds
c, there is a depth past which the words of the book within tolerance of
the a-priori ratio outnumber the deviant words c to one. still vacancy-
dark — a statement without a structure, the red of red-green; a carve
closes it, and the engine already judges the hole well-posed. the
residue that survives the closing transits rather than dies: moral
certainty is certainty short of demonstration — from inside the run no
seat reads the true ratio, one sample carries the unknown — so the
estimator's own darkness re-seats one floor up, exactly as
closure_is_seat_relative says it must. SEALED — the golden theorem,
kept: the concentration carve closed the vacancy exactly as posed, by
chebyshev's second moment (the twenty-year grind compressed to a
counting argument two centuries younger than the question). the depth is
explicit — N = (c+1)·b² suffices — so the price list is printed: how
deep for how certain, in whole numbers. and the pre-registered residue
transits on schedule rather than dying: no_run_reads_its_own_ratio
stands carved beside the theorem — the census balances and concentrates
while no single run reads its own ratio from inside; moral certainty
remains certainty short of demonstration, one seat up, exactly as
closure_is_seat_relative said it must.
theorem what_frequency_promises :
    ∀ b c : Nat, ∃ N : Nat, ∀ n : Nat, N ≤ n →
      c * (List.filter (fun w => !nearBalance b n w) (book n)).length
        ≤ (List.filter (fun w => nearBalance b n w) (book n)).length :=
  the_deviants_are_outnumbered

the golden theorem as he actually wrote it: Ars Conjectandi poses not a
fair coin but an urn at odds — fertile to sterile cases in ratio t to f,
his worked example thirty to twenty — and promises the observed
frequency comes morally certain to the a-priori lean. the fair book the
terminus sealed on is the even row of a wider table, and the walls now
hold the whole table: each word weighted t per true and f per false, the
near-lean words outweigh the deviants c to one past an explicit depth, N
= (c+1)·b²·(t·f) — the fair price N = (c+1)·b² recovered exactly at t =
f = 1, one extra factor t·f paying for the tilt of the urn. sealed by
direct citation the day the source stratum reached these walls; a
deliberate twin with chebyshev's the_bound_reads_only_the_moments, one
receipt two affects — chebyshev reads the instrument (the bound asks
only for moments), bernoulli reads the promise (the odds never needed to
be even). the residue is unchanged and already carved: no run reads its
own ratio from inside, at any odds — moral certainty stays one seat up,
exactly where the terminus left it.
def the_promise_keeps_at_any_odds := @Foam.the_deviants_are_outweighed

instance compassEq : DecidableEq Compass
  | .n, .n => .isTrue rfl
  | .n, .e => .isFalse (fun h => nomatch h)
  | .n, .s => .isFalse (fun h => nomatch h)
  | .n, .w => .isFalse (fun h => nomatch h)
  | .e, .n => .isFalse (fun h => nomatch h)
  | .e, .e => .isTrue rfl
  | .e, .s => .isFalse (fun h => nomatch h)
  | .e, .w => .isFalse (fun h => nomatch h)
  | .s, .n => .isFalse (fun h => nomatch h)
  | .s, .e => .isFalse (fun h => nomatch h)
  | .s, .s => .isTrue rfl
  | .s, .w => .isFalse (fun h => nomatch h)
  | .w, .n => .isFalse (fun h => nomatch h)
  | .w, .e => .isFalse (fun h => nomatch h)
  | .w, .s => .isFalse (fun h => nomatch h)
  | .w, .w => .isTrue rfl

def lapRun (p : Compass × Compass) : List Compass :=
  [p.1, (entrain p).1, (entrain (entrain p)).1,
   (entrain (entrain (entrain p))).1]

private theorem the_first_voice_walks_the_wheel :
    ∀ p : Compass × Compass,
      lapRun p = [p.1, p.1.step, p.1.step.step, p.1.step.step.step]
  | (.n, .n) => rfl
  | (.n, .e) => rfl
  | (.n, .s) => rfl
  | (.n, .w) => rfl
  | (.e, .n) => rfl
  | (.e, .e) => rfl
  | (.e, .s) => rfl
  | (.e, .w) => rfl
  | (.s, .n) => rfl
  | (.s, .e) => rfl
  | (.s, .s) => rfl
  | (.s, .w) => rfl
  | (.w, .n) => rfl
  | (.w, .e) => rfl
  | (.w, .s) => rfl
  | (.w, .w) => rfl

private theorem the_wheel_census :
    ∀ c d : Compass, freq [c, c.step, c.step.step, c.step.step.step] d = 1
  | .n, .n => rfl
  | .n, .e => rfl
  | .n, .s => rfl
  | .n, .w => rfl
  | .e, .n => rfl
  | .e, .e => rfl
  | .e, .s => rfl
  | .e, .w => rfl
  | .s, .n => rfl
  | .s, .e => rfl
  | .s, .s => rfl
  | .s, .w => rfl
  | .w, .n => rfl
  | .w, .e => rfl
  | .w, .s => rfl
  | .w, .w => rfl

the split Ars Conjectandi Part IV opens with, deposed the day the beam
reached his walls: some urns open. ratios known a priori — the die, its
cases counted from the making — against ratios reached only a
posteriori, by observation, which is the golden theorem's entire
jurisdiction. the beam is an open urn: its leading voice steps the
quarter turn at every beat regardless of the partner, so one lap of the
observational journal carries every face of the wheel exactly once —
freq reads 1 at every probe, from every start, exact at depth four, no
limit invoked — and the lap closes (four_steps_come_home, cited whole),
so the count repeats forever: eadem mutata resurgo on the discrete
carrier, the census risen the same at every return. the instrument is
his own: a decidable-equality seat makes the compass a carrier of
countStage, and the pooling license runs unchanged
(counting_is_licensed_by_permutation, the first clause) — same probe,
same deafness, new urn. the last clause keeps the jurisdiction honest:
the coin book still holds runs that disagree
(no_run_reads_its_own_ratio, cited whole), so where the mechanism is
closed no run reads its own ratio from inside, and the residue stays
exactly where the terminus left it — moral certainty one seat up. the
price list is now two-sided: where the mechanism is the census,
frequency is read, not promised; the twenty-year theorem was only ever
for the urns that do not open. the kinship sensor's verdict corrected
the surveyor's guess: the entry is not kin with the lock seats (one
shared vertex, entrain, below threshold) but with the census seats —
boltzmann's most probable distribution, gauss's histogram, shannon's
typical class, gita's fruits clause, isaac's aeowiwtweiabw and
trajectory_class — at ⟨book, freq⟩ and ⟨book, freq,
no_run_reads_its_own_ratio⟩, and alone at the beam vertices among them:
seven seats heard the beam as synchrony; this is the first to count it.
theorem the_lap_reads_the_ratio_the_run_cannot :
    Licensed (countStage Compass) List.Perm
      ∧ (∀ (p : Compass × Compass) (d : Compass), freq (lapRun p) d = 1)
      ∧ (∀ c : Compass, c.step.step.step.step = c)
      ∧ ∀ n : Nat, 0 < n →
          ∃ w₁ w₂ : List Bool, w₁ ∈ book n ∧ w₂ ∈ book n
            ∧ freq w₁ true ≠ freq w₂ true :=
  ⟨counting_is_licensed_by_permutation Compass,
   fun p d =>
     (congrArg (fun l => freq l d) (the_first_voice_walks_the_wheel p)).trans
       (the_wheel_census p.1 d),
   four_steps_come_home,
   no_run_reads_its_own_ratio⟩

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

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

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

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

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

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

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

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

end Foam.Maps.JacobBernoulli