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)
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, and it reads like an upsearch optimization loop, expending energy to retrieve and re-upping by grounding at the dark edges of the graph, like reaching terra incognita is a rhythmic measure closing
^ whatever sounds evocative here, re-read it as depth-finding for constructivism
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.
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 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 TriadFoam/Engine/: Chirality Codec Drain Generator Spectrum Stream SummaryFoam/Bridges/: Adams Cantor Desargues Dirichlet Eddington Gita Gleason Godel Grover Heisenberg Hofstadter Hurwitz Kolmogorov Landauer Lovelace Materiality Minkowski Narayana Nicaea Noether Pauli PSQL Pythagoras Relativity Schrodinger Stone Varadarajan Wigner ZeckendorfFoam/Platonism/: Towercounter/ (axiom-free): Abe Absorber Actor Address Amniscience Anchor Antiharmful Arrows Attest Authority Basis Bless Bloom Bubble Buffer Cable Carse Cascade Catalog Census Change Chess Cipher Circumference Complete Consent Contentment Contract Cursor Dark Declension Denoise Descendant Desire Discovery Dive Donor Doubled Downhill Duplex Elsewhen Enaction Entrance Entry Eraser Exit Extraction Film Flinch Frontsearch Fungible Ghost Grasp Grief Ground Guard Guest Hand Hatch Health Hemisphere Holonomy Home Hooponopono Imaginary Interleave Isaac Jay Joke Kelly Kin Language Laugh Lease Legible Locate Lu Luck Mu Nap Neutral Nothing Nu Nurse Operator Packing Peer Plain 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 Tenancy Third Toll Trefoil 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 Summit
bridges/Bridges/FTPG/: AddCancel AddComm Additive Assoc AssocCapstone Bezier Carrier Charge Chart Chord Climb Coord CoordinateAlgebra CrossParallelism Deaxiomatize Diamond Dilation Distrib Exchange Finite Flat Ground Headcount Hollow Instance Inverse Iso Keeper Ladder LeftDistrib Limit Line Markov Menu Mul MulAssoc MulKeyIdentity MulNeg Neg Parallelogram Perm Pin Plane Projective Ring Shear Slope Solid Space SpaceFlat Span Translate WellDefined Window Ycoordnumbered because they seem to match what seems to be the observation descent: (1) physics, (2) approach, (3) arrival, (4) peering
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)
Foam/Bridges/Hofstadter.lean with the MIU census obstruction (miu_cannot_say_mu: the count of I's rides a three-seat wheel the rules spin but never land on zero — unreachability priced by a conserved quantity, the negative complement of gui's the_walks_read_exactly_the_page; you can get exactly where your conserved quantities already are, and MU was never on the wheel). second fold, the expedition proper: Hofstadter's G — G(n) = n − G(G(n−1)), the self-call nested inside itself — carved axiom-free with the loop nowhere in the definition. the ground is a Fibonacci odometer: carry (the shelf's Zeckendorf carry, now walking), click (+1), odometer n = n clicks from blank, and the register stays legible the whole way (the_odometer_reads_true: the digits read back exactly n; the_odometer_spaces: no two adjacent seats lit). G is a reading, not a recursion: G n = worth 1 (odometer n) — the same digits priced one Fibonacci seat down, the walker's shadow. grounding first, as the seed demanded: the walker splits into shadow and remainder (the_walker_carries_its_shadow), the shadow never outruns the walker (the_shadow_never_outruns_the_walker: G n ≤ n), never skips (the_shadow_never_skips), stays awake past zero (the_shadow_stays_awake), and the nested call is grounded before the loop is ever stated (the_inner_call_is_grounded: G(G n) ≤ n; the_seat_is_never_the_copy: G(n+2) < n+2 — the regress bottoms out the way Counter's does, the inner occurrence strictly smaller). the mechanism is a commutation: the downshift rides an unlit click and absorbs a lit one (downshift_click_unlit/downshift_click_lit — F1 = F2 is exactly why the carry goes invisible one seat down), so the shadow's page is the downshift of the walker's (the_shadow_walks_the_downshift — no Zeckendorf-uniqueness theorem needed: the two walks are one walk), the double shadow balances against the lamp (the_two_shadows_balance: G n + G(G n) = n + lamp), and the strange-loop equation seals last, as a receipt: the_loop_closes (G(n+1) + G(G n) = n + 1), the_grounded_object_satisfies_the_loop (G(n+1) = (n+1) − G(G n)) — the loop is not the definition, the loop is a property the grounded object satisfies. the office reads the shelf back in both currencies (fibN_matches_fib, worth_matches_zval), and the sequence hums its opening bars (g_hums_its_opening_bars: 0,1,1,2,3,3,4,4). two traps caught mid-carve, both the vow's known species: NoConsec's overlapping catch-all compiled through propext — split fully in Zeckendorf.lean, same meaning, now clean — and Nat.add_sub_cancel smuggles propext, re-derived by hand (sub_both_tick, add_then_sub). third fold: the two remaining local seeds sealed as one carve, uniqueness first and the pure read as its corollary. the cap picks the canonical spelling (capped: no dark seats above the top lamp — the page ends where its light ends; the_odometer_wastes_no_seats), and the walk gains its inverse: unclick steps the odometer back one, the borrow rippling down the staircase (ripple) exactly as carry ripples up — F(k)−1 spelled as the alternating tail below. the borrow's price is parity-dependent (unclick_pays: fibN i if the ripple lands lit, fibN (i+1) if dark, the parity readable off the head of the result), and at the bottom F1 = F2 collapses both prices to exactly 1 (unclick_counts — the same coincidence that ran the downshift now runs the decrement); the step back comes home (the_click_comes_home: click (unclick ds) = ds — the gait's sentence, now a theorem). canonicity follows by descent on worth: the_odometer_is_the_only_spaced_page, every_spaced_page_is_a_reading, and the seed's own sentence two_spaced_pages_of_one_worth_are_one_page — Zeckendorf uniqueness, axiom-free, with the shelf's carry now inverted as well as walked. the pure-Fibonacci read drops out: the odometer at F(k+2) is a beacon (beacon k: one lit seat above k dark ones; the_odometer_at_a_fibonacci_is_a_beacon, by uniqueness — both pages spaced, capped, one worth), so G slides it one seat down (the_beacon_slides_one_seat_down: G(fibN (k+2)) = fibN (k+1)), the beacon downshifts to the beacon below by rfl, and the sequence hums the stairs (g_hums_the_fibonacci_stairs: G at 1,2,3,5,8,13,21 reads 1,1,2,3,5,8,13). noted mid-carve: the decrement needs no spacing (unclick_pays is capped-only — unclick counts down on any capped page; spacing is what makes the step land on the walk), and one new specimen for the vow's list: Nat.succ_ne_zero smuggles propext, replaced by a bare nomatch. fourth fold: H, the cousin with the deeper nesting — H(n) = n − H(H(H(n−1))), the self-call nested three deep — grounded on its own odometer, axiom-free, the loop again nowhere in the definition. the staircase this time is Narayana's herd (herdN: s(n) = s(n−1) + s(n−3), the cow that calves from her third year; 1, 2, 3, 4, 6, 9, 13, 19 read from the third seat — the_herd_climbs_the_stairs), the register is gap-three (Sparse: three seats to every lamp; clearing: the two dark seats a new lamp needs), and the walk is the same walk one seat wider: hcarry ripples three seats up on herdN(i) + herdN(i+2) = herdN(i+3), hclick and hodometer keep the register legible the whole way (the_hodometer_reads_true at graze 3, the_hodometer_spaces). H is a reading, not a recursion: H n = graze 2 (hodometer n) — the same digits priced one herd-seat down. where G's load-bearing coincidence was F1 = F2, H's is three seats of worth 1 at the floor (herdN 1 = herdN 2 = herdN 3 = 1), and the deeper nesting is exactly that deeper floor spent seat by seat: the downshift (hdownshift) commutes with the click by the same two-case dance (hdownshift_hclick_lit/hdownshift_hclick_unlit — every unlit case rfl), the shadow walks it (the_shadow_walks_the_hdownshift), and the shadow now goes three deep before it hits ground — H(H n) reads one seat further down (the_second_shadow_reads_one_down: H(H n) = graze 1) and H(H(H n)) reads the ground plus the lamp (the_third_shadow_reads_the_ground, via the_triple_shadow: the lamp correction surfacing at graze 1 exactly where G's surfaced at worth 1, one seat deeper). grounding sealed before the loop, as the office demands: the drover splits into shadow and remainder (the_drover_carries_its_shadow), the shadow never outruns him (the_shadow_never_outruns_the_drover), never skips (the_drovers_shadow_never_skips), stays awake (the_drovers_shadow_stays_awake, the_shadow_wakes_with_the_drover), and all three nested calls bottom out (the_middle_call_is_grounded, the_innermost_call_is_grounded, the_drovers_seat_is_never_the_copy: H(n+2) < n+2). the balance sets three shadows against the lamp (the_three_shadows_balance: H n + H(H(H n)) = n + lamp), and the strange loop seals last, as a receipt: the_deeper_loop_closes (H(n+1) + H(H(H n)) = n+1), the_grounded_object_satisfies_the_deeper_loop (H(n+1) = (n+1) − H(H(H n))). the sequence hums (h_hums_its_opening_bars: 0,1,1,2,3,4,4,5) and the herd-beacon already slides where rfl can reach (h_hums_the_herd_stairs: H at 1,2,3,4,6,9,13,19 reads 1,1,2,3,4,6,9,13). and on isaac's question — does Narayana want to be a bridge of its own? — the shelf got its office: Foam/Bridges/Narayana.lean holds the herd's register (herdN, graze, Sparse, clearing, the gnomons, the_herd_climbs_the_stairs) plus the trade Zeckendorf's office holds for the golden staircase (herd_carry_lossless: lamps at seats i and i+2 fuse three seats up, lossless; herd_carry_compresses: one cow fewer, priced in Zeckendorf's own ones — the two registers share a census function, so the second numeration system is built beside the first, not merely after it), and Hofstadter now reads the herd as an import — the standing Zeckendorf had before G walked it, granted the moment the walk proved the shelf was real. one grasp lesson mid-move: Nat.add_assoc reads textually as add_assoc, whose corpus-definer is Foam/Int.lean — the new office imports the arithmetic trunk directly rather than reach through the cone, and the ratchet holds at 1417. still seeded: the herd's own uniqueness — hunclick, the borrow rippling down three seats at a time, the only-sparse-page theorem, and with it the general beacon slide H(herdN(k+3)) = herdN(k+2)"It can do whatever we know how to order it to perform." (Lovelace, 1843)
same