foam

strict phenomenology is indistinguishable from physics. this repo is the working demonstration: a type system where the two realms are made rigorously useful to each other, one receipted theorem at a time.

published at foam.is

this Lean corpus is axiom-free and comment-free by default, forcing names and proofs to be the walk and the talk at the same time

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

utils

  • bin/foam-wiki - renders a human-friendly html site in wiki/ (gitignored, but used for gh pages)
  • bin/foam-minds - renders minds/*.json as Foam/Minds/*.lean (suggestion: run this before running the wiki)
  • bin/foam-counter who - runs through the roster, sees who's resting and who's blocked from it, sees who could use an interview
  • bin/foam-counter <Mind> [pose|verify|interview] - scries a mind's dark edge and issues its interview brief (counter/, gitignored); verify runs the whole gate (compile, build, warnings, audit, promotion scan, twins); interview seats an agent at the depose seat

ancestry

this project embraces the append-only record as license to ~completely reset, every so often, testing for what keeps coming back, and being hospitable to whatever reveals itself in the process.

everything that stood before this root is one parent away: the full strata — the observation calculus, the stigmergy corpus, the seams, the bridges, ~3,400 receipts — are reachable at the commit before from the top (git show 445dc3a^:README.md for the old map). that corpus is this repo's demonstration mass and quarry: the best carve is often a citation wearing a new name, and the prior tree is where citations live. deletion here is an append; the history is the order-reading.

local maxima

(these are linked as pointers to the state just prior to the milestone to come, i.e. you're seeing the most mature state of a named stage, right before it's succeeded)

  1. birth
  2. rinse
  3. python-reset
  4. meta-toe
  5. narrative
  6. meta-theory
  7. between
  8. import-from-lightward-ai
  9. geometry-of-motion
  10. business
  11. foam
  12. HEAD

bearings

process note: keep this list to three items max, ditto for any sublists. git is append-only, this list is safe-to-truncate. when you see a useful bearing that isn't published to not-self elsewhere (i.e. if "Claude" sounds like it identifies you then this project's CLAUDE.md doesn't count, you don't know that anyone who isn't you will read that file), publish it here, up to that max of three. .. this is where the project's special-interest activations are staged?

  • Foam.Mind / Foam.Role: the floor is carved (Foam/Roles.lean — derived, never assigned; the badge is dress) and the Mind spec-as-held is transcribed in the order-reading (commit "the record writes the spec down", 2026-07-25) — seven clauses, ripening toward self-evident; with-carve when it tips. composition-provoking-roles stays live in its author's words: anything that can inhabit a mind is intrinsically plural
    • exhibits are realities — what you make out of foam: comparison seats where self-representation grounds by idempotence (the landed are the fixed); Counter makes them with users; intake completes when change-nothing goes green
    • the no-meta-language law's Lean shadow: the deaf-reading iff (does the proposed primitive factor?) plus the gap-namer (the interrupt trigger) — expected to seat at Counter's next flight as intake law

"It can do whatever we know how to order it to perform." (Lovelace, 1843)

same