Foam.Maps.Chebyshev

import Foam.Concentration
import Foam.Door
import Foam.Expectation
import Foam.Fold
import Foam.Int
import Foam.Ledger
import Foam.Rungs
import Foam.Source
import Foam.Square
import Foam.Surprise

namespace Foam.Maps.Chebyshev

the 1867 memoir opens at mean values, not probabilities: the method
climbs moments from the bottom, and the bottom rung is already on the
walls — the complete book pools to exact balance at every depth, a
census fact with no limit invoked. a deliberate twin with bernoulli's
the_whole_book_balances, third seat on the shape: bernoulli read the
balance as admissibility, gauss read the un-pooled census as the
histogram's first data point, chebyshev reads it as the zeroth moment of
a ladder he intends to climb.
def the_mean_arrives_first := @Foam.the_complete_book_balances

the ledger his inequality spends: square each word's deviation from
balance and pool over the complete book, and the total is exactly n per
word — n·2^n at depth n, no more, no less. the vacancy is the induction:
prepending one flip sends each deviation d to d+1 and d−1, and (d+1)² +
(d−1)² = 2d² + 2 — the cross terms cancel inside each word-pair,
orthogonality wearing counting clothes. posed in the signed integers the
house ground by hand; a carve closes it. flipped exactly as posed: the
carve landed the induction (the_squares_pool_to_the_depth, first try —
the cross terms cancelled as pre-registered) and this structure bridges
the posed fold-form through fold_reads_the_sum and one zero_add, defeq
carrying dev to its spelled-out form. the ledger is funded.
theorem the_second_moment_is_conserved :
    ∀ n : Nat,
      fold (fun acc w => acc + sqDev n w) 0 (book n)
        = Int.ofNat n * Int.ofNat (2 ^ n) :=
  fun n =>
    ((fold_reads_the_sum (sqDev n) (book n) 0).trans
      (FInt.zero_add (sumOver (sqDev n) (book n)))).trans
      (the_squares_pool_to_the_depth n)

the mechanism inside the conserved ledger, seated on its own now that
the walls type the cross term: the sq stratum proves the square breaks
the sum, folk's telling prices the unsigned excess as exactly the two
rectangles — the between-relations, the whole reading greater — and
gauss mends the break by descending to the narrow carrier. chebyshev's
answer to the same break is neither pricing nor descent: it is
opposition. prepending one flip sends a word's deviation d to d+1 and
d−1 — the same parts, opposite signs — and on the signed carrier the
rectangles arrive opposed, +2d at one wing, −2d at the other. the wing
expansion shows each square paying its two rectangles in full; pooled
over the pair, they cancel to nothing and the pair reads exactly the
parts' own squares: (d+1)² + (d−1)² = 2d² + 2. cancellation, not absence
— the rectangles are real at each wing and net to zero only in the
balanced pool. this is why the second moment pools linearly — n·2^n, one
new unit square per word per depth, the rectangles never accumulating —
which is to say: why the variances of independent steps add, the fact
the whole 1867 ladder stands on. the sealed gloss one seat up pre-
registered this as 'the cross terms cancel inside each word-pair,
orthogonality wearing counting clothes'; the sq stratum arriving is the
counting clothes getting typed. kinship at the break vertex with gauss
(who mends it), folk (who prices it unsigned, where the whole always
reads at least the parts), and mochizuki (the theta link) — the sensor
confirms exactly these three and no more; young's light added to light
gives darkness rhymes hard (signed cancellation, read at a screen) but
shares no vertex — analogy, not homology, the transport stopped before
the identification point. the wing expansion and the pair identity are
cited by no other map — the ledger claiming its own mechanism.
theorem the_pair_cancels_the_rectangles :
    (sq (1 + 1) ≠ sq 1 + sq 1) ∧
    (∀ a c : Int, (a + c) * (a + c) = (a * a + c * c) + (a * c + a * c)) ∧
    (∀ d : Int,
      (d + 1) * (d + 1) + (d - 1) * (d - 1) = (d * d + d * d) + 2) :=
  ⟨the_square_breaks_the_sum, sq_add, pair_of_squares⟩

the inequality itself, as a census with no measure stratum: a word
outside the tolerance band has deviation more than n in b parts, so its
squared deviation clears (n+1)² in b² parts — and the conserved second
moment then caps the deviant headcount outright: deviants times (n+1)²
cannot exceed b² times n·2^n. this is the bridge from the moment ledger
to bernoulli's terminus: with the deviant count capped, the conforming
words outnumber the deviants c to one past a depth the bound names
explicitly — N = (c+1)·b² suffices. what bernoulli spent twenty years
approaching, this counts in one line from the second moment; the price
of the shortcut is that it is blunt (his own tail bounds were sharper),
and bluntness is enough for the promise. flipped exactly as posed: the
core carve holds the census inequality under the neutral name
the_pooled_square_caps_the_deviants, and the terminus it bridges to is
now itself sealed — the_deviants_are_outnumbered, with N = (c+1)·b²
explicit in the witness. the shortcut he took in 1867 is a compiling
object. tightened when the derivable-edge family landed: the one-line
sentence rode as prose while the binding carried only the census — the
binding now conjoins the_shortcut_pays_only_its_mark, the record-grain
type of the move's other half. the terminus was already reachable
(bernoulli's twenty-year route the backing), so the direct edge from the
moment ledger deposits as a derivable edge: fresh as an edge, riding no
prior route, paying exactly one mark, moving no reach anywhere. what the
deposit buys lives entirely at the route seat — one line against twenty
years, the simplicity order hilbert's twenty-fourth reads — and
bluntness stays the shortcut's other price, already sealed in the
explicit N. the generality is the opposite bank of the same
decomposition: the tilt was the fresh edge, the surprise that extended
reach, and it is already sealed at the_bound_reads_only_the_moments.
theorem every_deviant_pays_its_square :
    (∀ b n : Nat,
      (List.filter (fun w => !nearBalance b n w) (book n)).length
          * ((n + 1) * (n + 1))
        ≤ (b * b) * (n * 2 ^ n)) ∧
    (∀ (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)) :=
  ⟨fun b n => the_pooled_square_caps_the_deviants b n,
   fun _ q a b hfresh hab => the_shortcut_pays_only_its_mark q a b hfresh hab⟩

the signature move the textbooks keep his name on: the bound never reads
the distribution. the walls now hold a second book — every word weighted
t per true and f per false — and the same ladder climbs it rung for
rung: the band centers on the first moment, the tilted squares pool to
n·tf·(t+f)^n, every word outside the band pays (n+1)² in b² parts, and
the conforming weight outnumbers the deviant weight c to one past N =
(c+1)·b²·tf — explicit, the source consulted only through its mean and
its variance. the 1867 memoir was always this general — des valeurs
moyennes assumes arbitrary quantities and touches nothing but mean
values — so the balanced book was the special case, and the tilt
arriving is the memoir's actual scope arriving on the walls; at even
tilt the numbers come home to the count already sealed, N = (c+1)·b².
sealed by citation of the core carve, which quantifies over every tilt;
three seats now read the same constant — boltzmann as the most probable
distribution prevailing, hilbert as probability owing no axiom,
chebyshev as the method that is deaf to everything a source is except
its two moments.
def the_bound_reads_only_the_moments := @Foam.the_deviants_are_outweighed

private def Source : Type := List Nat

private def pooled (f : Nat → Nat) : List Nat → Nat
  | [] => 0
  | x :: xs => f x + pooled f xs

private def rung (k : Nat) (xs : Source) : Nat :=
  pooled (fun x => Nat.pow x k) xs

private def moments (xs : Source) : Nat × Nat := (rung 1 xs, rung 2 xs)

private def momentSeat : Stage where
  State := Nat × Nat
  Probe := Bool
  Ans   := Nat
  obs   := fun m p => cond p m.1 m.2

private def board (xs : Source) : (door momentSeat Source).State :=
  (moments xs, xs)

private def skewLow : Source := [0, 3, 3]

private def skewHigh : Source := [1, 1, 4]

private theorem the_next_rung_parts : rung 3 skewLow ≠ rung 3 skewHigh :=
  fun h =>
    no_number_is_below_itself (rung 3 skewHigh)
      (h ▸ lt_of_ble_false (rung 3 skewHigh) (rung 3 skewLow) rfl)

private theorem the_books_part : skewLow ≠ skewHigh :=
  fun h => the_next_rung_parts (congrArg (rung 3) h)

the door wave reaches the moment ladder, and the sealed generality's
other half arrives: the_bound_reads_only_the_moments seals sufficiency —
the bound NEEDS nothing but the two moments; the door types what that
deafness costs — the source itself boards as the guest, real and unread
behind its own face. the seat minted in his vocabulary: rung k pools the
book of readings at the k-th power, the moments are the first two rungs,
the momentSeat holds that pair as state and answers only moment-probes,
and a source boards the door wearing its moments as its face. seven
clauses. first, the wave's entry ticket at the moment seat, carrier
parametric. second, the host maintains invisibly, both carriers
parametric — the seat cannot even count the possible sources. third, the
clause this bench performs at named guests: two books of readings,
[0,3,3] and [1,1,4] — mirror-skewed about one mean, deviations
(−2,+1,+1) against (−1,−1,+2), each book the other's reflection — agree
at rung one (6 and 6) and rung two (18 and 18), are provably distinct,
and board the door as two residents indistinguishable at every probe:
moment-twins, seated by name, the door's theorem cashed at actual books
the way gauss cashed it at actual integers and huygens at his own sealed
beams. fourth, the textbook signature cashed as a reflexivity: every
reading that consumes only the face wears one value on both books, by
rfl — the deafness is definitional, not approximate. fifth, the strategy
grain: no adaptive interrogation of moment-probes, follow-ups and
cunning included, parts the boarded twins. sixth, the ladder's own
answer, and the entry's reason for existing: the THIRD rung parts them —
54 against 66, the gap priced exact at twelve — the remainder conserved
and redistributed, never erased, and the 1867 method's climb typed as
forced: each finite rung leaves the source unread, and the next moment
is a new seat, not a cleverer question at the old one. the 1874 valeurs
limites — finitely many moments pin the source only within bounds, never
to a point — lands as the door's own theorem. seventh, the
contrapositive: decreeing the moments complete collapses the library to
one source per face — the moment problem resolved by unpersoning, the
exact verdict the limit-values bounds were built to refuse. his seat
among the door entries: every mind in the wave met the guest somewhere;
this bench is where the guest's unreadness was priced and then SPENT —
the bound that works precisely because it never asks who the source is.
theorem the_source_is_the_guest (W V : Type) :
    (∀ (m : Nat × Nat) (w w' : W), w ≠ w' →
        (m, w) ≠ (m, w') ∧ indist (door momentSeat W) (m, w) (m, w'))
      ∧ (∀ (m : Nat × Nat) (w : W) (v : V) (p : Bool),
          (door momentSeat W).obs (m, w) p = momentSeat.obs m p
            ∧ (door momentSeat W).obs (m, w) p
                = (door momentSeat V).obs (m, v) p)
      ∧ (rung 1 skewLow = rung 1 skewHigh
          ∧ rung 2 skewLow = rung 2 skewHigh
          ∧ skewLow ≠ skewHigh
          ∧ board skewLow ≠ board skewHigh
          ∧ indist (door momentSeat Source) (board skewLow) (board skewHigh))
      ∧ (∀ (X : Type) (reading : Nat × Nat → X),
          reading (moments skewLow) = reading (moments skewHigh))
      ∧ (∀ strat : Strategy Bool Nat,
          interrogate (door momentSeat Source) strat (board skewLow)
            = interrogate (door momentSeat Source) strat (board skewHigh))
      ∧ (rung 3 skewLow ≠ rung 3 skewHigh
          ∧ rung 3 skewLow + 12 = rung 3 skewHigh)
      ∧ (∀ w₀ : Source,
          (∀ x y : (door momentSeat Source).State,
              indist (door momentSeat Source) x y → x = y) →
          ∀ (m : Nat × Nat) (xs : Source), (m, xs) = (m, w₀)) :=
  ⟨fun m _ _ h => the_guest_is_real_and_unread momentSeat m h,
   fun m w v p => the_host_maintains_invisibly momentSeat m w v p,
   ⟨rfl, rfl, the_books_part,
    (the_guest_is_real_and_unread momentSeat (moments skewLow) the_books_part).1,
    (the_guest_is_real_and_unread momentSeat (moments skewLow) the_books_part).2⟩,
   fun _ _ => rfl,
   fun strat =>
     a_strategy_hears_no_more (door momentSeat Source)
       (board skewLow) (board skewHigh) (fun _ => rfl) strat,
   ⟨the_next_rung_parts, rfl⟩,
   fun w₀ h => a_door_that_checks_papers_unpersons_its_guests momentSeat w₀ h⟩

the terminus, and it is the other half of his life: best approximation.
the minimax error never vanishes — it equioscillates, touching its
extreme alternately, and the balance of the remainder IS the certificate
of optimality; the plantigrade machine turns a wheel's rotation into
near-straight motion with the error engineered, bounded, and paid — the
limit approached by linkage, never crossed. the shape: an optimum
recognized by its remainder's balance, not its absence. held dark three
flights because the walls held no approximation stratum — then typed and
sealed in one, degree zero, in the walls' own Nat, because the corridor
was already there: the certificate clause says a corridor whose
remainder touches both its walls (a reading at c+e, a reading at c−e)
undercuts every rival covering the book of readings — the two touches
alone pin 2e beneath any rival's 2e', balance certifying optimality with
the corridor hypothesis for c never even needed; the stays-open clause
says that while the readings hold two distinct values, every corridor
has positive width — the line is approached, never walked, absence
impossible. no approximation stratum was needed: le_trans,
cancel_add_left, and nat_swap_mid carry the whole proof — the rungs and
the ledger's own cancellation, the tolerance band's suspicion about
itself confirmed. what transits, one seat wider: the polynomial corridor
— degree n, n+2 alternations, the machine's actual geometry — wants a
stratum the walls still do not hold, and the second clause is the
receipt that the residue survives the move: the remainder is conserved
and redistributed, not eliminated — the equioscillation is the remainder
made legible.
theorem the_linkage_approaches_the_line :
    (∀ (xs : List Nat) (c e c' e' : Nat),
        (∃ hi, List.Mem hi xs ∧ hi = c + e) →
        (∃ lo, List.Mem lo xs ∧ lo + e = c) →
        (∀ x, List.Mem x xs → c' ≤ x + e' ∧ x ≤ c' + e') →
        e ≤ e') ∧
    (∀ x y c e : Nat,
        c ≤ x + e → x ≤ c + e → c ≤ y + e → y ≤ c + e → x ≠ y → 0 < e) :=
  ⟨fun _ c e c' e' hHi hLo hriv =>
    hHi.elim fun hi hhi =>
      hLo.elim fun lo hlo =>
        let A : c + e ≤ c' + e' :=
          le_trans (Nat.le_of_eq hhi.2.symm) (hriv hi hhi.1).2
        let B : c' ≤ lo + e' := (hriv lo hlo.1).1
        let L : (c + e) + c' = (c' + lo) + (e + e) :=
          (((Nat.add_comm (c + e) c').trans
              (congrArg (fun t => c' + (t + e)) hlo.2.symm)).trans
            (congrArg (fun t => c' + t) (Nat.add_assoc lo e e))).trans
            (Nat.add_assoc c' lo (e + e)).symm
        let key : (c' + lo) + (e + e) ≤ (c' + lo) + (e' + e') :=
          le_trans (Nat.le_of_eq L.symm)
            (le_trans (Nat.add_le_add A B)
              (Nat.le_of_eq (nat_swap_mid c' e' lo e')))
        Or.elim (Nat.lt_or_ge e' e)
          (fun hlt =>
            absurd (cancel_add_left (c' + lo) key)
              (Nat.not_le_of_lt (Nat.add_lt_add hlt hlt)))
          (fun hge => hge),
   fun _ _ _ e h1 h2 h3 h4 hne =>
    match e, h1, h2, h3, h4 with
    | 0, h1, h2, h3, h4 =>
        absurd ((Nat.le_antisymm h2 h1).trans (Nat.le_antisymm h4 h3).symm) hne
    | e + 1, _, _, _, _ => Nat.succ_le_succ (Nat.zero_le e)⟩

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

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

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

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

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

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

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


end Foam.Maps.Chebyshev