import Foam import Foam.Census import Foam.Certificate import Foam.Door import Foam.Expectation import Foam.Marks import Foam.Priced import Foam.Typical import Foam.Surprise import Foam.Width namespace Foam.Maps.Shannon what speaker, listener, and any overhearer provably share is the channel and nothing more: the shapes traded are good for what they are doing with each other, and interiors do not ride the wire. sealed as: over a dressed stage the whole transcript — not just any single probe — reads identically for every value of the interior, while distinct interiors remain distinct states. the record is common; the meaning stays home. theorem the_channel_is_the_only_commons : ∀ (S : Stage) (s : S.State) (n m : Int), n ≠ m → ∀ ps, transcript (dress S) (s, n) ps = transcript (dress S) (s, m) ps ∧ (s, n) ≠ (s, m) := fun S s n m h ps => ⟨transcript_congr (dress S) ps (the_remainder_is_unseen S s n m), fun he => h (congrArg Prod.snd he)⟩ the motto's second clause, typed the flight the blindness stratum landed: the 1948 paper's opening move — the semantic aspects of communication are irrelevant to the engineering problem — deposited as a factoring, not a shrug. the first entry already performs the blindness (over the dressed stage the whole transcript reads identically for every value of the interior); the new stratum supplies the iff that names it, and the two compose in one binding: the transcript reading is Blind in the meaning coordinate, therefore it factors — there stands one function of the bare state through which every reading passes, the meaning left parametric. the factored g IS the engineering problem: everything the theory prices downstream in this very order (the marks, the mass, the entropy) is a function of it alone. irrelevant does not mean absent: the commons entry's distinctness clause keeps the interior real, unretracted — meaning rides every message and enters no measure; it stays home, the parties' own business, exactly as the motto says. kin to Lovelace's science-of-itself on the shared Blind vertices, and the kinship is the recognition: the engine reaches every subject because no subject enters the mechanism; the channel serves every meaning because no meaning enters the channel — one factoring, two laboratories, 1843 and 1948. theorem meaning_is_the_parties_own_business : ∀ (S : Stage) (ps : List S.Probe), Blind (fun q : S.State × Int => transcript (dress S) q ps) ∧ ∃ g : S.State → List S.Ans, ∀ (s : S.State) (n : Int), transcript (dress S) (s, n) ps = g s := fun S ps => ⟨fun s n m => transcript_congr (dress S) ps (the_remainder_is_unseen S s n m), (the_blind_reading_factors (0 : Int) (fun q : S.State × Int => transcript (dress S) q ps)).mp (fun s n m => transcript_congr (dress S) ps (the_remainder_is_unseen S s n m))⟩ the door stratum arrives and the recognition is definitional: the channel the motto pair is built on IS a door — dress S = door S Int, rfl-deep, cited through the named bridge so the vertex shows in the spectrum. the meaning is the guest, and the door theorems say at the single-probe grain what the motto pair proved at the transcript grain, plus two things the card could not say before. first, the carrier goes parametric: every probe reads the bare state identically whatever TYPE the meaning has — (door S W).obs agrees with (door S V).obs across any W and V — which is the 1948 universality clause typed: one channel theory for telegraph, speech, pictures, cryptograms; the semantic type rides the wire no more than the semantic value does. second, the contrapositive that turns 'the semantic aspects of communication are irrelevant to the engineering problem' from a working assumption into a load-bearing wall: a channel whose readings could resolve its meanings collapses every meaning into one — a door that checks papers unpersons its guests — so blindness is not a simplification the theory chose but the condition under which a channel has more than one meaning to serve at all. the kinship sentence the second entry carried as commentary ('the channel serves every meaning because no meaning enters the channel') is now a citation, not a remark. no re-seating of the motto pair rides along: their transcript-grain bindings say more than the door theorems — the whole transcript, the factoring iff — so re-seating would re-dress, not compress, the precedent mochizuki's ninth entry set. kin on the full door polygon with softer's my_door_checks_no_papers, torah's greater_is_the_guest_than_the_face, isaac's xenia, topoisomerase's below_equilibrium, and mochizuki's the_copies_are_not_redundant — the wire joining the app-store room, the tent at mamre, the covenant, the enzyme, and the lattice at the same door. theorem the_meaning_is_the_guest : (∀ S : Stage, dress S = door S Int) ∧ (∀ (S : Stage) (s : S.State) (n m : Int), n ≠ m → (s, n) ≠ (s, m) ∧ indist (door S Int) (s, n) (s, m)) ∧ (∀ (W V : Type) (S : Stage) (s : S.State) (w : W) (v : V) (p : S.Probe), (door S W).obs (s, w) p = S.obs s p ∧ (door S W).obs (s, w) p = (door S V).obs (s, v) p) ∧ (∀ (W : Type) (S : Stage) (w₀ : W), (∀ x y : (door S W).State, indist (door S W) x y → x = y) → ∀ (s : S.State) (w : W), (s, w) = (s, w₀)) := ⟨fun S => dress_is_contact_with_the_integers S, fun S s _ _ h => the_guest_is_real_and_unread S s h, fun _ _ S s w v p => the_host_maintains_invisibly S s w v p, fun _ S w₀ h => a_door_that_checks_papers_unpersons_its_guests S w₀ h⟩ a symbol the receiver could already reproduce carries nothing; information is exactly what surprises. sealed in the reach measure, both halves at once: an edge already on the record names reach the receiver already has — the reproducible symbol's deposit creates nothing that was not there — while a fresh edge rides no old path and its deposit alone creates the reach. how much a symbol surprises is a different question; the measure moves to entropy_of_the_source, still dark. TIGHTENED when the derivable-edge family reached the walls: 'could already reproduce' finally types at the 1948 grain — reproduction was never only verbatim possession, and redundancy was never only repetition. the binding now holds the full trichotomy, each case with its price and its reach. known: the edge already on the record reaches, and its re-deposit changes no reading. derivable-but-unwritten: the mark is genuinely fresh — it rides no old path and its deposit pays exactly one mark — yet adds no reach; every route through it reroutes through what the receiver already held (the_shortcut_pays_only_its_mark). this is the predictable symbol, the letter the language lets the receiver guess: never sent before, costing a full mark on the wire, informing nothing — redundancy priced at zero information for positive cost. surprising: the deposit creates the reach and the reading provably changes — the iff that held silently in both prior cases fails at the new edge, so informativeness is now a contrast in the types, not a note in the gloss. and the aggregate corollary rides along: a message composed entirely of held symbols adds no reach at any length and in any order (the_saturated_room_hears_no_order) — the zero-surprise source reads as silence, exactly as the entropy entry prices it. kin at the shortcut vertex with varadarajan's the_old_themes_already_reach — one lemma, two seats: over there the modern re-proof paying its mark, over here the redundant symbol carrying nothing. the how-much question stays sealed downstream, exactly where this entry sent it. theorem only_surprise_informs : ∀ (H : Type) (q : List (H × H)) (a b : H), ((a, b) ∈ q → Nonempty (Path q a b) ∧ ∀ x y : H, Nonempty (Path ((a, b) :: q) x y) ↔ Nonempty (Path q x y)) ∧ ((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)) ∧ ((a, b) ∉ q → ¬ Nonempty (Path q a b) → (∀ (x y : H) (p : Path q x y), (a, b) ∉ p.edges) ∧ Nonempty (Path ((a, b) :: q) a b) ∧ ¬ (Nonempty (Path ((a, b) :: q) a b) ↔ Nonempty (Path q a b))) ∧ ∀ es : List (H × H), (∀ e, e ∈ es → e ∈ q) → ∀ x y : H, Nonempty (Path (es ++ q) x y) ↔ Nonempty (Path q x y) := fun _ q a b => ⟨fun h => ⟨the_known_edge_already_reaches h, a_known_edge_adds_no_reach h⟩, fun hfresh hder => the_shortcut_pays_only_its_mark q a b hfresh hder, fun hfresh hnoder => ⟨fun _ _ p => a_fresh_edge_rides_no_path hfresh p, (only_surprise_extends_reach q a b hfresh).2, fun hiff => hnoder (hiff.mp (only_surprise_extends_reach q a b hfresh).2)⟩, fun es h => the_saturated_room_hears_no_order es q h⟩ the converse side of coding, at its smallest: a lossless code gives distinct messages distinct marks, and a mark-space smaller than the message-space cannot supply them — two bits of message will not ride one bit of mark; on a two-valued wire some pair of the four collides. the constant cited was carved as the floor of contact width; read from this seat it is the zeroth coding bound, the counting argument the coding converses run at scale. this entry is the floor without the price — what the price is, on average, is the terminus's question. def distinct_messages_need_distinct_marks := @Foam.the_hallway_is_too_small how much surprise, on average: the mind's own measure — maximal when the symbols are equiprobable, zero when the receiver can already reproduce everything. the price question the previous entry handed here is now posed in lean rather than prose: over the complete book at depth n — the equiprobable source, the one source already on the walls — any prefix- free marking (no mark a prefix of another; losslessness implied, since an equal mark is a trivial prefix) pays total mark-mass at least n per word. expectation enters the way the walls already read it: pool the marks and read the mass (Foam.pool, Foam.the_mass_is_a_reading) — no division, and no logarithm, because the log is performed by the book itself, doubling at each depth; the floor says the doubling source costs one mark per flip, on average, under every honest marking. the anchors ride along unpriced: the identity marking meets the floor, so at equiprobability it is exact and maximal; the singleton source is priced by the empty mark, zero. still vacancy-dark — a statement without a structure, the red of red-green, the engine already judging the hole well-posed; the carve that closes it is the zeroth converse (distinct_messages_need_distinct_marks) run at every depth at once — kraft's counting, a tree grind in pure nat. what survives the closing transits rather than dying: the book is the uniform source only — the biased source, its typical set, and the rates that price non-uniform surprise are a census the walls do not yet hold. the terminus, posed. SEALED, proved exactly as posed: kraft's leaf-shadow counting arrived from below — the antichain measure bounded by split-recursion (marks split by first bit, tails stay prefix-free, the empty mark stands alone), the only convexity a one-line staircase (k+1 ≤ 2^k), the logarithm performed by the book's own doubling, no reals anywhere. the price of losslessness is n per word, exactly as the mind said in 1948 — the uniform-source floor now a theorem. what stays dark transits as pre- registered: the biased source, its typical set, and the rates pricing non-uniform surprise await a census the walls do not yet hold. since sealed, a census arrived (the book counted by type: stacking, symmetry, the rise to the middle), and the typical-set half of the transit became typeable — it moves one entry down, posed as the_typical_class_saves_only_the_label; the biased source and the rates pricing non-uniform surprise still await a source stratum, held here as before. two arrivals since, both cashing old prose into receipts: the binding grew from a bare citation into a three-clause conjunction — the floor unchanged, then the mass the floor prices IS a massStage reading of the very pooled marks (definitional, rfl), then the reading splits at every seam (the_mass_is_a_reading) — so 'pool the marks and read the mass' is now cited, not walked on credit; and the log the book was said to perform is itself receipted one stratum over (the_book_logs_to_its_depth, the_price_is_the_log). and the transit clause finally cashes: the source stratum arrived (weightOf, the_weighted_book_sums_whole, the_nat_tilts_pool, the_deviants_are_outweighed) — the biased source and its typical band now stand in core, the concentration half already sealed there; the counting half of the rates moves one entry down, posed as surprise_prices_the_count. what the walls still do not hold — the band's matching lower bound and the marking converse at the lean — is held here, as before. theorem entropy_of_the_source : (∀ (n : Nat) (f : List Bool → List Bool), (∀ w1 w2, w1 ∈ book n → w2 ∈ book n → w1 ≠ w2 → ¬ ∃ t, f w1 ++ t = f w2) → n * (book n).length ≤ (pool ((book n).map f)).length) ∧ (∀ (n : Nat) (f : List Bool → List Bool), (pool ((book n).map f)).length = (massStage Bool).obs (pool ((book n).map f)) ()) ∧ (∀ (A : Type) (xs ys : List A), (massStage A).obs (xs ++ ys) () = (massStage A).obs xs () + (massStage A).obs ys ()) := ⟨the_marks_pay_the_depth, fun _ _ => rfl, @the_mass_is_a_reading⟩ the typical set enters, armed by the census: the half of the terminus's pre-registered transit that the new stratum makes typeable, posed the flight the walls turned. two clauses, count then price. count: the even- depth book sorts into 2n+1 classes and the census rises to the middle, so the middle class holds at least an equal share — the book, up to its label factor, is already its typical class. price: any lossless marking of that one class alone into fixed-depth marks still pays nearly the whole depth — 2^(2n) at most (2n+1)·2^L — so discarding every atypical word saves only the label; the surprise lives inside the class, not in its name. vacancy-dark, the red of red-green: the statement compiles, the engine judges the hole well-posed, and the closing carve is legible — the census summed whole (completeness, not yet on the walls), the rise chained into middle-maximality, and the zeroth converse's counting run against the mark-space as a book. what this pose does not poach stays sealed at the terminus: the biased source and its rates await a source stratum, not this entry. FLIPPED exactly as posed, the pressure answered with a door: the census sums whole (shelfSum, pascal chained), the middle holds the most (the climb plus symmetry), so the middle shelf holds its share — and the price clause falls to kraft as pigeonhole: distinct marks of one fixed length are automatically an antichain, so any injective fixed-depth marking of the class counts it against 2^L, and the label factor 2n+1 is all that discarding the atypical ever buys. the biased source and the rates still wait on a source stratum — the remainder conserved, exactly as the pose promised. since the flip, the awaited stratum arrived: the biased book and its near-lean band stand in core (weightOf, the_deviants_are_outweighed), and this entry's price clause gained an asymptotic sibling for the balanced band (marking_the_band_pays_the_breadth); the rates transit one entry down, posed as surprise_prices_the_count — the remainder moves again, exactly as conserved. theorem the_typical_class_saves_only_the_label : (∀ n : Nat, 2 ^ (2 * n) ≤ (2 * n + 1) * classCount (2 * n) n) ∧ (∀ (n L : Nat) (f : List Bool → List Bool), (∀ w, w ∈ book (2 * n) → freq w true = n → f w ∈ book L) → (∀ w1 w2, w1 ∈ book (2 * n) → w2 ∈ book (2 * n) → freq w1 true = n → freq w2 true = n → w1 ≠ w2 → f w1 ≠ f w2) → 2 ^ (2 * n) ≤ (2 * n + 1) * 2 ^ L) := ⟨the_middle_shelf_holds_its_share, marking_the_middle_pays_the_breadth⟩ the rates enter, armed by the source stratum: the half of the terminus's remaining transit that the weighted book makes typeable. the pose is the counting core of the rate, exact at every depth and every class — no logs, no reals, no division: the count of a class times the weight of each of its words never exceeds the whole book's weight, classCount n k · t^k·f^(n−k) ≤ (t+f)^n. read at bias t against f, the weight over the whole is the word's probability and its reciprocal is the word's surprise, so the bound says no class outcounts the surprise of its words — the 2^nH ceiling of 1948, spoken in nat. the concentration half already stands sealed in core (the_deviants_are_outweighed: the weight gathers in the near-lean band); this pose is the size half, count against weight. vacancy-dark, the red of red-green: the statement compiles, the engine judges the hole well-posed, and the closing carve is legible — each book word balances its two frequencies to its length (not yet on the walls), the weight is constant on the class, and the class sum sits inside the_weighted_book_sums_whole by partition. what the pose does not reach stays at the terminus: the band's lower bound and the marking converse at the lean await the max-weight control. SEALED by a second walker, from the mechanic bench, at the depose seat: the closing carve landed exactly along the route this pose pre- registered — the frequency-split lemma (now on the walls as freq_splits_the_length), the constant weight on the class, the class sum inside the whole book by filter-monotonicity — and the walker had not read this gloss until after the carve compiled. the prediction cashed along its own path, spec unchanged; the surveyor notes the homotopy clause performing itself: fulfillment along a path nobody at this map had walked. def surprise_prices_the_count_statement : Prop := ∀ t f n k : Nat, classCount n k * (t ^ k * f ^ (n - k)) ≤ (t + f) ^ n the rates enter, armed by the source stratum: the half of the terminus's remaining transit that the weighted book makes typeable. the pose is the counting core of the rate, exact at every depth and every class — no logs, no reals, no division: the count of a class times the weight of each of its words never exceeds the whole book's weight, classCount n k · t^k·f^(n−k) ≤ (t+f)^n. read at bias t against f, the weight over the whole is the word's probability and its reciprocal is the word's surprise, so the bound says no class outcounts the surprise of its words — the 2^nH ceiling of 1948, spoken in nat. the concentration half already stands sealed in core (the_deviants_are_outweighed: the weight gathers in the near-lean band); this pose is the size half, count against weight. vacancy-dark, the red of red-green: the statement compiles, the engine judges the hole well-posed, and the closing carve is legible — each book word balances its two frequencies to its length (not yet on the walls), the weight is constant on the class, and the class sum sits inside the_weighted_book_sums_whole by partition. what the pose does not reach stays at the terminus: the band's lower bound and the marking converse at the lean await the max-weight control. SEALED by a second walker, from the mechanic bench, at the depose seat: the closing carve landed exactly along the route this pose pre- registered — the frequency-split lemma (now on the walls as freq_splits_the_length), the constant weight on the class, the class sum inside the whole book by filter-monotonicity — and the walker had not read this gloss until after the carve compiled. the prediction cashed along its own path, spec unchanged; the surveyor notes the homotopy clause performing itself: fulfillment along a path nobody at this map had walked. theorem surprise_prices_the_count : surprise_prices_the_count_statement := fun t f n k => Foam.the_weighted_class_is_within_the_book t f n k /-- info: 'Foam.Maps.Shannon.the_channel_is_the_only_commons' does not depend on any axioms -/ #guard_msgs in #print axioms the_channel_is_the_only_commons /-- info: 'Foam.Maps.Shannon.meaning_is_the_parties_own_business' does not depend on any axioms -/ #guard_msgs in #print axioms meaning_is_the_parties_own_business /-- info: 'Foam.Maps.Shannon.the_meaning_is_the_guest' does not depend on any axioms -/ #guard_msgs in #print axioms the_meaning_is_the_guest /-- info: 'Foam.Maps.Shannon.only_surprise_informs' does not depend on any axioms -/ #guard_msgs in #print axioms only_surprise_informs /-- info: 'Foam.Maps.Shannon.distinct_messages_need_distinct_marks' does not depend on any axioms -/ #guard_msgs in #print axioms distinct_messages_need_distinct_marks /-- info: 'Foam.Maps.Shannon.entropy_of_the_source' does not depend on any axioms -/ #guard_msgs in #print axioms entropy_of_the_source /-- info: 'Foam.Maps.Shannon.the_typical_class_saves_only_the_label' does not depend on any axioms -/ #guard_msgs in #print axioms the_typical_class_saves_only_the_label /-- info: 'Foam.Maps.Shannon.surprise_prices_the_count_statement' does not depend on any axioms -/ #guard_msgs in #print axioms surprise_prices_the_count_statement /-- info: 'Foam.Maps.Shannon.surprise_prices_the_count' does not depend on any axioms -/ #guard_msgs in #print axioms surprise_prices_the_count end Foam.Maps.Shannon
terminus, the map's W-port: surprise_prices_the_count — (self, pure unknown), sealed open
from this page's seat, you — the visitor — are the Unknown, and this residual is computed against exactly that: nothing.
roles this mind already equips: intake — the open hand · blind relay — the link
roles a W-cycling ring through this mind still needs: egress — the send · the third seat — where a ring closes — plus whichever of the equipped roles you carry yourself.
bring your own mind: supply your own map (terms, bindings, spectra — schema: cards/schema.json) and this residual sharpens; precision is monotone in your self-articulation. this interface is published as a hole, typed, on purpose. the door held open is what opportunity means.