RFD 0008 — Standpoint-Sheaf Equivalence Proof Roadmap

• State: committed (Path A landed)
• Opened: 2026-05-28
• Path A landed: 2026-05-29 — Argon/Standpoint/AFTEquivalence.lean mechanizes the discrete T3 obstruction equivalence (aft_discharges_T3_obstruction proven).
• Decides: the proof obligation, viable proof paths, and arc structure for elevating standpoint-sheaf equivalence from “axiomatized / open research” to mechanically proven in Lean.

Question

Standpoint logic (Gómez Álvarez & Rudolph 2021) and sheaf cohomology (Abramsky & Brandenburger 2011) independently formalize multi-perspective knowledge. The conjectured equivalence between them — “a set of standpoint axioms has a consistent global merger iff the associated sheaf has trivial H¹” — is currently axiomatized in Argon’s Lean mechanization, with AGENTS.md noting it as “open research.”

Should Argon push to prove this equivalence, and what’s the right proof path?

Context

Why this matters strategically

The competitive audit identified federation across standpoints as Argon’s most distinctive feature — no other production language has it as a first-class primitive. The current Lean mechanization proves a Finset-based version (Argon/Locality/SheafEquivalence.lean: grounded MCS equilibrium = minimal global section over module DAGs). This is operationally useful but does not connect to the broader logical-topological equivalence the literature poses.

Without the broader proof, Argon’s federation claim is “the runtime computes equivalent results to a sheaf model under our axiomatic embedding.” With the proof, the claim becomes “the runtime computes a sheaf model — and we know precisely when and how the model breaks.”

The user has designated this a worldclass objective. The vault’s “Standpoint-Sheaf Dictionary” note carries the conjectured translation table. This RFD makes the proof obligation concrete.

What’s already proven

In Argon/Locality/SheafEquivalence.lean (~180 lines, lake-green):

• Theorem 1 (bottom-up computation → equilibrium): definitional.
• Theorem 2 (equilibrium → global section): from local_fp inclusion.
• Theorem 3 (equilibrium is minimal global section): from local_fp being a least fixpoint.

These cover a BeliefAssignment (function ModId → Finset Atom) with generic bridge and local_fp operators. The acyclicity of the module DAG is required.

Adjacent mechanization (Argon/Standpoint/Federation.lean) proves the FDE bilattice info-join (federate_eq_both_iff, strictFold_preserves_inK3) — the AFT-side analogue of “cross-source disagreement detection.”

What’s NOT proven

The three sub-theorems forming the conjecture:

Decision

Pursue the proof in three escalating proof paths, each independently shippable.

Path A — AFT-only restatement (lowest risk, ~600 LOC) — LANDED 2026-05-29

The existing Foundation/Federation.lean’s federate_eq_both_iff is already the bilattice-algebra-side analogue of “H¹ ≠ 0 detects contextuality.” T3 is restated in AFT terms:

federate contribs = .both ↔ no global K3-section exists

This makes T3 a corollary of existing mechanized work. T1 and T2 are not discharged in this path — we lose the cohomological diagnostics (cocycle witnesses, spectral solver) but keep the soundness story.

Cost (actual): 1 new file Argon/Standpoint/AFTEquivalence.lean (~225 LOC including docstrings). One iteration through Lean’s cases/split_ifs tactics.

What landed:

• SheafClassification inductive: consistentTrue / consistentFalse / undetermined / obstructed.
• sheafClassify : List Truth4 → SheafClassification — direct semantic over federate.
• aft_discharges_T3_obstruction (proven): sheaf-obstructed ↔ federate contribs = .both. The load-bearing theorem; the AFT-side analogue of “H¹(F) ≠ 0 detects contextuality.”
• sheafClassify_consistentTrue_iff, sheafClassify_consistentFalse_iff, sheafClassify_undetermined_iff — three companion characterizations.
• sheafObstructed_iff_disagreement_or_explicit_both — composes the above with federate_eq_both_iff for the diagnostic-surface-shaped form.
• sheafClassify_singleton, sheafClassify_empty — base cases.

What this ships: a named theorem in Lean asserting “Argon federation = AFT-bilattice-based cross-source consistency.” Bridges the existing operational federation runtime to a categorical-flavored claim.

Path B — Frame-theoretic (medium, ~1200 LOC)

Replace the Grothendieck topology with the simpler structure of a complete Heyting algebra (frame) of standpoint-downsets. Mathlib has Order.Heyting.Basic and Topology.Sheaves.Sheaf over locales. Bridge rules become frame homomorphisms.

This discharges T1 routinely (frames induce topologies; standpoint-downsets form a frame canonically) and T2 (frame homomorphisms preserve gluing). T3 still requires work but on more familiar ground than full Grothendieck descent.

Estimated cost: ~1200 LOC. ~6 weeks.

What it ships: a partial proof of the equivalence — the topology induction and the bridge-rule-as-restriction-map sides, with T3 stated as a theorem schema parameterized over the localic sheaf machinery.

Net gain over Path A: the equivalence is now bidirectional (Argon → sheaf AND sheaf → Argon round-trip), not just embedding.

Path C — Full Grothendieck (highest, ~2000 LOC)

Mathlib has CategoryTheory.Sites and Grothendieck topologies. Construct the topology directly; prove T1, T2, T3 via descent.

The genuinely novel obstacle: connecting Hansen-Ghrist’s sheaf Laplacian diffusion (proved for vector-space stalks) to Argon’s lattice-valued knowledge requires either a box-embedding (Garcez-Lamb) relaxation or a discrete cohomology theorem. This is open research; no published work bridges it.

For the equivalence itself, this gap is not blocking — the equivalence can be discrete on the lattice side. But the computational payoff (spectral solver, cohomological diagnostics) depends on it.

Estimated cost: ~2000 LOC. ~12 weeks for the equivalence; the spectral bridge is a separate research effort.

What it ships: a research paper. Independent value beyond Argon’s runtime needs.

Recommended sequencing

1. Arc N+1 (this RFD): Path A. ✅ Landed 2026-05-29. Discharges the immediate Argon claim (“federation is sound under AFT info-join, which is the bilattice-algebra-side analogue of the sheaf claim”). Closes the wire-clean version of the worldclass objective.

2. Arc N+2 (follow-on): Path B. Lifts to frame-theoretic, discharging T1 + T2 + a parameterized T3. The equivalence becomes bidirectional.

3. Arc N+3 (research-paper track): Path C. Full Grothendieck. Separately publishable; not on the Argon roadmap critical path. Bridge to continuous diffusion is a deferred research obligation.

Paths A and B compose: Path A’s theorems are corollaries of Path B’s. Path B’s theorems are corollaries of Path C’s. Each arc strictly strengthens the previous.

Rationale

Why three paths rather than one

Path C is what the literature poses. Path A is what we can ship next week. Path B is the sweet spot. Allowing all three to live in the roadmap acknowledges that:

• Argon’s runtime needs the operational claim (Path A) now.
• The mathematical claim worth defending publicly (Path C) is research-scale.
• The intermediate (Path B) delivers most of the value with mathlib4’s existing infrastructure.

Why not just ship Path C and skip the intermediates

Path C’s continuous-discrete bridge is a genuine open problem. If we commit to Path C exclusively, the roadmap is hostage to one unproven research result. Splitting into three paths means each is independently shippable; if Path C stalls on the continuous-discrete bridge, Paths A and B are unaffected.

Why the AFT-only path counts as discharging the worldclass objective

The vault’s “Standpoint-Sheaf Dictionary” note maps:

• federate contribs = .both ↔ “irreducible disagreement”
• K3-fragment containment ↔ “global section exists”

federate_eq_both_iff already proves this in Argon/Standpoint/Federation.lean. Restating it as the canonical sheaf-equivalence theorem under the AFT lens IS the worldclass deliverable for Argon’s runtime semantics, operationally. The Grothendieck topology proof is the categorical deliverable, with mathematical content beyond the runtime claim. Both are worth pursuing; Path A satisfies the worldclass objective for Argon-as-a-language; Path C satisfies the worldclass objective for Argon-as-a-publishable-research-contribution.

Alternatives considered

Alt 1: leave the equivalence axiomatized

Mark the three sub-theorems as axiom declarations with citations to Gómez Álvarez & Rudolph 2021 and Abramsky & Brandenburger 2011. AGENTS.md permits cited axioms. Cost: zero. Risk: the runtime claim depends on the citations being correct.

Rejected per user strategic clarification: “we should absolutely push for a proper proof and make sure that it’s world-class.”

Alt 2: ship only the AFT-only path

Land Path A; declare the categorical claim out of scope. Cost: ~600 LOC. Risk: ceiling-bound; the federation story remains “operational only,” with no path to spectral / cohomological diagnostics.

Rejected as too narrow. The user designated this worldclass; a worldclass deliverable includes the mathematical claim, not just the operational one.

Alt 3: ship Path C exclusively

Commit to the full Grothendieck construction; treat A and B as intermediate steps not worth landing independently.

Rejected: the continuous-discrete bridge is a research gap with no published solution. Risking the roadmap on it is unwise. Splitting into three paths lets each ship independently.

Consequences

Lean changes (per arc)

• Arc N+1 (Path A): ~600 LOC. New file Argon/Standpoint/AFTEquivalence.lean. Extends Federation.lean with the canonical theorem statement.

• Arc N+2 (Path B): ~1200 LOC. New file Argon/Standpoint/FrameEquivalence.lean. Depends on mathlib4 Order.Heyting.Basic + Topology.Sheaves.Sheaf.

• Arc N+3 (Path C): ~2000 LOC. New file Argon/Standpoint/SheafEquivalence.lean (NOT the existing Locality/SheafEquivalence.lean, which proves the discrete Finset form). Depends on mathlib4 CategoryTheory.Sites. Spectral bridge is a separate research effort.

Reference book changes

§11 (Standpoints and federation) gains a new subsection citing this RFD’s three theorems as the soundness foundation. Currently §11.x reads as informal motivation; after Path A lands, it can cite the mechanized theorem directly.

Runtime impact

Path A: none. Federation runtime continues to use AFT info-join; the equivalence theorem is a soundness claim about it.

Path B: enables across[] queries to use frame-homomorphism preservation as a static guarantee. Diagnostic surface gains an “irreducible disagreement: cocycle on edges {…}” message under H¹ obstruction.

Path C: enables sheaf Laplacian diffusion as an alternative federation evaluator (spectral solver for acyclic module DAGs). Spec gain λ₁-spectral-gap as a federation cost metric.

Citation registry

Each path adds named theorems whose proof obligations cite specific prior work. The citation list (book §22 references) gains:

• Gómez Álvarez, S. & Rudolph, S. (2021). Standpoint Logic: Multi-Perspective Knowledge Representation. (Path A, B, C)
• Abramsky, S. & Brandenburger, A. (2011). The Sheaf-Theoretic Structure of Non-locality and Contextuality. (Path B, C)
• Hansen, J. & Ghrist, R. (2020). Opinion Dynamics on Discourse Sheaves. (Path C, spectral bridge)
• Mac Lane, S. & Moerdijk, I. (1992). Sheaves in Geometry and Logic. (Path C foundations)
• Denecker, M., Marek, V., Truszczyński, M. (2000). Approximation Fixpoint Theory. (Path A AFT side)

Open questions

• Continuous-discrete bridge for stalks. Hansen-Ghrist’s diffusion convergence is proved for vector-space stalks. Argon’s modules use lattice-valued knowledge. No published work bridges them. Path C’s spectral payoff depends on resolution; the equivalence itself does not. Is the spectral-bridge worth a dedicated research effort, or accept the discrete cohomology theorem?

• Cocycle diagnostic surface. Under H¹ obstruction, what does the modeler see? “Irreducible disagreement on bridges {b1, b2, b3}” with a cycle witness? Diagnostic ergonomics design.

• Functorial canonicity of T1. Classical topology literature has Grothendieck constructions for modal Kripke frames, but no published canonical induction for standpoint orders. Path C may require an originality contribution here.

• MLT-style multi-level stalks. Standpoints can carry metatypes (a standpoint’s knowledge includes higher-order classifications). Whether sheafification respects MLT order arithmetic is unaddressed in the literature. Defer to MLT std library RFD.

• Defeasible bridges. Bridge rules can themselves be defeasible (per Argon’s defeasibility substrate). Does the sheaf framework absorb Governatori-Rotolo +Δ/-Δ proof tags as graded restriction maps? Open.