Federation: the DEFAULT layer joins as a constituent

Area: Standpoints & federation Teaches: the DEFAULT (unscoped) layer is not a privileged outer frame that overrides standpoints — it is a join constituent on equal footing. Because the DEFAULT layer restricts into every scoped view, a DEFAULT-asserted fact and a scoped refutation of the same individual collide inside one standpoint’s view, and the four-valued join yields both. Prerequisites: standpoint visibility and federation: when standpoints disagree. Run: ox build examples/federation_default_conflict && ox query examples/federation_default_conflict --with-truth4

The visibility example showed that a DEFAULT-layer fact restricts into every view — its agreement case. This example pins the disagreement case, and it is the subtle one. A single standpoint’s view is DEFAULT ∪ own. So when DEFAULT asserts a fact and the standpoint refutes it, both polarities live in the same view, and the information-join produces both — even though only one standpoint is federated. DEFAULT does not win by virtue of being the base; it participates in the join like any other source.

What to read in conflict.ar

One standpoint, with DEFAULT-layer facts above it:

pub type Person;

pub standpoint s;

// DEFAULT-layer (unscoped) facts — restrict into the scoped view `s`.
pub fact Person(eve);
pub fact Person(frank);

The standpoint refutes one of the DEFAULT facts, and refutes a third individual DEFAULT is silent on:

pub standpoint s {
    // `s` refutes the DEFAULT-layer `eve` — a same-view collision → Both.
    pub not_fact Person(eve);
    // `s` refutes `gwen`, on whom DEFAULT is silent → Not.
    pub not_fact Person(gwen);
}

Federating over the single standpoint still meets the DEFAULT layer — s’s view is DEFAULT ∪ s:

pub query conflicting() -> Person across [s];

Running it

Even across a single standpoint, the DEFAULT layer is a constituent, so the join surfaces three different verdicts:

eve    → Both   (DEFAULT asserts Person, s refutes — both meet in s's view)
frank  → Is     (DEFAULT asserts, s silent)
gwen   → Not    (s refutes, DEFAULT silent)

The decisive row is eve → Both. There is only one standpoint in across [s], so it is tempting to read DEFAULT as an outer context that s overrides — it is not. The DEFAULT assertion of eve and s’s refutation of eve are two constituents of one join, and the join holds both. Contrast frank (Is — DEFAULT alone) and gwen (Not — s alone): the verdict is exactly the information-join of whatever each layer contributes, with DEFAULT counted, never privileged.

Honest caveats (what runs today)

• This is the same paraconsistent federation policy as the two-source case: collisions are preserved as Both, not resolved in DEFAULT’s favor.
• Rows are reported by individual id; the name mapping above is how the package declares its facts.

This example is compiled and run in CI; the DEFAULT-disagreement verdicts (eve = Both in particular) are pinned by a corpus test (oxc-runtime/tests/examples_corpus.rs), so the equal-footing join rule can’t drift.

Source

The package’s real Argon source, transcluded from the files this corpus compiles — what you read here is exactly what CI builds.

root.ar

//! Federation: the DEFAULT layer and a scoped layer disagree.

mod conflict;

conflict.ar

//! Federation: the DEFAULT layer participates as a join constituent
//! (rsn-05). Pins the newly-introduced behavior the review's probe
//! surfaced: under the sheaf reading (§10.4) the DEFAULT (unscoped,
//! file/module-level) layer restricts into EVERY scoped view, so a
//! DEFAULT-layer `pub fact` and a scoped `pub not_fact` over the same
//! individual COLLIDE inside the single scoped view — the FDE
//! info-join yields `Truth4::Both`. DEFAULT is not a privileged outer
//! frame that overrides standpoints; it is a constituent that joins on
//! equal footing.
//!
//! This is deliberate and consistent with
//! `Argon.Visibility.scoped_view_eq_default_union_own` (the scoped view
//! is `DEFAULT ∪ own standpoint`): when DEFAULT asserts and `own`
//! refutes, the view holds both polarities. The four-quadrant matrix
//! (`standpoint_visibility`) pins DEFAULT *agreement* (a DEFAULT fact is
//! visible everywhere); this example pins DEFAULT *disagreement*.
//!
//! Expected runtime behavior (`across [s]`):
//!
//!   eve   — Truth4::Both  (DEFAULT asserts Person, s refutes)
//!   frank — Truth4::Is     (DEFAULT asserts, s silent)
//!   gwen  — Truth4::Not     (s refutes, DEFAULT silent)
//!
//! Soundness: `Argon.Standpoint.AFTEquivalence.aft_discharges_T3_obstruction`
//! (the per-tuple Truth4 classification the federated dispatcher computes)
//! and `Argon.Visibility.scoped_view_eq_default_union_own` (DEFAULT ∪ own).

pub type Person;

pub standpoint s;

// DEFAULT-layer (unscoped) facts — restrict into the scoped view `s`.
pub fact Person(eve);
pub fact Person(frank);

pub standpoint s {
    // `s` refutes the DEFAULT-layer `eve` — a same-view collision → Both.
    pub not_fact Person(eve);
    // `s` refutes `gwen`, on whom DEFAULT is silent → Not.
    pub not_fact Person(gwen);
}

// Federated over the single standpoint `s`: its view is DEFAULT ∪ s, so
// the DEFAULT assertion and s's refutation of `eve` meet here.
pub query conflicting() -> Person across [s];