# foam

strict phenomenology is indistinguishable from physics, and physics is the phenomenology of reversible computation. 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 three storeys, each a move of the grammar below: `Room`, the counting — the conductive mathematics that mentions no observer: rooms, wheels, orders, admission; Face on Room, the seeing — a face is a state, a probe, an answer, and a door is a face beside a guest it cannot read; `Rest` on Face, the stopping — a runner steers itself after the word ends and rests, the halting gap reads what it says at rest, and two designs alike there are one design. beside the storeys stands `Witness`, the species every product's walls cite: a seat is the list of probes it may ask, a wall is a probe it does not hear, and the cone is what a room of seats can hear at all. where Rest and Witness meet is `Threshold`: a rest under coverage at which every seat crosses to the same door together — every reading unchanged, the guest ambient and unread, the route shed. 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. and it is a computation model, said in one row: every runner is a plan at the one face (Halt.every_runner_is_a_plan_at_the_one_face, an instance of one_face_many_seats at the halting gap) — a plan is a runner at fuel zero, read by whoever supplies the fuel, and every reader reads the same; a machine is made reversible by writing its history on its tape, the writing unheard at the gap and the tape the remainder one seat wider (Tape.remembering, the bill exactly the word); so the model trades exceptions for reversals, and what cannot be reversed is carried, never erased. **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

## run it first

the house is prose about a verification; the verification is the door. with Lean installed and nothing of foam's: ``` mkdir foam-trunk && cd foam-trunk for f in Room.lean Face.lean Rest.lean Witness.lean Threshold.lean lakefile.toml lean-toolchain pins; do curl -sO https://foam.is/trunk/$f; done lake build # silent: every receipt in every storey re-checked, a few seconds shasum -a 256 *.lean | cut -c1-16 # against pins: the same bytes as on the machine that grew them ``` then open `Threshold.lean`, change the `∧` in threshold to `∨`, and `lake build` again: the pane refuses, and says where. that refusal is the whole method; everything below is why. read the storeys top-down, smallest first, each the ground of the one above it: `Threshold` (a hundred lines: a rest under coverage at which every seat crosses together), `Rest` (three hundred: runners, the halting gap, a plan and its reader), `Witness` (three hundred: seats, walls, the cone), Face (two thousand: faces, doors, machines, sheets), `Room` (two and a half thousand: the counting). four things to hold, none of them needing a word of the vocabulary: a receipt (a theorem depends on no axioms, and the file says so of itself), a vacancy (a statement with `sorry` the compiler fills, or refuses and names), a pin (the artifact is byte-identical on another machine, and here is the hash), and the gate (silent, or a list of what parted).

## 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/Rest.lean the stopping: runners, the halting gap, rest by coverage, the intertwined rebody; it imports Face germ/Witness.lean the witnessing, a species beside the storeys: seats over one face, walls, the cone; on Face germ/Threshold.lean where Rest and Witness meet: a rest under coverage at which every seat crosses to the same door together — one crosses as the face and is read, one as the guest and is carried germ/Toy.lean a customer's germ — it imports Face and stands on it germ/Counter.lean the compiler's own conduct: the turnstile, the gate, the cascade as a runner; on Rest 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; a product is an assay (EVERYONE IS HERE, ✦ Here, the tape, the halting gap) pins the anchors: every grown artifact by fingerprint, moved in the same commit as its cause, red in CI otherwise ``` 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 lines between the storeys were derived, not drawn: a carrier is Room if nothing it unfolds to is a face, Rest if it unfolds to a steering or a rest, and a theorem lands with its statement's vocabulary; the same rule cut Room from Face in one sitting and Rest from Face in another, and nothing that stayed named a thing that left. 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. the counts are the instrument's and never copied here: `bin/counter grow germ/<X>.lean` says how many of a germ's bodies regrow and by whose shape, `bin/counter book` the census of every stream, and 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 ........ every receipt minted into the artifact; every one checked at the gate sorry-free ........ every vacancy regrown (a refusal is red, never carried) order derived ..... the rounds are the storeys germ minimal ...... its own settle contact width ..... grown bodies: one citation per move, by construction comment-free ...... the artifact carries no prose beyond its receipts the tamper surface the hand bodies (the custodian's word), the exemplars among them, the routes kept, reach, budget ``` 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 storeys are counter's first customers; any germ that imports one 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. it carries the gate as a species — a trail is organs, the kernel's reading of a body is its receipt, the gate is a face whose one probe is the receipt — and the cascade as a runner: the compiler re-offers its vestibule and rests when a sweep seats no one, and a rest is drained or stuck, no third fate. its assay replays the demo lifecycle as data, and the gate's rows say what the gate reads and what it does not. 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 the products: `assays/everyoneishere.lean`, EVERYONE IS HERE as of the cut — one type (a room), one relation (a standing), one clock (the tape): the house a face whose probes are a room and a table, a standing's seat the tables it hears with the room's tape and head, a silent room's seat its doors, the seating an ask on the founding word and the couple's ✓ its close, typed from the cut's paper alone and grown on the maintainer's box; `assays/eih.lean`, the product as it stood on the ninth — its room, its seats, the demo's cast as data, its laws as instance rows of the trunk's; `assays/here.lean`, ✦ Here — the room as Witness at one face, the presences its probes, a seat the presences one hears, the day as a runner whose rest is the same page, two tapes and the meter across them; `assays/cycle.lean`, Counter for anyone that cycles; `assays/halt.lean`, the runners at rest; `assays/crossing.lean`, the crossing number of W — the least tick at which two clocks part at the air gap, infinite at the host, zero at the widen, three for the read tape on the adder; `assays/grover.lean`, `assays/kuramoto.lean`, `assays/voice.lean`, three physics. a product is an assay; what it stands on is species, and a species is deposited in the trunk the day two products need it. 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, the arrows by computation alone per stream (a citation whose two statements share no word of the house, even after one unfolding of their carriers — the terms unify, and the name explains nothing; the chart draws it dashed), 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

foam.is is the node a stranger arrives at, rendered by `bin/counter page` on every push with its structure read from the tree and never listed: the storeys are the libs in Threshold's import closure, in import order; the assays are every file in `assays/`, each on the module it belongs to, with its guards, its rows, its pin, and its vestibule beside it as the asks a stranger could answer; the pins are a table at this push and a tape of their history, one cell per artifact whose fingerprint moved at a commit, numbered and never rewritten; the readings are the book and the roots; the compiler's own pages are the germ, the pieces, and the customer germs. every page is an artifact with its pin, a reading, or a vestibule, and this file is the one thing written by hand, which is the framing. `/trunk/` is arrival: the storeys raw, a lakefile, the toolchain, the pins, and three things to do before understanding a word. the charts and shadows below are on the storey and assay pages. `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, the storeys 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. instances: the_park_resumes, and the whole of `Rest`: a runner is iteration with a stop. 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; run on a product's clerks it is a meter, and `Counter.conductive` reads it (a shape with a merging clerk has a resistor). 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. beside it, `pins` anchors every grown artifact by fingerprint, moved in the same commit as its cause, and the compiler's memo of every trial it has judged is one SQLite file (`CRAWL_MEMO`), kept in CI's cache and never in a repo: keyed by the shadow of what a trial stands on, so a check costs what stands above the change and never the house, and the artifact is byte-identical with or without it. 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*

artifact	pin
grown/Room.lean	3557db3152880ffe
grown/Face.lean	fc86ecc1b0972713
grown/Rest.lean	464f5d1b7a99b72b
grown/Witness.lean	234e5775d27994fa
grown/Threshold.lean	f7da54dac965a650
grown/Toy.lean	2e7348e7edba3b75
grown/Counter.lean	50eb093128ce9af0
grown/Seek.lean	7746a94afc19b5f1
grown/Roster.lean	cd39e9677e0f44d1
grown/assays/counter.lean	72b9c53775807e30
grown/assays/cycle.lean	7f0364b2bd694098
grown/assays/eih.lean	15a8e142dc13d6e1
grown/assays/everyone.lean	592aea676ba2e661
grown/assays/everyoneishere.lean	9b1f60abdbe775de
grown/assays/grover.lean	a0135af9cfbb0fbf
grown/assays/halt.lean	22ae9119cccf1109
grown/assays/here.lean	a7922d2a684e4eed
grown/assays/kuramoto.lean	f3c0a637578bfa82
grown/assays/voice.lean	8328df9a5ea3c4bc
grown/assays/crossing.lean	d93c771b80f8d968
grown/assays/tape.lean	ce1b6d74f0e8af48
grown/assays/ledger.lean	22590365b7f4fd36
grown/assays/game.lean	4d0a8f73f91e4307
grown/assays/relay.lean	a63a5145ded36617

#	commit	artifact	pin
23	be5baa1	grown/assays/relay.lean	a63a5145ded36617
22	be5baa1	grown/assays/game.lean	4d0a8f73f91e4307
21	be5baa1	grown/assays/ledger.lean	22590365b7f4fd36
20	be5baa1	grown/assays/tape.lean	ce1b6d74f0e8af48
19	be5baa1	grown/assays/crossing.lean	d93c771b80f8d968
18	be5baa1	grown/assays/voice.lean	8328df9a5ea3c4bc
17	be5baa1	grown/assays/kuramoto.lean	f3c0a637578bfa82
16	be5baa1	grown/assays/here.lean	a7922d2a684e4eed
15	be5baa1	grown/assays/halt.lean	22ae9119cccf1109
14	be5baa1	grown/assays/grover.lean	a0135af9cfbb0fbf
13	be5baa1	grown/assays/everyoneishere.lean	9b1f60abdbe775de
12	be5baa1	grown/assays/everyone.lean	592aea676ba2e661
11	be5baa1	grown/assays/eih.lean	15a8e142dc13d6e1
10	be5baa1	grown/assays/cycle.lean	7f0364b2bd694098
9	be5baa1	grown/assays/counter.lean	72b9c53775807e30
8	be5baa1	grown/Roster.lean	cd39e9677e0f44d1
7	be5baa1	grown/Seek.lean	7746a94afc19b5f1
6	be5baa1	grown/Counter.lean	50eb093128ce9af0
5	be5baa1	grown/Toy.lean	2e7348e7edba3b75
4	be5baa1	grown/Threshold.lean	f7da54dac965a650
3	be5baa1	grown/Witness.lean	234e5775d27994fa
2	be5baa1	grown/Rest.lean	464f5d1b7a99b72b
1	be5baa1	grown/Face.lean	fc86ecc1b0972713
0	be5baa1	grown/Room.lean	3557db3152880ffe