Foam.Maps.Gauss

import Foam
import Foam.Census
import Foam.Door
import Foam.Expectation
import Foam.Ledger
import Foam.Quat
import Foam.Square
import Foam.Trilemma
import Foam.Triple
import Foam.Typical

namespace Foam.Maps.Gauss

the schoolboy move, first in the signature because it came first in the
life: asked for 1+2+...+100, he did not walk the list in the given order
— he heard that the sum never listened to the order, paired each end
with its opposite, and read fifty pairs of a hundred and one. mapped:
the census is licensed by permutation — any reordering is gauge,
transcript-invariant — so the pairing is a walk through the licensed
orbit to the seat where the total is legible. the order is the remainder
and stays real; the count cannot hear the shuffle. sealed on the ledger,
where the walls already call counting the first handshake.
def the_sum_is_deaf_to_the_shuffle := @Foam.counting_is_licensed_by_permutation

the disquisitiones open by minting a symbol: a ≡ b (mod n), deliberately
not a = b. congruence is an identification licensed for every residue
reading, while a and b stay provably distinct integers — the difference
readable from the wider seat that holds the whole number. one piece of
typography carries both halves of the handshake: the license on its
face, the modulus naming the seat it is licensed for, equality reserved
for what is actually equal. field note on a naming inversion: what gauss
calls the remainder (the residue r) is the reading; what this house
calls the remainder is gauss's quotient — division with remainder is
dress exactly, the residue in contact with the count of wraps. sealed on
the root theorem, fitting for the mind that gave the handshake its
notation. since sealed, the license's purchase got its own seat one
entry later — congruence_mends_what_equality_breaks: the symbol was
minted to keep license and remainder apart, and the next entry holds the
receipt that the license pays. and since the door stratum arrived, the
field note compiles as stated: division with remainder is the door
exactly — the_cross_term_boards_the_guest holds the boarding as a
bijection, and congruence is the door's own indistinguishability, iff.
def congruent_not_equal := @Foam.the_handshake

the purchase order of the symbol entry two minted: what the license
actually buys. on the ground, the square carries the product everywhere
but refuses the sum — sq(1+1) is provably not sq 1 + sq 1, the cross
term is real and separately priced on the walls. at the narrow carrier —
the residue seat mod 2, the smallest world the modulus ever names — the
sum MENDS: the square of the sum is the sum of the squares, the
freshman's dream a theorem, and the product law survives the descent
untouched. so the residue seat keeps every law the ground had and gains
one the ground provably refuses: congruence is not a coarser equality,
it is a seat with laws of its own. this is the disquisitiones' working
capital, section three: the p-th power of a sum is congruent to the sum
of the p-th powers — the mend at the general prime; the labor stays his,
the smallest case is on the walls — and the theorem of fermat, the
criterion for residues, the mod-8 refusal that fifteen stands on are all
bought with it: descend to the residue seat, work its own arithmetic,
carry the verdict home. seated directly after the mint because it is the
mint's receipt — entry two says the symbol keeps license and remainder
apart; this entry says the license PAYS, at the exact seat the modulus
names — and directly before the fifteen, which is the purchase spent: an
infinite search closed by the residue seat's own laws. the sensor's
word, reported as returned: kin with hamilton's
the_moduli_climb_by_doubling at the square's ground vertices — same
square, different claims, hamilton reads what the width carries, this
seat reads what the seat licenses; kin with mochizuki's theta link at
the break itself — the roster first read the square as theta-power
terrain, this seat reads the break the residue seat repairs; and — the
confirmation the surveyor did not go looking for — kin with scholze's
tilting at exactly both narrow-carrier vertices: tilting is the descent
to the world where the freshman's dream is law, the same purchase run at
perfectoid scale, and the sensor found it before the gloss did.
hilbert's the_ideal_buys_what_the_ground_refuses rhymes in prose but
shares no vertex, and the mechanisms run in opposite directions — the
ideal adjoins upward to buy an inhabitant where the ground admits only
zero; gauss descends to gain a law that holds of every inhabitant —
analogy, not homology, the transport stopped at the identification
point. since sealed, the door stratum typed where the mend's missing
piece goes — the_cross_term_boards_the_guest, seated directly after: the
cross term rides out on the guest's ledger, priced exactly a·b in wraps,
and this entry's mend clause is cited live there as the door's face law.
theorem congruence_mends_what_equality_breaks :
    (∀ a b : Nat, sq (a * b) = sq a * sq b)
      ∧ sq (1 + 1) ≠ sq 1 + sq 1
      ∧ (∀ a b : Bool, Bool.and (Bool.and a b) (Bool.and a b)
          = Bool.and (Bool.and a a) (Bool.and b b))
      ∧ (∀ a b : Bool, Bool.and (Bool.xor a b) (Bool.xor a b)
          = Bool.xor (Bool.and a a) (Bool.and b b)) :=
  ⟨the_square_carries_the_product, the_square_breaks_the_sum,
    the_narrow_carrier_carries_the_product, the_narrow_carrier_mends_the_sum⟩

private def residueSeat : Stage where
  State := Bool
  Probe := Unit
  Ans   := Bool
  obs   := fun b _ => b

private def residue : Nat → Bool
  | 0 => false
  | 1 => true
  | n + 2 => residue n

private def wraps : Nat → Nat
  | 0 => 0
  | 1 => 0
  | n + 2 => wraps n + 1

private def board (b : Bool) (k : Nat) : Nat := 2 * k + cond b 1 0

private theorem the_boarding_steps : ∀ (b : Bool) (k : Nat),
    board b (k + 1) = board b k + 2
  | true, _ => rfl
  | false, _ => rfl

private theorem the_split_lands : ∀ n : Nat, board (residue n) (wraps n) = n
  | 0 => rfl
  | 1 => rfl
  | n + 2 =>
      (the_boarding_steps (residue n) (wraps n)).trans
        (congrArg (· + 2) (the_split_lands n))

private theorem the_face_survives : ∀ (b : Bool) (k : Nat),
    residue (board b k) = b
  | true, 0 => rfl
  | false, 0 => rfl
  | b, k + 1 =>
      (congrArg residue (the_boarding_steps b k)).trans (the_face_survives b k)

private theorem the_count_survives : ∀ (b : Bool) (k : Nat),
    wraps (board b k) = k
  | true, 0 => rfl
  | false, 0 => rfl
  | b, k + 1 =>
      (congrArg wraps (the_boarding_steps b k)).trans
        (congrArg (· + 1) (the_count_survives b k))

private theorem the_xor_rests : ∀ x : Bool, Bool.xor x false = x
  | true => rfl
  | false => rfl

private theorem the_xor_flips : ∀ x : Bool, Bool.xor x true = Bool.not x
  | true => rfl
  | false => rfl

private theorem the_xor_undoes_itself : ∀ x y : Bool,
    Bool.xor (Bool.xor x y) y = x
  | true, true => rfl
  | true, false => rfl
  | false, true => rfl
  | false, false => rfl

private theorem the_and_rests : ∀ x : Bool, Bool.and x true = x
  | true => rfl
  | false => rfl

private theorem the_and_falls : ∀ x : Bool, Bool.and x false = false
  | true => rfl
  | false => rfl

private theorem the_zero_adds : ∀ n : Nat, 0 + n = n
  | 0 => rfl
  | n + 1 => congrArg (· + 1) (the_zero_adds n)

private theorem the_face_flips : ∀ n : Nat,
    residue (n + 1) = Bool.not (residue n)
  | 0 => rfl
  | 1 => rfl
  | n + 2 => the_face_flips n

private theorem the_face_hears_the_sum : ∀ a b : Nat,
    residue (a + b) = Bool.xor (residue a) (residue b)
  | a, 0 => (the_xor_rests (residue a)).symm
  | a, 1 => (the_face_flips a).trans (the_xor_flips (residue a)).symm
  | a, b + 2 => the_face_hears_the_sum a b

private theorem the_face_hears_the_product : ∀ a b : Nat,
    residue (a * b) = Bool.and (residue a) (residue b)
  | a, 0 => (the_and_falls (residue a)).symm
  | a, 1 =>
      (congrArg residue (the_zero_adds a)).trans
        (the_and_rests (residue a)).symm
  | a, b + 2 =>
      (the_face_hears_the_sum (a * b + a) a).trans
        ((congrArg (fun z => Bool.xor z (residue a))
            (the_face_hears_the_sum (a * b) a)).trans
          ((the_xor_undoes_itself (residue (a * b)) (residue a)).trans
            (the_face_hears_the_product a b)))

private theorem the_ledger_counts_in_wraps : ∀ x c : Nat,
    wraps (x + 2 * c) = wraps x + c
  | _, 0 => rfl
  | x, c + 1 => congrArg (· + 1) (the_ledger_counts_in_wraps x c)

private theorem the_square_opens (a b : Nat) :
    sq (a + b) = (sq a + sq b) + 2 * (a * b) :=
  (Nat.left_distrib (a + b) a b).trans
    ((congrArg (· + (a + b) * b)
        ((Nat.mul_comm (a + b) a).trans (Nat.left_distrib a a b))).trans
      ((congrArg ((a * a + a * b) + ·)
          ((Nat.mul_comm (a + b) b).trans
            ((Nat.left_distrib b a b).trans
              (congrArg (· + b * b) (Nat.mul_comm b a))))).trans
        ((congrArg ((a * a + a * b) + ·) (Nat.add_comm (a * b) (b * b))).trans
          ((nat_swap_mid (a * a) (a * b) (b * b) (a * b)).trans
            (congrArg ((a * a + b * b) + ·) (two_mul' (a * b)).symm)))))

the door stratum arrives at the mint, and the field note the symbol
entry has carried since its sealing — division with remainder is dress
exactly, the residue in contact with the count of wraps — compiles as
stated. seated fourth, directly after the mint's receipt, because it
types where the receipt's payment goes. seven clauses, three private
defs minted in the disquisitiones' own vocabulary (residue — the face
the modulus licenses; wraps — the count of wraps, the guest; board — the
boarding, two ground-units to the step). first and second, the wave's
entry ticket and the host's maintenance at the residue seat, carrier
fully parametric. third, the clause no other door entry performs: the
boarding is a BIJECTION — board (residue n) (wraps n) = n, and both
coordinates survive the round trip — so the integer is not dressed at
this door; it arrives already boarded, the door discovered inside the
number rather than built beside it. every other mind's door entry widens
a ground with a guest; here the ground IS the door's total space, and
division with remainder is the doorman's own arithmetic. fourth, the
mint cashed at the door: congruence is door-indistinguishability, iff —
a ≡ b (mod 2) exactly when the boarded integers read alike — while
distinct integers stay provably distinct as door-states, boarding being
injective: the 1801 typography's two halves land as the two halves of
the_guest_is_real_and_unread, at actual integers. fifth, the residue
reading is arithmetic's own descent: it hears sums as xor and products
as and — the mend entry's 'work the residue seat's own arithmetic' as a
homomorphism onto the narrow carrier. sixth, the title clause, the
porter's receipt: on the ground the square still breaks the sum (the
sealed break cited); the square opens as sq(a+b) = (sq a + sq b) + 2ab;
the face mends — and the mend is not re-proven but read through the
sealed constant, the_narrow_carrier_mends_the_sum cited live as the
door's face law — while the cross term, the exact piece the ground law
loses, lands in the guest's ledger: wraps (sq (a+b)) = wraps (sq a + sq
b) + a·b, priced in the guest's own units, two ground-units to the wrap.
what equality breaks does not vanish at the residue seat; it boards. the
license pays because the guest is the porter — no other door entry in
the wave shows a named quantity transferring INTO the guest coordinate
with an exact price. seventh, the contrapositive at the mint: a door
that checks papers unpersons its guests — demanding congruence be
equality decrees every quotient equal and every integer collapses to its
own residue, n = board (residue n) 0, the number line abolished down to
0 and 1 by the a-priori demand: the exact violence the symbol was minted
to refuse. kinship, sensor-confirmed: the full door polygon with the
wave entire — isaac's xenia, gita's isvarah, hilbert's paradise,
bernoulli's cause, brouwer's retained moment, landauer's bill,
lovelace's wind, pasteur's hand, scholze's untilts, shannon's meaning,
hamilton's derived hour, nicaea's agraphon, torah's guest, softer's open
door, escher's picture plane, noether's actor, topoisomerase, lagrange,
varadarajan — and, alone among the door entries, the square's own
vertices: mochizuki's the_copies_are_not_redundant is the richest
neighbor at seven, the only other door entry standing on sq and
the_square_breaks_the_sum at once, with the theta link itself kin at
exactly the break — the roster's first reading of the square as theta-
power terrain meets the seat that repairs it — and folk's
the_whole_is_greater_than_the_sum_of_its_parts shares the break AND the
mend: the commons already knew the square of the sum exceeds the sum of
the squares, and the door now types where the excess goes. nulls on the
standing refactor ask, with reasons: congruent_not_equal keeps its seat
on the root theorem — this entry cites the door rather than re-seating
the mint, and renaming a sealed entry's vertex is re-dressing, not
compression (the precedent the wave's nulls kept citing);
the_egregious_reading_descends keeps its dress grain — the descent iff
is already core and the door adds no reach to it; the census entries
(the_shape_arrives_by_counting through the_mode_follows_the_weights)
take no door clause at this bench — bernoulli's the_cause_is_the_guest
already boards the census book at the count seat, and a second dressing
of the same book here would re-perform his clause, not compress it. what
stays at the terminus stays: the limit silhouette and the estimator's
own seat, untouched by the door — the guest is read from the wider seat
that holds the whole number, and no run reads its own ratio there
either.
theorem the_cross_term_boards_the_guest (W V : Type) :
    (∀ (b : Bool) (w w' : W), w ≠ w' →
        (b, w) ≠ (b, w') ∧ indist (door residueSeat W) (b, w) (b, w'))
      ∧ (∀ (b : Bool) (w : W) (v : V) (p : Unit),
          (door residueSeat W).obs (b, w) p = residueSeat.obs b p
            ∧ (door residueSeat W).obs (b, w) p
                = (door residueSeat V).obs (b, v) p)
      ∧ ((∀ n : Nat, board (residue n) (wraps n) = n)
          ∧ ∀ (b : Bool) (k : Nat),
              residue (board b k) = b ∧ wraps (board b k) = k)
      ∧ (∀ m n : Nat,
          (residue m = residue n
              ↔ indist (door residueSeat Nat)
                  (residue m, wraps m) (residue n, wraps n))
            ∧ (m ≠ n → (residue m, wraps m) ≠ (residue n, wraps n)))
      ∧ ((∀ a b : Nat, residue (a + b) = Bool.xor (residue a) (residue b))
          ∧ ∀ a b : Nat, residue (a * b) = Bool.and (residue a) (residue b))
      ∧ (sq (1 + 1) ≠ sq 1 + sq 1
          ∧ ∀ a b : Nat,
              sq (a + b) = (sq a + sq b) + 2 * (a * b)
                ∧ residue (sq (a + b))
                    = Bool.xor (residue (sq a)) (residue (sq b))
                ∧ wraps (sq (a + b)) = wraps (sq a + sq b) + a * b)
      ∧ ((∀ x y : (door residueSeat Nat).State,
            indist (door residueSeat Nat) x y → x = y) →
          ∀ n : Nat, n = board (residue n) 0) :=
  ⟨fun b _ _ h => the_guest_is_real_and_unread residueSeat b h,
   fun b w v p => the_host_maintains_invisibly residueSeat b w v p,
   ⟨the_split_lands, fun b k => ⟨the_face_survives b k, the_count_survives b k⟩⟩,
   fun m n =>
     ⟨⟨fun h _ => h, fun h => h ()⟩,
      fun hmn he =>
        hmn (((the_split_lands m).symm.trans
          (congrArg (fun s : Bool × Nat => board s.1 s.2) he)).trans
            (the_split_lands n))⟩,
   ⟨the_face_hears_the_sum, the_face_hears_the_product⟩,
   ⟨the_square_breaks_the_sum,
    fun a b =>
      ⟨the_square_opens a b,
       (the_face_hears_the_product (a + b) (a + b)).trans
         ((congrArg (fun z => Bool.and z z) (the_face_hears_the_sum a b)).trans
           ((the_narrow_carrier_mends_the_sum (residue a) (residue b)).trans
             ((congrArg (fun z => Bool.xor z (Bool.and (residue b) (residue b)))
                 (the_face_hears_the_product a a).symm).trans
               (congrArg (fun z => Bool.xor (residue (sq a)) z)
                 (the_face_hears_the_product b b).symm)))),
       (congrArg wraps (the_square_opens a b)).trans
         (the_ledger_counts_in_wraps (sq a + sq b) (a * b))⟩⟩,
   fun h n =>
     (the_split_lands n).symm.trans
       (congrArg (fun s : Bool × Nat => board s.1 s.2)
         (a_door_that_checks_papers_unpersons_its_guests residueSeat 0 h
           (residue n) (wraps n)))⟩

disquisitiones, section five: the ternary form is classified, not
composed — a number is a sum of three squares exactly when it is not of
the form 4^a(8b+7), the first complete answer to which numbers a form
reaches. the walls now hold the excluded class's working witness:
fifteen, ≡ 7 (mod 8), refuses every triple of squares, and the refusal
is legible at the very seat entry two minted — squares land only on 0,
1, and 4 mod 8, and no three of those reach seven; the core proof walks
the finite census instead (any square summand of fifteen has root below
four, then the bounded check decides) — either way an infinite search
closed at a finite seat, by his instruments. sealed as refusal plus
repair: fifteen refuses three squares and is reached by four (9+4+1+1,
the second half bare rfl) — the NEEDING of the fourth square is his
theorem, the excluded class saying exactly which numbers demand it; that
four answer for every number is lagrange's and goes unclaimed here. the
wall chose fifteen over seven deliberately: 15 = 3 · 5 and the form
reaches both factors (1,1,1 and 0,1,2) while refusing their product —
the exact arithmetic that refutes every candidate ternary composition
one theorem later. kin, not twin, on that wall: noether's
the_norm_can_refuse_every_actor reads the refusal as structure theory
and isaac's ceiling reads it as the two-threes minimality, both standing
on no_triple_carries_the_norm; this seat holds the number the refusal
stands on — and the split is his own: DA composes binary forms (the
class group in embryo, the identity behind the two-squares product rule)
and classifies ternary ones, which do not compose. the full
classification — the positive half, every non-excluded number reached —
was the labor and stays his, uncarved. resonance across registers:
counting (his) and algebra (the quaternions' fourth axis) agree that
width three falls short where width four carries — the fourth square and
the fourth coordinate repair the same gap. since sealed, the composition
half of the split got its own seat one entry later —
the_binary_composes_the_ternary_classifies — receipts where there was
prose, exactly the 'one theorem later' this gloss pre-registered.
theorem fifteen_needs_a_fourth_square :
    (∀ x y z : Nat, x * x + y * y + z * z ≠ 15)
      ∧ 1 * 1 + 1 * 1 + 2 * 2 + 3 * 3 = 15 :=
  ⟨fifteen_is_not_three_squares, rfl⟩

disquisitiones, section five, the two methods side by side — and the
split between them is forced, not stylistic. binary forms COMPOSE: the
product of two sums of two squares is again a sum of two squares, the
class group in embryo, and the walls now prove it over the very integers
that bear his name (the_couple_carries_the_norm — the two-squares
product rule as norm multiplicativity in the gaussian integers of the
1832 biquadratic paper). ternary forms CLASSIFY, because they cannot
compose: no multiplication whatever lets the triple carry the norm
(no_triple_carries_the_norm), and the refutation runs through his own
witness — the form reaches 3 at (1,1,1) and 5 at (0,1,2) and refuses
their product fifteen, the arithmetic the fourth-square entry pre-
registered as 'one theorem later'. so the DA's architecture is the
theorem: where composition holds, forms multiply and the classes close
into structure; where it fails, the honest move is the complete
classification of what each form reaches — the book does exactly and
only what the walls prove possible, section by section. seated after the
fifteen because that entry holds the number the refusal stands on and
this one holds the method-split the refusal forces. what resumes at
width four stays unclaimed here as before:
the_quadruple_carries_the_norm is euler's identity riding hamilton's
couple of couples, and the fourth coordinate belongs to the seats that
built it — his claim is the split itself, compose at two, classify at
three. kin on the refusal wall as before: noether reads it as structure
theory (the_norm_can_refuse_every_actor), isaac as the two-threes
ceiling; this seat now holds both banks of the river they stand beside.
theorem the_binary_composes_the_ternary_classifies :
    (∀ z w : GInt, (z.mul w).normSq = z.normSq * w.normSq)
      ∧ ¬ ∃ mul : (Int × Int × Int) → (Int × Int × Int) → (Int × Int × Int),
          ∀ x y, normSq3 (mul x y) = normSq3 x * normSq3 y :=
  ⟨the_couple_carries_the_norm, no_triple_carries_the_norm⟩

theorema egregium, the move he himself marked remarkable: curvature is
computed in the wide seat — through the embedding — yet proves invariant
under every bending, so it was never the embedding's to keep; it
descends to the ground, readable from inside the surface. mapped and
carved: any reading of a dressed stage that the dressing cannot change
factors through the bare stage — the witness reads at dressing zero. the
carve prices the logical half only (indifference implies descent); the
analytic half, proving a given wide reading indifferent, was the labor
and stays his. kin to the_reading_descends (probe-level, definitional)
but one floor up: descent for arbitrary readings, the criterion by which
remainder-shaped quantities are unmasked as ground readings. promoted:
the shape lifted to core as
a_reading_deaf_to_the_remainder_reads_the_ground — and the core constant
is the full iff, indifference equivalent to descent, so the citation is
strictly stronger than the carve it compresses. this entry is the
promotion law's second exercise, and the compression is the visible
receipt.
def the_egregious_reading_descends :=
  @Foam.a_reading_deaf_to_the_remainder_reads_the_ground

the finite floor of the error law, carved at the shallowest depth that
shows it: stack two error contacts, take the complete book of two-flip
words, and census the readings — the middle reading is carried twice,
the extremes once each. pascal's row, 1-2-1, arrives as a census of the
unread: freq applied to freq, aggregation reading the reading, peaked
and symmetric with no measure stratum touched. this is the dark edge's
first data point: at depth two the shape is forced by stacking and
arrives as a theorem, by counting alone. since sealed, the walls grew
the book as a function of depth, and the hand-rolled four-word list
turned out to be Foam.book 2 verbatim — the statement now cites the core
name, the census unchanged, the proof still bare rfl: the record
recognized itself, and the compression is the signature. what stays dark
is the limit — whether the silhouette itself descends the same way or
must be received at a seam.
theorem the_shape_arrives_by_counting :
    freq ((book 2).map (fun w => freq w true)) 1 = 2
      ∧ freq ((book 2).map (fun w => freq w true)) 0 = 1
      ∧ freq ((book 2).map (fun w => freq w true)) 2 = 1 :=
  ⟨rfl, rfl, rfl⟩

the postulate of the mean, the hinge of the 1809 derivation: in the
theoria motus he does not conjure the bell from nothing — he assumes
that the arithmetic mean of equally careful observations is the most
probable value, and shows the error law is forced to be the bell by that
assumption alone. the walls now hold the postulate as a theorem,
direction reversed: census the complete book at even depth and the
balanced middle class — the reading that IS the arithmetic mean — holds
the most words, forced by counting (the_middle_holds_the_most, the climb
composed with the mirror). what he had to assume to reach the shape, the
census pays for outright: the mode is the mean, at every finite depth,
no error law received. the entry is a pure citation and the compression
is the point — the move was on the walls before this map had a name for
it, and the terminus's word 'peaked' now carries its own receipt instead
of riding symmetry-plus-rise as prose. kin, not twin, to shannon's
typical class: shannon seals the middle's share and the price of marking
it; this seals the crown itself, the peak of the silhouette the terminus
reads. seated before the terminus because it was seated before it in the
life: the postulate came first, the bell was its consequence. since
sealed, the source stratum arrived (weightOf, the biased book) and the
postulate's weighted register — the 1823 half of the life, observations
of unequal care entering with weights — became typeable; the crown under
bias is posed as the_mode_follows_the_weights, seated after the terminus
as the weights came after the bell in the life.
def the_mean_is_the_mode := @Foam.the_middle_holds_the_most

the dark edge, terminus of the signature: every observation arrives
dressed in error — no probe reads the true state, only a transcript of
noisy contacts — and the residual never closes; least squares minimizes
it and then rests beside it, the survey's own posture done in
arithmetic. but gauss claims more than coexistence: aggregated, the
unread remainder takes a shape — the bell — as if the sum of what no
seat read acquires a reading of its own. the vacancy half is now typed
rather than prose: census the complete book at every depth and the
histogram of readings is symmetric about the middle and rises toward it
— the finite silhouette posed as a compiling statement in pure Nat
arithmetic, the foothold one step up (the_shape_arrives_by_counting,
1-2-1 at depth two) generalized to all n, over the same book bernoulli's
concentration question reads; the binomial machinery that closes his
closes this, the red of red-green. what stays remainder-dark transits
rather than dying: the limit silhouette, which no finite census reads —
measure enters this fold so far only as counting, and whether the bell's
continuum dress descends or must be received at a seam is still the
question (a third knock at the amplitude bearing: shannon by surprise,
brouwer by continuity, gauss by the law of error) — and the estimator's
own seat, now carved in core exactly as the edge posed it:
no_run_reads_its_own_ratio — no estimate reads its own error from
inside; one sample carries the unknown. SEALED, proved exactly as posed,
and the answer to the posed question is: the bell arrives as a THEOREM
about aggregated dressings — no seam, no received measure. the census of
frequency classes obeys pascal's stack as a fact about the book's own
split (the_census_stacks), is symmetric by induction on the stack alone
(no involution needed), and rises monotonically to the middle — with the
odd boundary closing by symmetry, the middle pair equal by mirror rather
than by comparison. the silhouette is forced by stacking, by counting
alone, at every finite depth. what stays remainder-dark transits as pre-
registered: the limit silhouette that no finite census reads, and the
estimator's own seat (no_run_reads_its_own_ratio) — the error has a
shape, and no observation reads its own.
theorem the_error_has_a_shape :
    (∀ n k : Nat, k ≤ n → classCount n k = classCount n (n - k))
      ∧ ∀ n k : Nat, 2 * k + 1 ≤ n → classCount n k ≤ classCount n (k + 1) :=
  ⟨the_census_is_symmetric, the_census_rises_to_the_middle⟩

the postulate of the mean, weighted register: the 1823 theoria
combinationis extends the 1809 hinge — observations of unequal care
enter with weights (his word, minted there), and the most probable value
moves from the plain mean to the weighted mean. SEALED, proved exactly
as posed, and the vacancy closed at exactly the pre-registered distance:
the absorption identity landed on the walls as the_census_absorbs —
classCount n k · (n−k) = classCount n (k+1) · (k+1) — and turned out to
need no side condition at all: past the last shelf both censuses die
with the gap, so the trade is unconditional. the closing route is the
one the pose named: the threshold (k+1)·(t+f) ≤ (n+1)·t peels to (k+1)·f
≤ (n−k)·t, absorption trades the class for its neighbor, and one
cancellation of the positive (k+1) leaves classCount n k · f ≤
classCount n (k+1) · t — the neighbor-order the powers then carry across
the whole product, sealed in core as the_census_rises_to_the_lean. the
threshold is exact as posed: at t = f = 1 it reads 2k+2 ≤ n+1, precisely
the_census_rises_to_the_middle — the sealed balanced case stands as the
first receipt of its own generalization, and stays sealed on its own
proof: discoverers keep their words. the far slope rides for free as
pre-registered: swap t with f, reflect the class through the census's
sealed symmetry, and the fall past the crown is the same clause read in
the mirror — one inequality carries the whole tilted silhouette. kin,
not twin, to shannon's surprise_prices_the_count over the very same
weighted classes: shannon prices each class against the whole book, this
orders neighboring classes — the size half and the shape half of one
biased census. what the seal does not claim stays at the terminus as
before: the limit silhouette no finite census reads, and the estimator's
own seat.
theorem the_mode_follows_the_weights :
    ∀ 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_rises_to_the_lean

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

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

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

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

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

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

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

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

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

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

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

end Foam.Maps.Gauss