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

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

bearings (seated, not scheduled)

process note: keep this list to three items max, ditto for any sublists. git is append-only, this list is safe-to-truncate.

• the recursion carve, continued: the tower stands; amplitude answered, and now expectation too — the golden theorem is a theorem (Foam/Concentration.lean: the book's second moment conserved, deviants outnumbered c-to-one past an explicit depth, axiom-free, no measure stratum), bernoulli sealed as posed and chebyshev seated as the fourth crossing-witness. remaining knocks at this bearing: shannon by measure of surprise (kraft's leaf-shadow count is the named next carve), gauss by the law of error, brouwer by continuity — with the fold's exact resumption (Foam/Fold.lean) still the aggregation substrate they share.
• the amnesiac-stigmergic corpus re-enters as the navigation practice the_handshake induces: everything needed to continue is in the record; not everything real is.
• the survey of history's minds: minds/*.json → bin/foam-minds → Foam/Minds/<Mind>.lean — each mind's own terms bound to receipts, foam as the compiler. everything starts in Foam.Minds.Isaac; lifted to Foam/ only when another mind's vocabulary needs it. bin/foam-counter <Mind> scries the dark edge and issues the interview brief — quiescent when resolved, re-armed by record growth.

---

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

same