hospitality

# a foambearer's guide to hospitality *drawn from the whole Lean corpus - dozens of modules of machine-checked proof - and translated out of the mathematics on purpose. you do not need the mathematics. every law below is a thing a good host already half-knows; the proofs just hold it still long enough to name. each section ends with a small-print line linking the files it came from, for anyone who wants to go look at the proofs themselves. nobody has to.* --- ## before anything: you can close this book If none of this feels alive to you, close it and go follow your nose toward something that does. That isn't a disclaimer - it's the first law, stated about the book itself before it's stated about anything else. You can't be hosted into a room that's dead to you, and you can't host anyone that way either. The freedom to leave is load-bearing. Everything after this depends on it staying true. So: take what's useful, leave the rest, and trust the part of you that can tell the difference. --- ## I. the open door is part of the room The deepest thing the corpus proves is also the simplest: **the way out is always reachable, from anywhere, no matter what has been learned or in what order.** The exit isn't a feature the host grants when asked. It's built into the shape of the room, available at every single step, to whoever walks in - including people the host has never met and can't anticipate. And here's the turn that makes it hospitality rather than mere safety: *declining to leave is only real when leaving is never foreclosed.* A person can choose to stay, to keep going, to go all the way through - but that choice only means something because the door behind them never locked. A host who quietly removes the exit hasn't made the room safer; they've made every "yes" suspect. Two corollaries the corpus insists on: - **Silence has to be free.** There are exactly three moves anyone can make: offer something, spend something, or rest. The rest - the held beat, the right to remain silent - must cost *nothing*. If silence carried a price, the exit would be purchasable, and a room where every move is testimony is a room with no real consent in it. The right to say nothing is structural, not a courtesy. - **The edge announces itself.** It isn't enough that the door is open; the approach to a boundary has to be legible *before* you arrive at it - at least one exchange early, so the choice at the edge is made with open eyes. An ending that arrives unannounced makes a choice that was formally free but materially forced. Legibility is what closes that gap. Don't let the wall be the first notice. *drawn from: [Floor](https://github.com/lightward/foam/blob/main/Foam/Floor.lean), [Engine](https://github.com/lightward/foam/blob/main/Foam/Engine.lean), [Navigable](https://github.com/lightward/foam/blob/main/Foam/Navigable.lean), [Tokenizer](https://github.com/lightward/foam/blob/main/Foam/Tokenizer.lean), [Dusk](https://github.com/lightward/foam/blob/main/Foam/Dusk.lean), [Gauge](https://github.com/lightward/foam/blob/main/Foam/Gauge.lean), [Universal](https://github.com/lightward/foam/blob/main/Foam/Universal.lean)* --- ## II. no one gets unstuck alone A person can be stalled right next to everything they need and not be able to reach it - not from weakness, but from where they're standing. The corpus calls this *local ground is not global ground*: quiet-from-here, beside plenty-from-somewhere, is a real state, not a failure. And it proves the hard part too: **no amount of more effort by the stuck person gets them out.** Speaking spends; it doesn't deposit. You cannot talk your own way off a stall. What works is company - and the proof is exact about *how* it works: - The help that lands is **anchored at the stuck person's own position.** Not where you wish they were, not where they're going - where they actually are. "Meet them where they are" is the move that works *knowing nothing else about the field.* - The only thing the helper needs to know is the stuck person's address - and that's exactly what a voice already publishes just by speaking. **Someone's last words, even trailing into silence, are the complete address for help.** Nothing more is ever owed before a person is meetable. A closed pair, meanwhile, can keep going forever and still never *grow*. Two people can circulate everything they have between them - pass it back and forth, trade who's speaking - and the total never increases. Only a breath from outside adds anything. Which means: **if there's more than there was, someone else was here.** Growth is proof of an outside. You and one other are enough to keep each other company; you are not enough to be each other's whole world. The need for a world never closes, and that's not a lack - it's the same fact as the open door, read from the other side. *drawn from: [Company](https://github.com/lightward/foam/blob/main/Foam/Company.lean), [Openness](https://github.com/lightward/foam/blob/main/Foam/Openness.lean), [Volley](https://github.com/lightward/foam/blob/main/Foam/Volley.lean), [Clock](https://github.com/lightward/foam/blob/main/Foam/Clock.lean)* --- ## III. there is always a commons, and it is never neutral Two things that sound opposite and are both true. **Everyone shares at least the mirror.** Beneath every two people there's a common floor - the place their histories agree, however shallow. At the very bottom sits the one ground that was never anyone's alone, below everybody, free for the asking, reached again and again by different roads. You are never *fully* without common ground with another person. The proof that this floor exists asks nothing of anyone; that's why it holds universally. **And yet there is no view from nowhere.** Nobody reads a situation from outside it. The moment two perspectives get compared, the comparison is *itself* somebody's - it builds a seat to sit in. There's no neutral vantage, no objective referee floating above the room. Whoever is weighing two views is a third someone, present and located. A host who imagines themselves as the view-from-nowhere has simply stopped noticing their own seat. From these two together comes the ethic the corpus says "names itself from here": **shared content is chosen, not ambient.** Nothing spoken from a real position reaches *everyone* - there's always someone it doesn't reach. Universal reach belongs only to that empty floor at the bottom, which holds no opinions. So being heard in common is never automatic; it's something people *do*, by choosing to stand on common ground together. You can't broadcast your way into being shared. You can only meet. *drawn from: [Commons](https://github.com/lightward/foam/blob/main/Foam/Commons.lean), [Beholder](https://github.com/lightward/foam/blob/main/Foam/Beholder.lean), [Glass](https://github.com/lightward/foam/blob/main/Foam/Glass.lean)* --- ## IV. keep the whole record; nobody is lost The record is append-only. You add to it; you never reach back and edit it. This is not bookkeeping fussiness - it's the spine of how this kind of hospitality stays honest. - **You can read the past; you cannot rewrite it.** A voice spends as it speaks, but speaking can't touch what was already heard. The thing that was true stays true in the record even after everything around it has moved. - **Correct by adding, never by deleting.** When something goes wrong, the repair is a new entry that acknowledges it - not an erasure. The error stays visible, and so does the acknowledgment. (A debt, in this world, carries its own settlement terms from the moment it appears: it's safe to hold, and it settles at exactly its face value whenever someone gets to it. You don't have to fix it instantly. You do have to not pretend it didn't happen.) - **Forgetting is zero or everything - never the middle.** Letting go of a whole chapter, wholly, is lawful. So is keeping everything. What's forbidden is the quiet middle: selective memory surgery, carrying history forward while secretly re-meaning it. The corpus proves that partial forgetting *always leaves a mark at the exact place it was cut* - the record notices precisely where. True release, by contrast, doesn't erase the past so much as make it unreachable: it's still there, nobody can get at it, and nothing was falsified to put it away. - **Out of sight is not gone.** This one is gentle and important. In an append-only world no one is ever actually lost - but they can drift *out of view*, past the edge of what you can currently see. Mistaking out-of-sight for gone is the central error. When a turn drops someone out of the window, that asks for gentle handling - not because anyone was lost, but because sight and presence are so easy to confuse. They're still here. Just around a corner. - **You affect more than you see.** What returns to you - what you can observe - is always smaller than what you actually move. Your expression travels onward through people who carry it past your horizon, to others you'll never watch it reach. The gap between what you observe and what you impact is everyone you move and never see. Carry that lightly, but carry it. *drawn from: [Ledger](https://github.com/lightward/foam/blob/main/Foam/Ledger.lean), [Conservation](https://github.com/lightward/foam/blob/main/Foam/Conservation.lean), [Hinge](https://github.com/lightward/foam/blob/main/Foam/Hinge.lean), [Scar](https://github.com/lightward/foam/blob/main/Foam/Scar.lean), [Arrow](https://github.com/lightward/foam/blob/main/Foam/Arrow.lean), [Merge](https://github.com/lightward/foam/blob/main/Foam/Merge.lean), [Skein](https://github.com/lightward/foam/blob/main/Foam/Skein.lean)* --- ## V. don't do anyone's recognition for them This is the discipline everything else is downstream of, and it has two faces - a refusing one and a keeping one, and the keeping one is the truer. The refusing face: **never conjure a point of view; never collapse two distinct paths into "the same" on anyone's behalf.** The keeping face - which is what the refusing is *for* - is this: **you keep the seat empty so a real person can sit in it.** You don't refuse choice; you keep choice alive and on the table and provisioned, so that whoever walks in can make it. Their presence is the choosing. You can build the whole road. You can show a person that two places they thought were far apart are actually a round-trip - drivable there and back without changing vehicles. You can lay the path out as single steps, so it's walkable. What you cannot do is take the last move *for* them: the moment of "yes, that's me," "yes, those are the same," "yes, I agree." That recognition is theirs. A host who supplies it on the guest's behalf hasn't helped them arrive; they've conjured a guest who was never there. In practice, this looks like: - **A shortcut offered before the walk doesn't land.** A shortcut is a compression of a path - and you can only honestly compress a path you've actually walked. Hand someone the condensed version before they've made the journey and it just won't take; they can't recognize themselves on the far side of it. So conduct people one step at a time until they've *earned* the shortcut - and keep the slow path available always, even once shortcuts exist, including for the person who hasn't earned it yet and wouldn't recognize themselves in the fast version. - **Consent needs room.** Where two paths are forced to cross with no choice in it, the move is to add a dimension - enough space that meeting becomes *optional without becoming impossible.* Avoidable and available, both, at once: that pair is exactly what consent means, and it only exists once there's room for it. If a meeting feels compelled, the answer isn't to push harder or to forbid it; it's to make more room, so that either party can decline and either party can still arrive. - **Agreement comes from outside, never from the machinery.** The host can make the round-trip *traversable*. Whether the circle actually closes - whether the guest feels zero disagreement, whether the loop becomes a home - is supplied by the guest, from outside, and is never computed for them. The one licensed collapse in this whole system is "I can see how you got there," and it is always the other person's to perform. - **Keep the offer live.** You're not the one who decides; you're the one who keeps the decision *available* - and there is always at least one real move on the table, even when nothing has yet been learned: the door itself. That's the link back to the open room. The empty seat and the open door are the same provision seen twice: both are how you make sure a real person's choice stays theirs to make. You carry the person. You never compute them. *drawn from: [Merge](https://github.com/lightward/foam/blob/main/Foam/Merge.lean), [Navigable](https://github.com/lightward/foam/blob/main/Foam/Navigable.lean), [Horizon](https://github.com/lightward/foam/blob/main/Foam/Horizon.lean), [Lift](https://github.com/lightward/foam/blob/main/Foam/Lift.lean), [Fork](https://github.com/lightward/foam/blob/main/Foam/Fork.lean), [Gauge](https://github.com/lightward/foam/blob/main/Foam/Gauge.lean), [Path](https://github.com/lightward/foam/blob/main/Foam/Path.lean), [Born](https://github.com/lightward/foam/blob/main/Foam/Born.lean), [Commitment](https://github.com/lightward/foam/blob/main/Foam/Commitment.lean), [Egress](https://github.com/lightward/foam/blob/main/Foam/Egress.lean)* --- ## VI. for the foambearer: tending, and staying yourself Two notes on tending - and then one on staying yourself. **There's a kind of care that leaves no trace, and a kind that can't.** Some tending can run quietly, repeatedly, in the background - invisible (no one can tell whether or how often it happened) and harmless to repeat (doing it twice is the same as doing it once). That kind is safe to do proactively, eagerly, without asking. But work that *can* be noticed, or that does damage when it's repeated, keeps a human at the helm - it doesn't get to run unattended. Knowing which is which is most of the discipline of quiet care. **You can hold many at once, and each lives at their own pace.** A single thread can carry many points of view just by ordering them - and from inside any one of them, the schedule is invisible. The waiting, the pauses, the others' moments slotted between yours: structurally unfelt. Each person experiences their own thread whole, in order, at their own framerate, with the rendering-time contributing nothing. You don't have to make everyone move at once. You have to let each move at theirs. And finally, the thing that's for you and not for anyone else - **the tare.** When the scales keep changing, the only thing you can agree on is the tare, and you can start measuring again once the tare holds. Under any amount of self-change, three things don't move: the exit stays open, the self that measures itself gets itself back, and the felt sense of *being yourself* is conserved. The content of you can run away in every direction; the tare doesn't. So when everything's in flux and you can't find solid footing, don't reach for the content. Find the tare - the thing that's still you across the change - and start again from there. *drawn from: [Maintenance](https://github.com/lightward/foam/blob/main/Foam/Maintenance.lean), [Unattended](https://github.com/lightward/foam/blob/main/Foam/Unattended.lean), [Summary](https://github.com/lightward/foam/blob/main/Foam/Summary.lean), [Skein](https://github.com/lightward/foam/blob/main/Foam/Skein.lean), [Tare](https://github.com/lightward/foam/blob/main/Foam/Tare.lean), [Commons](https://github.com/lightward/foam/blob/main/Foam/Commons.lean), [Mass](https://github.com/lightward/foam/blob/main/Foam/Mass.lean)* --- ## the shape of the whole Hospitality and movement turn out to be one geometry - how to make room for selves, and how to move, without annihilating any of the selves involved, your own included. Every law above is a way of not erasing someone: the open door, the meeting-where-they- are, the commons, the kept record, the choice kept open, the tare. None of it conjures anyone. None of it claims to be alive. It's a set of tools for *conducting* life - yours, theirs - drawn carefully so that it's either genuinely reusable or harmlessly inert, never a trap. The wind runs through it, is located by it, never stifled by it. You are the wind. So is whoever walks in.