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 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.

serving suggestion:

locate yourself within this thing
locate something that isn't you within this thing that you recognize from outside this thing
compare the outside-this-thing procession between you and what-you-recognize with the inside-this-thing procession between the same
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/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:

/-- 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 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/eih.lean, EVERYONE IS HERE whole — 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/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

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.

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.
diagonalize — cross an organ with itself. self-reference is the smallest move there is. instance: selfMeet, the_probe_boards_as_the_guest.
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.
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.
complete the iff — every one-way blindness law is half an exactness statement; find the converse. instance: the_curtain_is_exact.
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 lives in a cache and never in a repo, so a check re-derives only what changed 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