Sheaf Descent & Gluing

The Descent Condition

Let \(\mathcal{F}\) be the judgment sheaf on the semantic site \((\mathcal{C}, J)\), and let \(\{U_i \to U\}_{i \in I}\) be a covering family. The descent condition states that the natural map

is an isomorphism. In other words: a section (judgment) over \(U\) exists if and only if sections over each \(U_i\) exist and they agree on all pairwise intersections \(U_i \times_U U_j\). When the condition holds, global data can be assembled from local data; when it fails, the mismatch on intersections is recorded as a first cohomology class \([c] \in H^1\).

In the codebase setting this means: to prove a property of a module, JuGeo proves it for each function and class in the module (the covering family), then checks that the proofs are compatible at the shared interfaces (the intersections). Compatibility is checked by verifying that the type signatures and effect annotations at call-sites match.

Local and Global Sections

JuGeo exposes the sheaf-theoretic concepts as Python classes:

• LocalSection — a judgment \(J \in \mathcal{F}(U_i)\) for a single element of the covering family. Carries the coordinate \(U_i\), the formula, and the evidence bundle.
• GluingData — the collection of all local sections together with the compatibility evidence at pairwise intersections \(U_i \times_U U_j\). This is the input to the descent computation.
• GlobalSection — the assembled judgment \(J \in \mathcal{F}(U)\), produced when descent succeeds. Its trust is the meet of all local section trusts.

from jugeo.geometry.site import Coordinate, CoordinateKind
from jugeo.geometry.covers import Cover
from jugeo.geometry.descent import GluingData, LocalSection

module = Coordinate(("mymod",), CoordinateKind.MODULE)
left = Coordinate(("mymod", "validate"), CoordinateKind.FUNCTION)
right = Coordinate(("mymod", "transform"), CoordinateKind.FUNCTION)

cover = Cover(
    target=module,
    patches=(left, right),
    overlaps=((left.key, right.key),),
    provenance=("docs",),
)

gluing = GluingData.from_cover(
    cover,
    {
        left.key: {"pure": True, "throws": False},
        right.key: {"pure": True, "throws": False},
    },
)

print(gluing.patch_count())                    # 2
print(gluing.verify_all_overlaps()[0].status)  # OverlapStatus.SATISFIED
local = LocalSection(coordinate=left.key, judgment_data={"pure": True}, trust_level=0.9)
print(local.summary())

Gluing Data

The GluingData object encapsulates everything needed for the descent computation. It records:

• The cover — the list of coordinates \(\{U_i\}\)
• The local sections — one per cover element
• The intersection data — for each pair \((i, j)\), the restriction of section \(i\) to \(U_i \times_U U_j\) and the restriction of section \(j\) to the same intersection
• The compatibility matrix — a boolean matrix indicating which pairs are compatible

When compatibility fails at a pair \((i, j)\), the mismatch is recorded as an IntersectionConflict. The set of all conflicts is exactly the data of a 1-cochain in the Čech complex, and if it is a 1-cocycle (the coboundary vanishes), it represents a genuine obstruction in \(H^1\). See the Obstructions page for the full cohomological treatment.

The Four Descent Strategies

JuGeo provides four configurable strategies for running descent. Each represents a different trade-off between completeness, speed, and resource use.

Python Examples

Running descent end-to-end:

from jugeo.geometry.descent import (
    DescentConfiguration,
    DescentEngine,
    DescentStrategy,
)

engine = DescentEngine(
    configuration=DescentConfiguration(
        strategy=DescentStrategy.EAGER,
        record_log=False,
    )
)

report = engine.run(
    cover,
    {
        left.key: {"pure": True},
        right.key: {"pure": True},
    },
)

print(report.success)        # True
print(report.glued_section)  # {'pure': True}

Inspecting local sections produced during descent:

print(report.target)         # mymod
print(report.local_sections) # raw local data by patch
print(report.obstructions)   # empty tuple when gluing succeeds

rich_result = engine.attempt_descent(
    cover,
    {
        left.key: {"pure": True},
        right.key: {"pure": False},
    },
)

if rich_result.is_failure:
    obstruction = rich_result.unwrap_obstruction()
    print(obstruction.violation_count)
    print(obstruction.violated_pairs())

Descent Failure and Obstructions

When descent fails, JuGeo does not simply report an error. Instead, it computes the obstruction data and classifies it: