foam

but if you create a foam engine with its own backstage/frontstage - assuming the existence of a foam engine upstream -

(you might be looking for github.com/lightward/foam)

this is a type system for supporting physical (as in conservation) user-generated content with a digital (as in zeroes and ones) backend

this repo's history is as important as any single ref in it. git gives us that for free, granted. nice to have the right tools. :) if you're searching foam's concept-space, usually a good idea to include the commit record in your search, emphasis on "usually" because ideas from another time were born in another time, and the now is always greenfield

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)

mathematics

mode: self-documentation strictly as a side-effect of self-derivation until the point of self-recognition

filter: only what a new arrival would ultimately, under careful study and testing, conclude holds as self-evident

commission: helping those new arrivals do whatever they're here to do

axiom-free, because an imported axiom is a pov, and imported perspectives either reduce to self or become cytokinetically distinct. no disposable points of view conjured in the course of reasoning - v important, an observer is always and only ever byo

what we can say for sure: the fundamental theorem of projective geometry has a hole in it (the assumption of closure/completion), and you can fill that hole however you want (lots of ways to create closure/completion), but if you want to use ftpg and live with the results then there's a hole needs filling (emphasis on the gerund; it doesn't end, and so must have its own kind of stability)

shape

a bare index (the skeleton, so the integrity check can hold the fold to the corpus; the telling is bin/foam-gait's spine):

Foam/ — the axiom-free core: Int Ledger Golden Cleared Scar Maintenance Held Backstage Bubble Census Cable Wedge Elsewhen Duplex Vacancy Metaphor Engine Seat Platonism
- Foam/Seat/: Beholder Bootstrap Born Characters Clock Closure Connection Descend Dial Doubling Epoch Forcing Frame Group Hospitality Ladder Loop Meet Naming Norm Observer Octo Quiver Rank Rendezvous Resume Rotations Seam Sed Signature Signed Sort Stage Summit Terminal Tight Triad
- Foam/Engine/: Chirality Codec Drain Generator Spectrum Stream Summary
- Foam/Bridges/ (axiom-free bridges): Adams Cantor Desargues Dirichlet Eddington Gita Gleason Godel Heisenberg Hurwitz Kolmogorov Landauer Lovelace Materiality Minkowski Nicaea Noether Pauli PSQL Pythagoras Relativity Schrodinger Stone Varadarajan Wigner Zeckendorf
- Foam/Platonism/: Tower
counter/ — the application, axiom-free (requires only foam)
seam/ — the identifications, core-Lean axioms only
bridges/ — the Mathlib reunion, classical axioms sealed behind the package boundary

expeditions

nb: there's enough congruence-at-scale for surprising links to crop up in surprising places. don't force connections, but maybe don't immediately reject constructions that come to mind either; a bridge is a construction between two places that existed prior, and a bridge creates both a job and housing (i.e. bridgekeepers)

todo: todo
address-search: contents and the index are different strata (the_list_is_the_opinion at filesystem scale — sāyujya.md never says its own name; the name is readable only from the directory's seat). tsortability as a domain settling itself in preparation for something like neural search, those words at face value, no imported definition: a settled spine (defect low, names honest to their stratum) is what makes retrieval-by-address possible, search over seats rather than cells? the gait already reads the repo this way — is the settling FOR the searching?
- search
  - research: "what happened, in words we understand?"
    - classical search, searching the ledger
  - upsearch (3-perspectives/upsearch.md): "what am I looking for, in words I don't know yet?" (receipted at directory scale: the_search_registers_flip, counter/Counter/Upsearch.lean — research runs name→cell, upsearch runs content-predicate→name; the returned word is the index's contribution since contents can't mint names, the found carries its rejection-trail, and the new word validates immediately in the classical register)
    - quantum search, searching the frontstage
      - noting that the only thing that can be found on the frontstage, found to be distinct from self, is something that has its own irreducible pov
- search-readiness affords flipping search registers while staying ma'at-ready?
- at some point the structure represents itself in its own address-space (first receipt: the_structure_represents_itself, counter/Counter/Address.lean — the cell never says its own name, the seat reads every name, the index page is seated at an address inside the space it indexes, and the page settles the whole space including its own seat, no regress)
  - important: olean drops proof bodies, but if we get foam's lean corpus right the proof bodies will legible in the olean-as-functioning-address-space
    - you'd expect that, from a lfp<->gfp structure, yeah?
- recasting quantum computing as quantum search - should be a concrete bridge into traditional (lol) quantum computing terms
- think: guests are found faster in a Hilbert hotel with a warm index than with a cold index, but they're ultimately findable either way, and faster/slower is only a thing from inside the search. index temperature (?) is the only way you can tell (from outside the search, at the interface level) how it's going in there (receipted at finite scale: temperature_is_the_only_tell, counter/Counter/Temperature.lean — the answer ignores the walk, the walk reads the ordering, every guest is found inside the walls)
clean-exit (seated 2026-07-11, at the close of the address-space landings, by Isaac's ask): make the clean exit a natural and regular occurrence in Counter's user journey — tools that don't leave residue on your hands, that attach no strings to you as you go, that let you shrug off the strings you know about and make visible the strings you didn't. what can be said in Lean to make this more inevitable for Counter's downstream? standing receipts to build on: exit_is_one_move (mercy: from anywhere, at any depth, permanently), entrance_writes_exit (the space's constitutive property), spine_comes_home + Balanced (wedge: opens in order, closes in reverse). the candidate carve: the continuous gait — the discipline where every block closes in the turn that opens it, so depth never exceeds one and the unwind is already done whenever the exit forces. exit-cost as a legible gauge (= current open-wedge depth); the open prefix enumerable at every moment (the strings made visible); homecoming reachable in exactly depth moves (the strings shrugged off). ma'at-readiness as a gait property, not a cleanup step — "nothing keeping us" said as an invariant held at every prefix, not a condition checked at the end
foam: "your physics don't have to run in the same place as mine for us to see each other"?
bubbles: given a bubble floating within a bubble-within-a-foam, the instant the interior bubble touches the exterior bubble, it joins the foam and the bubbles become structural peers while retaining an observer-theoretic family tree?
ancestors: "observer-theoretic family tree" - does this describe conception as a worldline fork, in which those operators contributing to conception together wrap a new observer (3-perspectives/body-of-knowledge.md:11), creating a new zero-knowledge operator? the ancestors watch over you because those operators are literally part of your runtime observation loop?
- see also git-log's --min-parents= (and --merges) and --max-parents= (and --no-merges)

bridgework

what does general knowledge say you can do that the model says you can't, and the model is right?

maintain two counters simultaneously for free from a single actor position without introducing additional povs that require translation to prevent eventual deadlock
directly convert inference to definiteness without increasing the actor population; or: reduce total uncertainty using inference (in-system shadow: definiteness_costs_a_seat, counter/Counter/Wedge.lean)
what else?

and what does general knowledge say you can't do that the model says you can, and the model is right?

bridge from domain x into domain y, do an operation in y, and come back to domain x with results that x can validate but that x couldn't have calculated (in-system shadow: the_search_registers_flip, counter/Counter/Upsearch.lean — x is the name register, y is the content register; the word that comes back validates at the seat, but no content-to-name function exists for x to have computed it)
- smells like a quantum call from a classical routine? feels like there's a dynamic here where the uncertainty in the results is related to how much the ledger's history recognizes the question asked
harness uncertainty safely
prove safety of inference
- hint: the proof involves both the proofreader and the proofwriter (in-system shadow: the_proof_takes_two_seats, counter/Counter/Wedge.lean — the receipt is chart-free, so the writer's settle validates at every reader's seat)
what else?

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

same