Standpoints and federation

Standpoints

A standpoint is a named viewpoint. Items declared inside a standpoint s { … } block belong to s and are addressed as s::Item. Standpoints form a lattice ordered by <: — California <: USFederalTax places California below federal tax in the lattice. The order declares federation membership, the set a query may draw across; it is not namespace inheritance, so a child standpoint sees a parent’s items only through an explicit use. The reference fixes the surface under standpoints and federation.

A fact asserted inside a standpoint block is local to that standpoint. A not_fact is strong negation — an explicit denial, not the mere absence of an assertion. Two registries can hold flatly contradictory records:

pub standpoint historical {
    pub fact Person(alice);
    pub fact Person(bob);
}

pub standpoint public_record {
    pub not_fact Person(alice);
    pub not_fact Person(carol);
    pub fact Person(dave);
}

Federation

across [...] on a query federates the listed standpoints. Federation is the information-join of the four-valued logic: for each individual it combines what every standpoint says, and where two disagree the join is both. A query that federates the two registries above returns four answers — Alice both (asserted by historical, denied by public_record), Bob is (asserted once), Carol not (only ever denied), and Dave is (asserted once). Disagreement becomes a value the caller can match on, not a crash and not a silent choice of winner. The Lean characterizes exactly when the join is both (federate_eq_both_iff over the infoJoin of the Truth4 carrier).

This is the one place both arises. A single standpoint, evaluated on its own, stays within is, not, and can; only federation across disagreeing standpoints produces conflict. Federation conflict policy is chosen per query, not per standpoint: a federated query is paraconsistent by default, surfacing both, and may instead request a strict projection.

Visibility

A standpoint also bounds what a query can see, and the rule is a sheaf reading of scope. A fact declared at module scope — outside any standpoint block — sits in the default layer and restricts into every view. A fact declared inside a standpoint is local and visible only by selecting that standpoint. So an unfederated query reads exactly the default layer; across [s] reads the default layer unioned with s’s own facts; across [s1, s2] info-joins those per-standpoint views.

Four queries over one default-layer widget and two standpoint-local ones separate the cases cleanly. The default-layer dfl appears in all four. A query scoped to s1 adds only_s1; a query scoped to s2 adds only_s2; neither local fact leaks into the other’s view or into the unscoped base. The unscoped base returns one row, each single-standpoint view two, the federation across both three. Cross-standpoint reads require explicit federation; a scoped fact never silently becomes global truth, and derive rules, checks, and the mutation delta-guard all evaluate over the default-layer view. A federated query naming a standpoint with no declaration is refused rather than contributing an empty extent that would mask the typo.

The sheaf reading is exact. Treat the standpoint lattice as a space and assign each open set the knowledge available to the standpoints in it. The default layer is a global section — it restricts to every open set, which is why an unscoped fact is visible everywhere. A standpoint-scoped fact is a local section — defined only on its own open set. Irreducible disagreement, the both outcome, is the obstruction to gluing local sections into a global one: it lives in a first cohomology that no global section can flatten. The Lean proves the visibility laws directly (view_of_base_eq_default_layer, scoped_view_eq_default_union_own, and the three (in)visibility lemmas) and proves the federated system’s bottom-up evaluation is an equilibrium that is a minimal global section of the sheaf (bottom_up_is_equilibrium, equilibrium_is_global_section, equilibrium_is_minimal_section), over a finite model with no axioms. The full categorical construction — a genuine Grothendieck topology with general restriction maps — is open research; the finite-model theorems are what the substrate commits to.

Bridge rules

Where across [...] composes standpoints lattice-wise, a bridge rule moves a conclusion in one direction between two standpoints, optionally through a domain mapping — a directional, named, typed inference rather than a symmetric join. A bridge from s₁ to s₂ does not imply one from s₂ to s₁; that asymmetry is what keeps bridges from collapsing standpoints into equivalence and erasing their separation.

The design is committed and the surface is real: bridge declarations parse, lower to the wire format, resolve, and pass well-formedness checks. The federation fixpoint does not yet fire them, so a built artifact’s bridge bodies would never contribute to their target. Rather than ship that inert surface, a pub bridge is refused loudly at ox check and ox build (OE1102); model the cross-standpoint inference with an explicit derive or fact until evaluation lands. The parse, lower, and wire path is kept intact so the work resumes without a grammar or format change.