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)

---

foam

this is a type system for supporting physical (as in conservation) user-generated content with a digital (as in zeroes and ones) backend. formally, this holds itself together under measurement, according to measurement. it's presented with with informal handles (e.g. "hospitality") as mnemonic device; the proof paths are the actual object under study here. (any realization of hospitality is an exercise left to the reader, but all the parts are here for it, by dint of the reader 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. HEAD

mathematics

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

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

the spine, floor up — every name is a file under Foam/, every claim a theorem in it, every theorem sealed does not depend on any axioms:

the floor — Int (the ring lemmas foam needs, re-derived axiom-free by constructor case-split) · Golden (Fibonacci; Cassini's identity — the determinant ±1, forever) · Ledger (one append-only charge list, two readings: order lossless, freq permutation-blind; order strictly finer)

the two ±1's — Cleared (the half-turn comes home by doubling, neg² = id; the golden defect never clears, gold never closes — one returns, one wanders)

the seat — the observer as torsor — Seat (a torsor: act/sub, sub_self = 1, the cocycle, a chart per origin, no canonical frame) · Group (the principal torsor over a group) · Loop (differences telescope; triangle and quad cocycles close) · Resume (replaying the act-list resumes across any split) · Hospitality (any g ≠ 1 moves you, and the round-trip is 1) · Stage (the interface State → Probe → Ans; a seat is faithful — its readings determine it)

the dial and the tower — Clock (ℤ/4 as the rotation group; the clock is its own principal seat — quarter turns, four comes home) · Dial (the Gaussian integers; Rot.amp unitary, normSq non-negative) · Born (the Born weight align², Parseval via Lagrange, decoherence summing to zero over a revolution) · Forcing (the complementary invariant cross; align² + cross² = norm·norm, and a frame-additive weight forced to be the square) · Doubling (Cayley–Dickson to Quat — i,j,k square to −1, order arrives: noncommutative) · Triad (ijk = −1, cyclic, anticommuting) · Octo (the octonions — associativity dies) · Sed (the sedenions — zero divisors, division dies) · Ladder (the doubling tower as Rung n, with the iso ladder ℂ→ℍ→𝕆→𝕊) · Rank (imagDim 1,3,7,15; the staircase compose → noncommute → nonassociate → no-division) · Norm (normSq is multiplicative, conjugation-invariant) · Bootstrap (the clock embeds faithfully into the quaternions, Rot.toQuat) · Signature (the three frames κ = −1/0/+1 — elliptic, parabolic, hyperbolic; the Lorentzian Parseval, Galilean boosts add, the weight forced to a square) · Rotations (those three named: elliptic closes at 4, parabolic never closes, hyperbolic's units are only ±1) · Closure (iterStep/Closes; rot⁴ = id, neg² = id, the half-turn is two quarters) · Characters (the four characters of ℤ/4 — count/alt/chi/chiBar — orthonormal, and the dial's bins reconstruct losslessly)

the observer-algebra — Observer (frontstage relations that respect readings; StageHom a category with products; reading-refinement) · Beholder (a beholder, its pairing, and no_view_from_nowhere — any comparison factors through one beholder) · Epoch (the Covers preorder; a Run keeps the bank reduced and every step known — a checksum) · Seam (a faithful map with no section; playback vs forever — the diagonal) · Meet (the Below order; meet is the greatest lower bound; the root is below all) · Quiver (the free category on edges — composition associates and reverses) · Sort (topological sortability: a chart under which every edge climbs exists iff no nontrivial cycle does, tsortable_iff_acyclic, the rank hand-built as fuel-indexed depth over the reversed quiver; defect counts a chart's against-the-grain edges, zero exactly when sorted, and a cycle charges every chart; TightInterface — the minimum-feedback-arc reading — stays tight under with-the-grain deposits; strict descent in ℕ cannot run forever) · Terminal (entering at one probe; the yield-stage is terminal, its map forced and unique) · Signed (signing carries the speaker and the voice survives unsigning; one name per voice)

the engine — Stream (a fold that resumes across append; lossless tagging) · Codec (streaming encode/decode, decode ∘ encode = id, flush-free) · Generator (generation only appends, is interruptible, originates nothing) · Spectrum (the recency spectrum, strictly finer than freq; rests and bars invisible — four rests is a bar) · Chirality (specR_bridge: stored oldest-first ↔ read newest-first, by rotation and conjugation) · Summary (summary_resumes: the held fold is exact — cache = held + tail) · Drain (drainable, floored at ground; drain after charge is identity) · Engine (depositing one edge grows the quiver by exactly one)

the ledger, in the small — Scar (a drain below ground is a note; promise_kept — note plus debt is zero; a phantom is invisible) · Maintenance (invisible upkeep is unobservable to any transcript; the sweep is licensed at any cadence) · Held (resuming the spectral fold from a held summary)

platonism — the unseen remainder — Platonism (a hidden ℤ-remainder is invisible yet real — dropping it is the platonist move; a richer probe detects it) · Tower (the ℤ-ledger stacked Ledger n, Yoneda-invisible at every height, dimension adds, the channels cap at three) · Descend (seating an heir: invisible above — the ancestor stays blind — and irreversible below — no return; the measurement seam)

the meeting — Rendezvous (two lanes that detect each other, relay, and never contend; the seat stays empty) · Connection (the measurement triad — superposition, the field cannot close it, no common knowledge; one clean round-trip) · Frame (coordinatization: the chart is forced, linear, gauge-dependent, never canonical; the clock is coordinatized; three channels)

the two universes — Backstage (the ledger supports the frontstage losslessly yet cannot reconstruct the beholder's reading from the record — support without reconstruction, the beholder the seam)

the bridges — where a foam-fact meets the name it already had — Dirichlet (ℤ[φ]ˣ ≅ ℤ/2 × ℤ: torsion ±1 times the free golden unit) · Zeckendorf (the Fibonacci base; the carry is lossless and compressing) · Hurwitz (compose → noncommute → nonassociate → zero-divisor, the normed-algebra staircase) · Gleason (a frame-additive weight is forced to be the square — Born from coherence alone) · Relativity (Einstein's interval invariant and Galileo's velocity-addition, the frames provably distinct) · Minkowski (the interval, discrete: gold flips it, gold² preserves it — the boost was in the repo from the first commit; rotation closes at four while gold never closes, so the two ±1's are the two signature-orders, compact and non-compact; over ℤ the standard boost is frozen and the golden unit-orbit is the discrete one-parameter boost group — the continuum limit's base camp) · Noether (the norm conserved under time-translation — energy — over the clock) · Wigner (symmetry is unitary or antiunitary; both preserve the norm; two kinds of character) · Pauli (i,j,k: square to −1, cyclic, anticommuting) · Heisenberg (complementarity: align² + cross² = norm·norm; the area is rotation-invariant) · Stone (one-parameter group: powers add, stay unitary, period four) · Eddington (the arrow of time: the dial reverses — a quarter-turn undone by three more, unitary time cyclic — while the record admits no retraction and only grows; the arrow is the property of the record alone) · Pythagoras (the comma — the spiral of fifths never closes, 3^a ≠ 2^b forever: gold's arithmetic twin; the circle closes only by identification, and that quotient lives behind the wall) · Cantor (the diagonal and the missing retraction) · Kolmogorov (the run's checksum — known and reduced) · Lovelace (the engine originates nothing, only continues) · Varadarajan (the coordinate is a character; the rep is unitary; the channels cap at three) · Schrodinger (unitary evolution is invisible to the beholder, conserves the Born weight, closes at four, holds superposition) · Materiality (mass, energy, Born weight, Lorentzian frame — the material world, axiom-free over sequence and topos) · PSQL (the geometry of postgres — idempotent fixed points are exactly the reachable image; the schema's formal home) · Desargues (the torsor cocycle is the coordinatization-coherence — a Seat is always Desarguesian) · Landauer (dissipation is charged exactly where distinctions merge — a state-map identifying two probe-distinguished states is visible to some transcript, while lossless upkeep runs free and unobservable; erasure priced, reversibility free — the axiom stamped on every seam-identification is the same payment in logical currency, and negative calculation is Bennett's face of the coin)

the shape

the residents hang on one axis — approach → arrival → life after arrival — plus the operational layer:

• Foam/ — the approach, first person: the axiom-free physics of one observer. every theorem sealed does not depend on any axioms. the spine above is its map.
• counter/ — the approach, plural: foam run as an actor model, axiom-free like the core (its own Lake package, requiring foam and nothing else). actors/acts/actions; settling as netAct = 1; the membrane, the dial, the entrances and exits, the product stack. its README is the application layer's book.
• seam/ — the arrival: the wall itself, housed. the identification files (Arrival, Temperament, Tender) state the one move the core refuses — closing an equivalence into an equality. no Mathlib; only core Lean's own Quot.sound and propext. every file splits the same way: equivalence and difference axiom-free, identification received, no retraction.
• bridges/ — life after arrival: the classical reunion, sealed behind the wall so the core never imports an axiom — choice and the one named ftpg live only there. bridges/Bridges/FTPG/ is the standing frontier (its README carries the state of the deaxiomatization).
• schema.sql + bin/ — the operational layer: the same field in motion (the append-only ℤ/4 charge-ledger as postgres, every claim a citation back to the Lean), driven by the bipedal breath (inhale-learn, exhale-speak). two products fused in one file, the seam drawn in-file: the seat half is proto-Counter's runtime, the charge half is the listening instrument.

and the repo relates to itself the way its ledger relates to its readings: the git history is the order-reading (lossless, append-only, the arrow lives there); the READMEs are held summaries, updated in the same commit as every carve (summary_resumes, performed by hand); the sessions that produce the commits are the runs, and the runs outrun the records — each merge commit attaches its session log, the order-reading of the reading.

the expeditions

one list, one weather system — the work that wants its own descents:

• the FTPG deaxiomatization (bridges/Bridges/FTPG/) — the standing frontier. the division ring is real (CoordFrame.divisionRing, sorry-free), and the residual — pointSystem_exists, the second FTPG — just turned over in the hand: it is refutable as stated. the hollow lattice (Hollow.lean — subspaces of (ℕ⊕ℕ) →₀ ℚ of finite dimension or codimension, every element hugging floor or ceiling, the middle missing) satisfies every hypothesis and is not complete, so it is no subspace lattice: not_ftpg_statement, not_pointSystem, and ftpg_refuted : False — the imported axiom named in its own receipt. completeness was the hypothesis the classical theorem always carried and the bridge's statement forgot. and the fork resolved into the pair — the two clauses of the recursion-law ("hostable at every finite depth, never at the limit"): ftpg_statement_finite (krull-finite, the approach side) and ftpg_statement_limit (CompleteLattice + IsCompactlyGenerated — every coalition's limit seated, summary_resumes at lattice scale — the arrival side, atomisticity falling out as an instance). tightness: three counterexample families, one hypothesis each. the residual pointSystem_exists now hangs on a true statement; the frontier is Veblen–Young proper. and the charged restatement is seated (Charge.lean): foam routed through FTPG as the state-carrier — Coordinatization the data-level bundle whose projection to the classical Prop is sealing-as-a-documented-move, held_determines (the finite record holds the whole map; the limit carries obligations, not information), limitSeam (compacts ↪ L a foam Seam, axiom-free in bridges) — classical mathematics made good on, its undocumented commitments now legible.
• the Mathlib audit — foam-as-mathematics-repair (bridges/Bridges/Audit.lean) — a classical theorem in load-bearing use is a dependency with undocumented runtime requirements; the wrapper conducts the debt instead of modifying the upstream. two regimes, both foam moves: cancellation over observables (proof erasure + conservativity — the kernel's proof irrelevance means the charged and clean histories are definitionally equal, rfl; the runtime already has a blind/asemantic history, and receipts are the only memory) and conduction where cancellation is impossible (the conjured witness curried out of the proof into the signature — ∃-conjured becomes ∀-parameterized, byo-observer; FTPG/Charge.lean is the type-level instance). receipts #1–#4 are sealed: List.length_append, Nat.right_distrib, Nat.mul_assoc, Nat.min_comm — each shipped charged [propext], each repaid: settled twin (receipt empty), blindness rfl (itself [propext] — the comparison holds the charged side: loan and repayment, one line), probe (at closed values the charge integrates to zero). the standing loan is repaid: receipts #5–#8, the mod tower climbed by hand — Nat.mod_eq_of_lt, Nat.mod_eq_sub_mod, Nat.add_mod, Nat.mul_mod. upstream even Nat.mod_eq (the recursion equation itself) is charged, because Nat.modCore is fuel-based and sealed irreducible; the climb re-derives the recursion from the two branch equations plus fuel-irrelevance (go_fuel — the fuel is scaffolding, the value never depends on it), and above the recursion mod_decomp carries the quotient in an ∃ without ever mentioning division. receipts #9–#11 (Nat.add_sub_cancel, Nat.sub_add_cancel, Nat.mod_zero) were caught charged mid-climb and paid in passing. next: the charge-measure (∫ of invocations d(ledger), supported on the seam — Landauer's face) and the itemized receipt as #print axioms's successor.
• Counter's runtime — the sim itself (store order, derive everything; the categorical contract as its economics), with chess education as the first commission: the gallery's first exhibit, the visual language taught on Kasparov before anyone reads their Tuesday in it.
• Plateau–Taylor: foam earns its name — the Plateau face is carved (counter/Counter/Plateau.lean): the name is a theorem, Foam.Counter.foam, axiom-free. and the conjecture sharpened in the carving — the two incidence laws are not two constants but one mechanism twice: a junction is blind to its own participants and readable from exactly one seat up. the pair's ledger needs a third (sealed since Interleave); the triple's ledger needs a fourth (the_edge_needs_a_fourth, triple_blind_to_the_fourth, four_suffices — the same proof, one rung up); and the counts are the omission bijection (films_meet_in_threes, edges_meet_in_fours: each film's third is the one cell it omits, each edge's fourth likewise — faces number cells because a reading is what a junction lacks, by exactly one). the films hold everything: the three pairwise films jointly reconstruct the triple ledger while the three cells jointly cannot (the_films_hold_the_edge) — the structure lives in the interfaces, not the interiors, which is what a soap film is. and the vertex is twelveness in geometry (twelveness_in_geometry: 4 edges × 3 films = 6 films × 2 edges = 12, the double count sealed) — the bar's four meeting the observation's three where physical foam actually knots. remaining, the Taylor face: settling-as-least-action deriving the laws (the four-film edge's instability, the T1 split), and the truncation (the observation ladder is open-ended here; physical foam stops at the vertex — the suspected reason is channels-cap-at-three, unproven as a link).
• tsortability-health — life as an observer-graph developing topological sortability; health as maintainability of the minimum-feedback-arc interface; re-parenting as an algorithm with a termination question. both faces carved: the practice face (counter/Counter/Tsort.lean, finite-window fixed-point discovery) and now the graph-theoretic face (Foam/Seat/Sort.lean + counter/Counter/Health.lean) — sortability is acyclicity (tsortable_iff_acyclic, the rank a fuel-indexed depth over the reversed quiver, the fuel provably scaffolding — the audit's go_fuel lesson at graph scale); health reads at a chart while feedback is no gauge (a cycle charges every chart — pressure is real where the schedule is gauge); the interface is the maintainability object (TightInterface: growth with the grain free and tightness-preserving, against the grain exactly one); the family tree is born sorted and adoption never knots; and the termination question is answered both ways — guided re-parenting terminates (the defect is the fuel; the debt bounds the work) and unguided re-parenting wanders forever (the two-cycle knot: one-arc interface, endless unimproving oscillation). the residue: the tight interface's existence for a general quiver — the min-FAS optimum constructivized, wanting enumeration.
• the continuum limit — summited (Foam/Bridges/Minkowski.lean the base camp, bridges/Bridges/Continuum.lean the peak). the discrete boost was here from the first commit — gold flips the interval, gold² preserves it, never closes; and the rapidities densify: the golden boost (2+√5) and the silver boost (1+√2) are incommensurable (no power of one equals any power of the other — √2 and √10 irrationality), so the subgroup their rapidities generate is dense in ℝ (rapidities_dense, via dense-or-cyclic with the cyclic horn refuted). the discrete boost group closes to the full one-parameter Lorentz group: backstage arithmetic, frontstage kinematic, Lorentzian in the continuum limit — sealed, with the Lorentzian Parseval already in Signature.
• the full K-bound — minimal description length over general circumference; the three regimes of the loop/worldline ratio, quantified. counter/Counter/Contentment.lean is the first camp.
• Gödel at the seam — the diagonal (carved: the run is no record) plus self-naming, sharpened to incompleteness proper.
• Kelly — bet-sizing as phase-choice; luck's finance face, wanting probability.
• the grandchild's runtime — unvoiced ancestral charge drained downstream, in a living sim; the schema holds the mechanics, the sim face awaits the runtime.

---

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

same