Cohomological Obstructions

Cohomology Classification

JuGeo uses the language of Čech cohomology on the semantic site \((\mathcal{C}, J)\) to classify descent failures. Given a covering family \(\mathcal{U} = \{U_i \to U\}_{i \in I}\) and the judgment sheaf \(\mathcal{F}\), the Čech complex is:

The cohomology groups \(\check{H}^n(\mathcal{U}, \mathcal{F})\) measure qualitatively different kinds of failure. JuGeo computes an approximation of these groups and assigns one of four obstruction degrees to each descent failure. Each degree corresponds to a distinct structural problem that requires a different remediation strategy.

Obstruction Class Fields

Every obstruction is represented as an ObstructionClass dataclass. The fields encode both the mathematical data (which degree, which cochain) and the engineering data (source locations, repair hints, backpressure score) needed to present actionable diagnostics to the developer.

Constructing and inspecting an obstruction manually:

from jugeo.geometry.descent import (
    CohomologyClass,
    DescentObstruction,
    OverlapCondition,
    OverlapStatus,
    RepairFrontier,
)

obs = DescentObstruction(
    coordinate="mymod.payments",
    violated_overlaps=(
        OverlapCondition(
            left_coordinate="mymod.payments.validate",
            right_coordinate="mymod.payments.charge",
            overlap_coordinate="mymod.payments.validate∩mymod.payments.charge",
            status=OverlapStatus.VIOLATED,
        ),
    ),
    repair_frontier=RepairFrontier(
        missing_evidence=("spec:payments-charge",),
        weakened_claims=("align validate/charge currency assumptions",),
    ),
    cohomology_class=CohomologyClass(
        cocycle_data={"validate∩charge": {"currency": {"left": "USD", "right": "EUR"}}}
    ),
)

print(obs.violation_count)
print(obs.violated_pairs())
print(obs.cohomology_class.cocycle_data)

Repair Frontiers

A repair frontier is the minimal set of code locations that, if modified, would eliminate a given obstruction. JuGeo computes repair frontiers by working backward from the obstruction through the antecedent DAG of judgments — finding the earliest points where an intervention would propagate forward and resolve the mismatch.

For H⁰ obstructions:

• The frontier is the set of functions or classes that lack the required local section.
• JuGeo suggests adding or strengthening a postcondition annotation, or fixing the implementation to satisfy the required property.
• Minimum effort: tighten the local claim, re-run jugeo prove, and inspect the new obstruction data.

For H¹ obstructions:

• The frontier is the set of call-sites where the caller's precondition disagrees with the callee's postcondition at an intersection.
• JuGeo suggests either: (a) strengthening the caller's precondition, (b) weakening the callee's postcondition, or (c) introducing a boundary adapter.
• The lowest-effort option is usually (a): restrict the inputs so both sides agree.

For H² obstructions:

• The frontier spans three components. JuGeo identifies which triple \((i, j, k)\) causes the triple intersection to fail and suggests a refactoring that separates the conflicting concerns.

Computing the frontier programmatically:

from jugeo.geometry.descent import RepairFrontier

frontier = RepairFrontier(
    missing_evidence=("runtime trace:payments.validate",),
    weakened_claims=("weaken charge() postcondition on accepted currencies",),
    suggested_refinements=("split payments cover into auth/charge",),
    estimated_cost=2.5,
)

print(frontier.total_items())
for category, item in frontier.prioritized_items():
    print(category, item)

Backpressure System

An obstruction at a low-level utility function does not exist in isolation — every function that depends on that utility inherits an unresolved antecedent obligation. JuGeo's backpressure system quantifies this propagation by assigning a score \(\beta \in [0, 1]\) to each obstruction that measures how broadly its effects cascade through the semantic site.

Edge weights \(w(f)\) depend on the morphism kind: direct call edges carry weight 1.0, import/module edges 0.5, and containment edges 0.8. Scores are normalised to \([0, 1]\) across the full obstruction report and displayed in the jugeo prove CLI output.

JuGeo recognises five canonical backpressure families, each suggesting a different response:

Python Examples

Querying the obstruction report for a module:

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

cover = Cover(
    target=Coordinate("payments", kind=CoordinateKind.MODULE),
    patches=(
        Coordinate(("payments", "validate"), kind=CoordinateKind.FUNCTION),
        Coordinate(("payments", "charge"), kind=CoordinateKind.FUNCTION),
    ),
    overlaps=(("payments/validate", "payments/charge"),),
)

sections = {
    "payments/validate": {"currency": "USD", "status": "ok"},
    "payments/charge": {"currency": "EUR", "status": "ok"},
}

result = DescentEngine().run(cover, sections).to_descent_result()
obstruction = result.unwrap_obstruction()

print(obstruction.violation_count)
print(obstruction.violated_pairs())
print(obstruction.cohomology_class.cocycle_data)

Attempting automatic repair:

import subprocess

        completed = subprocess.run(
            ["python3", "-m", "jugeo", "--format", "json", "repair", "payments.py"],
    check=True,
    capture_output=True,
    text=True,
)

print(completed.stdout)

Inspecting the Čech cochain directly:

cohomology = obstruction.cohomology_class

print(cohomology.dimension)
print(cohomology.rank)
print(cohomology.is_trivial())
print(cohomology.cocycle_data)