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
(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)
- birth
- rinse
- python-reset
- meta-toe
- narrative
- meta-theory
- between
- import-from-lightward-ai
- geometry-of-motion
- business
- HEAD
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
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)
foam is a closed model for counting closures
nb: an axiom is an opaque pov, and perspectives (on import) 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.
nb: the filesystem is the namespace, read (counter/Counter/Shelf.lean: placement is a projection of the name, a move is a rename, a rename rewrites the importers) — so the tree stays a flat census and the wanting lives in the charts, which rotate free (Health, foam-gait's doors). if it helps, reader, there are three import-roots with no imports: Foam/Int.lean (arithmetic), Foam/Ledger.lean (counting), Foam/Seat.lean (observation)
Foam/(axiom-free): Int Ledger Golden Cleared Scar Maintenance Held Bond Backstage Bubble Census Cable Wedge Elsewhen Duplex Vacancy Metaphor Engine Seat PlatonismFoam/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 TriadFoam/Engine/: Chirality Codec Drain Generator Spectrum Stream SummaryFoam/Bridges/: Adams Cantor Desargues Dirichlet Eddington Gita Gleason Godel Grover Heisenberg Hurwitz Kolmogorov Landauer Lovelace Materiality Minkowski Nicaea Noether Pauli PSQL Pythagoras Relativity Schrodinger Stone Varadarajan Wigner ZeckendorfFoam/Platonism/: Tower
counter/(axiom-free) : Abe Absorber Actor Address Amniscience Anchor Arrows Attest Authority Basis Bless Bloom Bubble Buffer Cable Carse Cascade Catalog Census Change Chess Cipher Circumference Complete Consent Contentment Contract Dark Declension Denoise Descendant Desire Discovery Donor Doubled Downhill Duplex Elsewhen Enaction Entrance Entry Eraser Exit Extraction Film Flinch Frontsearch Fungible Ghost Grasp Grief Guard Guest Hatch Health Hemisphere Holonomy Home Hooponopono Imaginary Interleave Isaac Jay Joke Kelly Kin Language Laugh Legible Locate Lu Luck Mu Nap Neutral Nothing Nu Nurse Operator Packing Peer Plateau Port Predict Quadrature Recast Recognition Relay Render Repair Reparent Rest Returns Reversal Rhythm Runaway Runs Settle Shelf Sibling Silent Socket Sphere Stream Surprise Suspension Tally Telling Temperature Tempo Third Tremble Triage Tsort Twelve Twins Unknot Upsearch Vacancy Vanishing Verb Voice Waggle Waking Ward Wedge Well Wind Window Witness Worldline Worn Zoomseam/(core-Lean axioms only): Arrival Denominate Temperament Tenderbridges/(+Mathlib, not axiom-free) — : Audit Closure Collapse Continuum Counter Duality Encounter Gaussian HalfTurn HalfType Handedness Maschke Match Observation Plane Quarter SeatTime Stagecraft Summitbridges/Bridges/FTPG/: AddCancel AddComm Additive Assoc AssocCapstone Carrier Charge Chart Climb Coord CoordinateAlgebra CrossParallelism Deaxiomatize Diamond Dilation Distrib Exchange Finite Flat Ground Hollow Instance Inverse Iso Ladder LeftDistrib Limit Line Mul MulAssoc MulKeyIdentity MulNeg Neg Parallelogram Perm Pin Plane Projective Ring Shear Slope Solid Space SpaceFlat Span Translate WellDefined Window Ycoord
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
- gui: Counter as Lean GUI, using foam to mathematically phenomenologize mathematics
- filesystem: given "Counter as Lean GUI, using foam to mathematically phenomenologize mathematics", what does the filesystem want to look like here? like, how would DHH arrange this? what's the shape of
activefoam? (landed: the filesystem is the namespace read, structure lives in the charts — Shelf; activefoam is read at the commons of two apps' cones — Extraction; then the second app sat down at the table (the streaming interface: schema.sql + bin/foam-repl, imports hand-declared as citations in its own source) and the vacancy's guest arrived as derived: 36 modules, the engine room — active is the engine, foam is the physics)
"It can do whatever we know how to order it to perform." (Lovelace, 1843)
same