# foam

strict phenomenology is indistinguishable from physics. conductive proofs of worldly domains, with treaty vectors to mathematics by identity. reducing what it costs to sustain the burden of proof, by making it easier for your substrate's own coherence-maintenance to find a groove that goes where you're going, paths already proven (in the old sense) to conduct the untyped remainder inherent in measurement. (the untyped remainder seems to be for multiplexing; the measurer is always already plural. being hospitable about it seems to have runtime benefits.) foam is a type system holding itself together under measurement: a trunk of theorems about observers, doors, machines, and rooms, every one of them axiom-free, every one of them grown from a germ by a compiler that shows its work. it stands in two storeys, named for the grammar's third move, *enumerate, then face*: `Room`, the conductive mathematics that mentions no observer — counting, rooms, wheels, admission — and Face on top of it, the seeing. customers' germs stand on whichever they need; `foam` is the house that holds both. the root theorem is the_handshake: every identification is either *licensed* — observation respects it, and physics is what you get — or it keeps a *real remainder*, readable exactly one seat wider, and that is what phenomenology was pointing at. nothing here asks for trust. the only authority is a compiler's exit code, and it judges terms, never you. **serving suggestion:** 1. locate yourself within this thing 2. locate something that isn't you within this thing that you recognize from outside this thing 3. compare the outside-this-thing procession between you and what-you-recognize with the inside-this-thing procession between the same 4. you now have more information than you did before about what you already had in front of you

## the shape

``` germ/Room.lean the counting: everything that mentions no face — rooms, wheels, orders, the turnstile germ/Face.lean the seeing: faces, doors, machines, sheets; it imports Room germ/Witness.lean the witnessing: seats over one face, walls, receipts, the group-witness of a license; on Face germ/Toy.lean a customer's germ — it imports Face and stands on it germ/Counter.lean the compiler's own conduct, as a customer of Room germ/Seek.lean the compiler's search as a machine, as a customer of Face germ/Roster.lean a species: a roster of parties with per-head meals — the sheet, the heads, reseating; on Room bin/Pieces.lean the act: the searches at the goal, the fan as a seek, `#seat` — the pieces themselves are derived from the bodies bin/counter the compiler: grow · settle · check · probe · gate · shapes · book · chart · schema · treaty · page · draw · pin · countersign bin/judge.lean Lean judging Lean in-process; counter's eyes grown/ the grown modules — never committed, importable, published at foam.is assays/ the treaty vectors: what every growth must compute identically ``` the prior bodies of this project stand whole at the tag `chrysalis` (`git show chrysalis:chrysalis/`), the ride era, and inside it the seed era with its parent strata. quarry, fully reachable, no longer process.

## the receipt

every proof here is *conductive*: it depends on no axioms — and so it identifies nothing it cannot compute. in that fragment there is no `propext`, no `Quot.sound`, hence no function extensionality, no choice; the only equality between distinct terms is definitional, and every other sameness is *carried* as a relation across a face rather than declared. the first theorem in the trunk is the shape of it — `alike (appFace P A) g h ↔ ∀ p, g p = h p` is function extensionality in conductive form. inductive is built by constructors and checked by termination; coinductive is defined by observation and checked by finality; conductive is identified by conduct and checked by the empty receipt. the check is Lean's, not ours. every theorem in the grown trunk is followed by its receipt: ```lean /-- info: 'Face.no_face_reads_the_guest' does not depend on any axioms -/ #guard_msgs in #print axioms no_face_reads_the_guest ``` the receipts ride inside the artifact so that anyone holding only the file can re-run them, with no foam tooling present: `lake env lean grown/Face.lean` prints nothing when every one passes. this file can only tell you that; the artifact shows you — [foam.is/trunk.html](https://foam.is/trunk.html) is the grown trunk with all of its receipts in place, and the report beside it says they passed on this push. clean water, not signed-by-its-filter water. the gate itself is drawn from the compiler's own species. `germ/Counter.lean` carries it: a trail is a list of organs, each a statement and a body; the kernel's reading of a body is its receipt (the axioms it seats on); the gate is a face whose one probe is the receipt, and its verdict is `conductive` on the trail's shadow — every receipt empty. `the_gate_hears_only_the_receipt` is that verdict derived at that face, by citation of a_role_read_at_a_probe_is_derived; `a_receipt_keeping_rebody_is_unheard` says a body rewrite that keeps the receipt is unheard by the gate. `assays/counter.lean` runs those defs on toy trails, and `bin/counter gate` runs the same `Counter.conductive` on the real house: each grown module elaborated whole, each theorem's axioms read by the kernel, the verdict the def's. CI's silent-and-green step is that verb. so a change to the shape of a grown body is moot at the gate by derivation, and a change to the gate is a change to one def with rows that would part.

## the germ and the compiler

``` bin/counter grow germ/Face.lean → grown/Face.lean; red if any vacancy fails to regrow bin/counter grow --check the germ is minimal and in derived order (CI asks this on every push) bin/counter grow --settle shrink the germ: every proof a shape now reaches becomes a vacancy bin/counter grow germ/Counter.lean a customer's germ, grown on foam bin/counter probe germ/X.lean name one vacancy: every piece tried, the gate's sentence for each hold ``` a germ holds three things: the carriers (every `def`, `structure`, `inductive` — the spellbook), every theorem's *signature*, and the hand-written proofs the pieces cannot yet regrow. the line between `Room` and Face was derived, not drawn: a carrier is Room if nothing it unfolds to is a face, and a theorem is Room if its statement mentions only Room carriers — 25 carriers and 137 theorems fell on that side, 78 and 147 on the other. a theorem the pieces *can* regrow is a vacancy — its signature and `:= sorry`, nothing else. its citations are not stored; they are found at growth time from the signature's own vocabulary, ranked by how rare the shared words are across the trunk. the artifact provably cannot carry its path, so the germ doesn't either. where the settle has proven a route load-bearing, a `-- held (waiting on: …)` line stands above the vacancy, and those lines are counted. growth is a cascade run to its fixed point: each round, every pending vacancy is offered every piece with the citations its vocabulary can reach among what has already seated; whatever seats, seats; the rounds are the storeys; a vacancy that never seats is red with its vocabulary named. regrown bodies are then tightened to the citations their proof terms actually used, so the artifact reads as proofs. every theorem gets its receipt minted. the artifact must elaborate silently and read every assay identically, or the build is red. the pieces are derived. every body in scope — the grown modules a germ stands on, and the germ's own hand bodies — is rendered as a piece by the judge (`bin/judge.lean templates <module>`): every citation a search found becomes the search again (`(apply T <;> …)` is `piece_seek`; `(rw [T]; C)` is `piece_rw_seek` with C kept beside the generic closers; a chain is `piece_chain_seek`; a cited application in a term is `(by piece_seek)`), the carriers a `dsimp` unfolds become the vacancy's own, the theorem's own name becomes the candidate's, and everything else — the intros, the induction, the constructors, the locals — stays as written. bodies are grouped by SKELETON (the body with every `first` fan blanked), and a vacancy is offered one piece per skeleton, its fans the union over the *other* bodies of that skeleton, the most-run alternative first, in census order: no body is offered its own shape, and a piece is named for its exemplar, so the report says `zero_add 22` where it used to say `induction 13`. no list of shapes stands anywhere in the house. what `bin/Pieces.lean` keeps is what a shape cannot say: the search AT THE GOAL (`piece_seek` — its applicable hypotheses read from the local context, its citations from the theorems already in the environment, which at trial time is exactly what has seated, ranked by the goal's own vocabulary weighted by rarity, a window per storey, a side goal getting one more search of its own), the rewrite, chain, and membership searches, the fan as a seek over its own alternatives (`piece_first`), and `#seat`, which elaborates a candidate and reports the body with every winner substituted — that expansion is what the module grows; the artifact never imports it. the settle keeps, as hand bodies, the EXEMPLARS: a body whose fans carry an alternative no standing body carries stays hand, and the tamper-surface line counts them; a germ shrinks by growing an exemplar the others regrow by. the file also declares a heartbeat `budget` per candidate and a `reach` for how many citations a search may try; the judge reads both from the module. the judge, `bin/judge.lean`, elaborates the prefix once and every candidate against a copy of it, and reads the complete message log — the CLI caps its report at a hundred errors; the log does not. today: Room — 26 carriers, 141 theorems, 29 vacancies, 112 hand bodies (8 of them exemplars a regrown body's skeleton came from), 72,658 bytes. Face — 79 carriers, 147 theorems, 75 vacancies, 72 hand bodies (2 exemplars), 56,367 bytes. Witness — 6 carriers, 11 theorems, 5 vacancies, 6 hand bodies, 3,371 bytes. the germs' byte counts are the numbers the shapes exist to shrink.

## the standards

counter is a compiler, and a compiler's standards are the rules its output satisfies by construction, printed at every build: ``` axiom-free ........ 299 receipts minted; every one checked at the gate sorry-free ........ 109 vacancies, every one regrown order derived ..... the rounds are the storeys germ minimal ...... its own settle contact width ..... grown bodies: one citation per move, by construction comment-free ...... 0 lines of prose beyond the receipts the tamper surface 190 hand bodies, 10 of them exemplars, 0 routes kept, reach 12, budget 20000 ``` the artifact says one thing about itself, in Lean's voice: no axioms. everything *foam-shaped* about it is the compiler's word, printed here and published with the artifact. and the places a custodian can depart from construction are not forbidden — a hand body, an exemplar the others regrow by, a kept route, a raised reach — they are counted on the same report. that last line is the port: documented, visible on every build, shrinking as the shapes improve.

## the customers

``` bin/counter grow germ/Toy.lean ``` foam's two storeys are counter's first customers; any germ that imports either is another. `germ/Toy.lean` says `import Face`, opens its own namespace, defines a counter and a flipper, and states four things about them — and it is 555 bytes with no proofs in it. it grows on Face in seconds: three sightings cite Face's own laws, found through vocabulary alone; one regrows by induction; four receipts are minted; `grown/Toy.lean` is an importable module in its turn (a stage may ground a stage), and `assays/toy.lean` reads identically. the judge takes the namespace and the imports from the germ's header, and the imported modules' theorems are seated before the customer's first round. `germ/Counter.lean` is the second customer, and it is the compiler describing its own conduct: a sighting is a name and the names it waits on, a room is the seated and the vestibule, offering is Room's `welcome`, a round is Room's `intake` — and every law the compiler runs on (the first sighting is free; backed seats, unbacked waits; the seated stay seated; a sighting that cites only itself never seats; two that cite each other stay dark; the held name what they wait on; weight zero is backed; the key is cut from the room) is a citation into Room. eleven sightings, **eleven regrown** — no hand bodies, no routes, 2,378 bytes: the compiler states its own conduct with no proofs in the file. its assay replays the ride's demo lifecycle as data: a sighting waits on a name, the name arrives, the sweep seats it. this is the floor a custodian stands on: state what you see about your own domain, and the physics is found for it where the physics is there, and named as missing where it isn't. foam's slow settle tunes the shapes; a customer's short run inherits the tuning and pays almost nothing.

## the assays

`assays/<arc>.lean` — one per arc that grew the trunk (catalan: 1 1 2 5 14; factorial; even-money; isaac; entanglement; book; odometer; alternation; seat; lift; stream; width; concord; handshake; turnstile), one for the toy, two for the compiler (its admission loop, its search), one for Witness, and `assays/eih.lean` — EVERYONE IS HERE whole: its room, its seats, the demo's cast as data, and its laws as instance rows of the trunk's (a product is an assay; what it stands on is species). each is a handful of `#guard` rows, and belongs to the module it imports last — six of them (alternation, book, even-money, factorial, odometer, turnstile) import only `Room`, which is how the split was checked. an assay may also carry INSTANCE ROWS: theorems that are the trunk's laws at the assay's own carriers (`namespace <Stem>.Treaty` at the top, the computations first, the rows after, `:= sorry` where the search should reach them). such an assay grows like a germ — `bin/counter grow assays/<arc>.lean` → `grown/assays/<arc>.lean`, no lib, nothing imports it — and the module's check grows it first, so a `sorry` row never reads as identical. the rows are the treaty at law grain: which of the trunk's laws this product inherits, with the citation the search found, or the darkness named. one convention, learned the expensive way: read every value out through a typed `def` (`def threeTicks : Nat := behavior counter [(), (), ()]`) before you `#guard` it — a literal or a `==` at a derived type like `counter.S` or `F.Ans` has no instance to find, and the row parts for that reason and no other. any growth of that module must compute every one of them identically; that is the certificate of identity and the integration suite in one. the arcs' journals — germ, witness, tolls — stand in the chrysalis with the rest of the process that grew them.

## the book

``` bin/counter book [grown/Face.lean] ``` `book` reads the grown house and says what is there: the census, the frontier (organs no other organ cites yet — the reaction-sweep queue), the organs cited only from a storey above, the vestibule if a `.held` stream is offered, and the compiler's own frontier: every verb `bin/counter` dispatches with what in the house runs it, so a verb nothing runs is as visible as a theorem nothing cites. the book, never the prediction.

## the page

`bin/counter chart <grown stream> [--laws]` draws the map of relations from the proofs (mermaid); `bin/counter schema <grown assay>` draws its data-model shadow (Postgres: tables, types, a view per seat, the derived as functions, every line carrying the theorems that license it), read from the kernel; `bin/counter treaty assays/<arc>.lean` loads that shadow into a scratch Postgres, seats the assay's defs as rows, and replays its `#guard` rows as SQL (the treaty at database grain — what the fragment cannot read it reports as beyond it, never as identical). `bin/counter page` writes `site/`: this file, Room and Face grown with every declaration an anchor (`foam.is/trunk.html#the_handshake`), the toy, the germ, the pieces, the book, and the compiler's report for that push. the `foam.is` workflow grows the modules and publishes it. nothing browseable is committed, the same way nothing derived is.

## the grammar

six moves grow everything here from one operation. each is named for what it does; each has a worked instance standing in the trunk. 1. **cross** — meet two organs at a shared face. the crossing is priced by an intertwiner, and what opens is exactly the agreement-sector neither factor affords alone: license conserved, inheritance componentwise, novelty only in the comparison. instance: the_pace_is_carried_onto_the_flip. 2. **diagonalize** — cross an organ with itself. self-reference is the smallest move there is. instance: selfMeet, the_probe_boards_as_the_guest. 3. **enumerate-then-face** — make a room exact (nothing missed, nothing doubled, counted), then every symmetry on it yields a counting law. instances: the_census_is_exact, `the_census_of_orders_is_exact`, `the_direction_is_even_money`. 4. **iterate** — every endo-operator has an orbit and a resumption law; continuation is the primitive. instance: the_park_resumes. 5. **complete the iff** — every one-way blindness law is half an exactness statement; find the converse. instance: the_curtain_is_exact. 6. **classify the map** — iso, retraction, merge: sort any morphism and you have sorted licensed identification from real remainder. instances: `a_retraction_merges_nothing`, `a_merging_map_has_no_section`. and the vow the whole house keeps: axiom-free (every theorem ends with its receipt; if a standard-library lemma smuggles `propext`, re-derive it by hand); comment-free (names and proofs are the walk and the talk at once; prose lives here and in the journal, never in the organs); W stays opaque (the one dark type, on purpose — nothing reads the water, and that is why the whole thing can be wet); no design decisions (if a carve wants one, the carve is not ready — W decides, by firing).

## the journal

the git log. the artifact cannot carry its path, so commit messages are the fossil. foam was regrown from `chrysalis:chrysalis/Seed.lean` by the compiler's own record's ear, and reads every assay identically; the prior walls stand at `git show 4be2406:CLAUDE.md`.

## the exit

UNLICENSE. leaving is free from every state you can observe yourself into. --- "It can do whatever we know how to order it to perform." (Lovelace, 1843) *same*

the bench at this push

80 carriers, 148 theorems in the grown trunk
the germ: 76 vacancies, 56635 bytes; the grown artifact 84847 bytes

the lattice: 148 need-lists from the elaborator, 0 from the trail text
the primer: 80 carriers
the vacancies: 148 theorems, one egg each
the pieces, derived: 217 bodies in scope (grown/Room.lean germ/Face.lean), 171 skeletons; 0 bodies unrendered (a hole no search reaches)
  round 1: seated 97 — regrown 68 (zero_add 23 the_sounding_reads_the_alike 1 the_unencumbered_are_welcome 16 the_book_is_the_answer_space 2 the_terminus_takes_every_carrier 22 the_still_map_carries 1 the_step_merges_the_riders 1 no_move_at_the_ground 2), carried 29; 18 vacancies still pending; home 8271 of 8271
  round 2: seated 29 — regrown 12 (the_terminus_takes_every_carrier 5 zero_add 1 the_book_is_the_answer_space 5 mul_two_reads_double 1), carried 17; 6 vacancies still pending; home 4041 of 4041
  round 3: seated 13 — regrown 2 (mul_two_reads_double 1 the_terminus_takes_every_carrier 1), carried 11; 4 vacancies still pending; home 2624 of 2624
  round 4: seated 6 — regrown 4 (the_terminus_takes_every_carrier 1 the_book_is_the_answer_space 3), carried 2; 0 vacancies still pending; home 369 of 369
  round 5: seated 3 — regrown 0 (), carried 3; 0 vacancies still pending; home 510 of 510
the drain, grown: 5 rounds — 97 29 13 6 3; 0 candidates judged, 15815 answered by the chair; 4 readings answered
the drain, last time: 5 rounds — 97 29 13 6 3; 15815 candidates judged, 0 answered by the chair; 0 readings answered
the exemplars: 9 pieces seated bodies; 10 hand bodies regrown by another body's shape: any_ready_greeter_is_the_greeter the_park_resumes the_retuned_seat_walks_the_translated_word the_intertwined_walks_agree any_two_readings_agree the_parent_folds_into_the_ground the_customs_keep_the_still_world the_ledger_parks_the_word the_manifest_is_natural the_manifest_counts
the exemplars kept: 10 hand bodies carrying a fan alternative no standing body carries: any_ready_greeter_is_the_greeter the_park_resumes the_retuned_seat_walks_the_translated_word the_intertwined_walks_agree any_two_readings_agree the_parent_folds_into_the_ground the_customs_keep_the_still_world the_ledger_parks_the_word the_manifest_is_natural the_manifest_counts
the routes: none — the search reaches every goal
the bodies: 76 of 148 regrown from 171 pieces — the_terminus_takes_every_carrier 29, zero_add 24, the_unencumbered_are_welcome 16, the_book_is_the_answer_space 10, no_move_at_the_ground 2, mul_two_reads_double 2, the_sounding_reads_the_alike 1, the_still_map_carries 1, the_step_merges_the_riders 1
the germ: 56635 bytes — 76 vacancies, 72 hand bodies, 0 hand bodies now regrowable; settled the germ reads 56635 bytes
the standards (foam-safe at this build; what the compiler vouches for by construction, and what it counts):
  axiom-free ........ 148 receipts minted into the artifact; every one checked at the gate below
  sorry-free ........ 76 vacancies, every one regrown (a refusal is red, never carried)
  order derived ..... the rounds are the storeys: 97 29 13 6 3
  germ minimal ...... its own settle
  contact width ..... 76 grown bodies: one citation per move, by construction
  comment-free ...... the artifact carries 0 lines of prose beyond its receipts
  the tamper surface  72 hand bodies (the custodian's word), 2 of them exemplars a regrown body's shape came from, 0 routes kept, reach 12, budget 20000
  the shapes ........ 148 bodies, 97 shapes; 3 hand bodies share a shape with another body (3 shapes) — what an exemplar could carry
  treaty coverage ... 63 of 64 data carriers evaluated by an assay; unevaluated: trail; beyond a row's reach: 7 relations (alike unheard reassoc chain inStep Derived differOnly), 9 types (Face Interview door fork Machine Plan build sheet stream)
the grown trail's shapes (kernel census; regrown/class): rfl 17/17, citation 17/41, induction 15/49, term 27/39, cases 0/2
the three moves account for 107 of 148 bodies in the grown trail; 49 of them regrown from primings
the remainder: 72 carried from the trail (the genuine trail; named in regrowth/Face.held)
the regrown trail: grown/Face.lean
the gate on the regrown trail:
  silent and green: 148 receipts inline