Mathematical Background
A self-contained introduction to the mathematics of Judgment Geometry — a new field synthesizing sheaf theory, cohomological obstruction theory, and formal logic to give proof-carrying Python verification a rigorous geometric foundation.
1 Sheaves and Sites
The language of sheaves on sites provides the geometric backbone of JuGeo. We recall the essential definitions, emphasising the axioms that will reappear — sometimes in disguise — throughout the system.
1.1 Categories
A category \(\mathcal{C}\) consists of:
- a class of objects \(\Ob(\mathcal{C})\),
- for each pair \(X, Y \in \Ob(\mathcal{C})\) a set of morphisms \(\Hom_{\mathcal{C}}(X, Y)\),
- a composition law \(\circ : \Hom(Y,Z) \times \Hom(X,Y) \to \Hom(X,Z)\),
- for each object \(X\) an identity morphism \(\id_X \in \Hom(X,X)\),
satisfying associativity and the unit laws:
1.2 Presheaves
A presheaf on a category \(\mathcal{C}\) is a contravariant functor
Explicitly, \(\mathcal{F}\) assigns to each object \(U \in \Ob(\mathcal{C})\) a set \(\mathcal{F}(U)\) (the sections over \(U\)), and to each morphism \(f : V \to U\) a restriction map \(\mathcal{F}(f) : \mathcal{F}(U) \to \mathcal{F}(V)\), written \(s \mapsto s|_V\), satisfying \(\mathcal{F}(\id_U) = \id\) and \(\mathcal{F}(g \circ f) = \mathcal{F}(f) \circ \mathcal{F}(g)\). The category of all presheaves is denoted \(\PSh(\mathcal{C})\).
1.3 Grothendieck Topology
A classical topology on a space \(X\) is determined by its open sets. Grothendieck's insight was that the essential structure is not the sets but the covering relations between them — a much more flexible notion, applicable even to categories with no underlying point set.
A Grothendieck topology \(J\) on \(\mathcal{C}\) assigns to each object \(U\) a collection \(J(U)\) of covering sieves (equivalently, families of morphisms \(\{U_i \xrightarrow{f_i} U\}_{i \in I}\)) satisfying three axioms:
- Identity The singleton family \(\{\id_U : U \to U\}\) is always a covering family.
- Stability If \(\{U_i \to U\}_{i}\) is a cover and \(V \to U\) is any morphism, then the pullback family \(\{U_i \times_U V \to V\}_{i}\) is a cover of \(V\).
- Transitivity If \(\{U_i \to U\}\) is a cover and for each \(i\) we have a cover \(\{V_{ij} \to U_i\}_{j}\), then the composite family \(\{V_{ij} \to U\}_{i,j}\) is a cover of \(U\).
A site is a pair \((\mathcal{C}, J)\) of a category \(\mathcal{C}\) equipped with a Grothendieck topology \(J\). We write \(\Site\) for the 2-category of sites.
1.4 Sheaves and the Equaliser Condition
A presheaf is a sheaf if local data that agrees on overlaps glues uniquely to global data. This is captured by an equaliser diagram in \(\Set\).
A presheaf \(\mathcal{F} \in \PSh(\mathcal{C})\) is a sheaf for the topology \(J\) if for every covering family \(\{U_i \xrightarrow{f_i} U\}_{i \in I}\) the canonical map
is an isomorphism. Here the two parallel arrows send a family \((s_i)_i\) to \((s_i|_{U_i \times_U U_j})_{i,j}\) and \((s_j|_{U_i \times_U U_j})_{i,j}\) respectively. The full subcategory of sheaves is denoted \(\Sh(\mathcal{C}, J)\).
2 The Semantic Site of a Program
Judgment Geometry's first fundamental construction is to regard a Python program \(P\) not merely as syntax but as a geometric object — a site \(\mathcal{S}_P\) whose opens are code coordinates and whose covers encode control-flow decompositions.
2.1 Code Coordinates as Objects
The coordinate stratum of a program \(P\) is the ordered set
with the partial order given by containment (\(\mathtt{expression} \le \mathtt{branch} \le \mathtt{function} \le \cdots\)). An object \(c \in \Ob(\mathcal{S}_P)\) is a pair \((n, \sigma)\) where \(n\) is a node in the abstract syntax tree (AST) of \(P\) and \(\sigma \in \Sigma\) is its stratum.
2.2 Morphisms: Restriction, Inclusion, Transport
Three families of morphisms generate the site \(\mathcal{S}_P\):
2.3 Covering Families
The Grothendieck topology \(J_P\) on \(\mathcal{S}_P\) declares the following families to be covers:
The semantic site of a program \(P\) is the site \(\mathcal{S}_P = (\mathbf{AST}(P), J_P)\). A semantic sheaf on \(\mathcal{S}_P\) is a sheaf \(\mathcal{F} \in \Sh(\mathcal{S}_P)\).
3 The Judgment 4-Tuple
A judgment in JuGeo is not a bare proposition but a rich geometric object living on the semantic site. It packages a verified claim together with its epistemic provenance — the channel of evidence, the trust level, and the cohomological obstructions that remain.
A judgment is a 4-tuple
where each component carries the following meaning:
| Symbol | Type | Meaning |
|---|---|---|
| \(\mathbb{S}_{\mathrm{top}}\) | Semantic Topos | Semantic Topos. The site, Grothendieck topology, sheaf topos, and internal logic. Subsumes the old coordinate \(c\) and proposition \(\varphi\). |
| \(\mathbb{P}_{\mathrm{str}}\) | Proof Structure | Proof Structure. Contexts, types, terms, and derivation trees. Subsumes the old carrier type \(A\) and evidence bundle \(E\). |
| \(\mathbb{C}_{\mathrm{spec}}\) | Cohomological Spectrum | Cohomological Spectrum. Covers, Čech complex, cohomology groups, and obstruction classes. Subsumes the old obligations \(O\) and obstruction classes \(B\). |
| \(\mathbb{G}_{\mathrm{eval}}\) | Graded Evaluation | Graded Evaluation. Grade semiring, quantale, evaluation functor, and trust algebra. Subsumes the old trust annotation \(T\) and provenance \(\Pi\). |
3.1 Restriction Maps on Judgments
The assignment \(c \mapsto \Jud_c\) (the set of all judgments at \(c\)) extends to a presheaf \(\Jud : \mathcal{S}_P^{\op} \to \Set\). For a morphism \(f : V \to U\), the restriction \(J|_V := \Jud(f)(J)\) is given componentwise by
where \(\varphi|_V\), \(A|_V\), \(E|_V\), \(O|_V\), \(B|_V\) are the images of the respective components under the restriction maps of their individual sheaves, and \(\Pi\) gains the morphism \(f\) as a provenance record. The trust level \(T\) is invariant under restriction — evidence cannot gain trust by localisation.
4 Sheaf Descent and Gluing
The central algorithmic problem of JuGeo is gluing: given local verifications of each branch, loop body, or call-site, does there exist a single coherent global verification? The sheaf condition answers this precisely, and descent theory provides the machinery to compute the answer.
Let \(\{U_i \xrightarrow{f_i} X\}_{i \in I}\) be a covering family in \(\mathcal{S}_P\), and let \(\{J_i\}_{i \in I}\) be a compatible family of judgments, i.e. a family satisfying the compatibility condition
Then the sheaf condition for \(\Jud\) guarantees the existence of a unique global judgment \(J \in \Jud_X\) such that
Moreover, the trust level of the glued judgment satisfies \(T(J) \preceq \min_{i} T(J_i)\), i.e. the global judgment cannot exceed the minimum trust of the local data.
4.1 Descent Data and the Descent Category
One can re-package Theorem 4.1 in terms of descent data. Define the descent category \(\mathbf{Desc}(\{U_i\}, \Jud)\) to have as objects compatible families \((J_i, \phi_{ij})\) where \(\phi_{ij} : J_i|_{U_{ij}} \xrightarrow{\;\sim\;} J_j|_{U_{ij}}\) are the coherence isomorphisms on the double intersections \(U_{ij} := U_i \times_X U_j\), satisfying the cocycle condition on triple intersections \(U_{ijk}\):
The sheaf condition says precisely that the canonical comparison functor
is an equivalence of categories. In JuGeo this equivalence is computed: the engine attempts to construct descent data from local verification results and, when it succeeds, extracts the global judgment.
5 Čech Cohomology of Obstructions
Verification does not always succeed. When it fails, JuGeo does not merely report an error: it classifies the failure} using the first Čech cohomology group. This classification tells the developer why gluing failed and, often, how to repair it.
5.1 The Čech Complex
Let \(\mathcal{F}\) be an abelian sheaf on \((\mathcal{C}, J)\) and let \(\mathfrak{U} = \{U_i \to U\}_{i \in I}\) be a covering family. The Čech complex \(\check{C}^\bullet(\mathfrak{U}, \mathcal{F})\) is the cochain complex
where
and \(\delta^p\) is the alternating sum of the face restriction maps. The Čech cohomology groups are \(\check{H}^p(\mathfrak{U}, \mathcal{F}) := H^p(\check{C}^\bullet(\mathfrak{U}, \mathcal{F}))\).
5.2 Cohomological Interpretation of Failure Modes
| Group | Interpretation in JuGeo |
|---|---|
| \(\check{H}^0\) | Global sections — verification succeeded. The judgment glues. |
| \(\check{H}^1\) | Primary obstruction. Failure to glue local verifications across intersections. Classifies pairwise incompatibilities. |
| \(\check{H}^2\) | Secondary obstructions. Arise when pairwise compatibility holds but triple-intersection consistency fails — e.g. non-associativity of state merges. |
| \(\check{H}^p,\; p \ge 3\) | Higher obstructions, typically zero for programs with bounded nesting depth (by acyclicity of the AST). |
Let \(\{J_i\}\) be a family of local judgments. If the compatibility condition of Theorem 4.1 fails, there is a canonically-defined obstruction class
such that \(\Delta = 0\) if and only if the family is compatible, i.e. gluing is possible. When \(\Delta \ne 0\), its cohomology class encodes the precise failure mode:
- Its support identifies the intersections \(U_{ij}\) where incompatibility occurs.
- Its image in \(\Ext^1\) groups classifies the type of conflict (data-flow, control-flow, heap aliasing, etc.).
5.3 Repair Frontiers as Chain Homotopies
A repair of a failed gluing is a modification of some local judgments \(J_i \leadsto J_i'\) that eliminates the obstruction. In cohomological terms, a repair is a chain homotopy \(h : \check{C}^0 \to \check{C}^{-1}\) that trivialises \(\Delta\):
JuGeo's repair engine searches for minimal-cost chain homotopies in a cost-weighted complex, where the cost of changing \(J_i \leadsto J_i'\) is measured by the trust-level drop \(T(J_i) \ominus T(J_i')\) in the trust algebra. This gives repair a natural optimisation formulation over the geometry of \(\check{H}^1\).
6 The Trust Ordered Algebra
Different evidence channels carry different epistemic weight. A Lean proof term is more trustworthy than an LLM attestation; an SMT certificate is more trustworthy than a random test. JuGeo internalises this hierarchy as a formal algebraic structure \(\mathfrak{T}\), the trust algebra, so that trust flows through computations in a principled, auditable way.
The trust algebra is the structure
where:
| Component | Description |
|---|---|
| \(\mathcal{E}_{\mathrm{adm}}\) | The set of admissible trust levels — a finite poset with elements ranging from Verified (Lean proof) down through Solver, Runtime, Oracle, Copilot, to Unverified. |
| \(\preceq\) | The partial order on \(\mathcal{E}_{\mathrm{adm}}\), with \(\mathtt{Unverified} \preceq \mathtt{Copilot} \preceq \cdots \preceq \mathtt{Verified}\). |
| \(\oplus\) | Composition (join). Commutative, associative, idempotent — the conservative join law \(t_1 \oplus t_2 = \min(t_1, t_2)\) ensures trust never silently increases. |
| \(\ominus\) | Attenuation (meet-like operation). Formalises the trust cost of a repair step; \(t_1 \ominus t_2\) is the trust deficit incurred by demoting evidence of level \(t_2\) within a context of level \(t_1\). |
| \({\uparrow}_\pi\) | Promotion. Promotes a judgment's trust by providing a certificate \(\pi\) of higher type (e.g. upgrading a runtime check to a solver certificate). |
| \({\downarrow}_\chi\) | Demotion. Attenuates trust by a context restriction \(\chi\), used when a verified fact is used in a less-trusted context. |
6.1 The Conservative Join Law
The single most important algebraic law is:
This is precisely the pessimistic join: the trust of a combined judgment is limited by its weakest component. An SMT-verified branch combined with an LLM-attested branch yields only LLM-level trust for the whole, because the weakest link governs.
6.2 The No-Silent-Promotion Theorem
Let \(J = (c, \varphi, A, E, O, B, T, \Pi)\) be any judgment and let \(f : V \to U\) be any morphism in \(\mathcal{S}_P\). Then
Furthermore, if \(\{J_i\}\) is a compatible family with global gluing \(J\), then \(T(J) = \bigoplus_i T(J_i) = \min_i T(J_i)\). In particular, no operation in JuGeo can increase the trust level of a judgment without providing a certificate of the target trust level.
6.3 The Trust Tower
The admissible trust levels form a chain (a totally ordered subset of the poset \(\mathcal{E}_{\mathrm{adm}}\)):
Each level corresponds to a class of evidence: \(\mathtt{Verified}\) requires a complete Lean proof term; \(\mathtt{Solver}\) an SMT refutation certificate; \(\mathtt{Runtime}\) an exhaustive test witness or property-based test; \(\mathtt{Oracle}\) a trusted external assertion; \(\mathtt{Copilot}\) an LLM-generated assertion; \(\mathtt{Unverified}\) unchecked hypotheses.
7 Cut Admissibility
In proof theory, cut elimination is the fundamental normalisation theorem: every proof using the cut rule can be transformed into a cut-free proof. In JuGeo the analogous result — cut admissibility — guarantees that intermediate lemmas can be inlined without changing the trust level of the conclusion.
7.1 The Cut Rule for Judgments
Write \(\Gamma \vdash J\) for "the context \(\Gamma\) of judgments entails judgment \(J\) on the semantic site." The cut rule asserts:
In the judgment calculus of JuGeo, the cut rule is admissible: any derivation using Cut can be mechanically transformed into a cut-free derivation of the same conclusion at the same or higher trust level. Formally, there is a trust-level-preserving algorithm
with \(T(\mathrm{elim\_cut}(d)) \succeq T(d)\) for every derivation \(d\).
- Principal case: when \(A\) is introduced by the last step in \(\Gamma \vdash A\) and consumed by the first step in \(\Gamma, A \vdash J\), the cut is directly eliminated by composing the two derivations along their shared formula.
- Left-commutative case: when \(\Gamma \vdash A\) ends with a rule that does not introduce \(A\), the cut is permuted past that rule.
- Right-commutative case: symmetric to the above.
7.2 Cut Elimination as Proof Normalisation
The practical consequence of Theorem 7.1 is that JuGeo's verification engine can freely use intermediate results (verified helper judgments) without fear of trust contamination. A lemma verified at \(\mathtt{Solver}\) level can be used in a proof that aims for \(\mathtt{Verified}\) level, provided that the lemma itself is subsequently upgraded. Cut elimination computes the normalised proof in which all intermediate steps are at the appropriate level.
Every cut-free derivation satisfies the sub-formula property: every formula appearing in the derivation is a sub-formula of a formula in \(\Gamma \cup \{J\}\). Equivalently, the derivation contains no "detours" through auxiliary propositions.
8 Connections to Classical Mathematics
Judgment Geometry does not stand in isolation. It is a synthesis of ideas from category theory, algebraic geometry, proof theory, and programming-language semantics. This section makes the connections precise.
Abstract Interpretation
Classical abstract interpretation — in the sense of Cousot & Cousot — corresponds to a pair of adjoint functors \(\alpha \dashv \gamma\) between the sheaf category \(\Sh(\mathcal{S}_P)\) (concrete semantics) and a sheaf category \(\Sh(\mathcal{A})\) on the abstract domain site. The abstraction map \(\alpha\) is left adjoint to the concretisation \(\gamma\), and the soundness condition \(\alpha \circ \mathrm{concrete} \;\sqsubseteq\; \mathrm{abstract}\) is exactly the unit of the adjunction.
Hoare Logic
A Hoare triple \(\{P\}\,C\,\{Q\}\) is a section of the proposition sheaf over the two-point site \(\mathcal{S}_{\mathrm{HT}} = \{\mathtt{pre}, \mathtt{post}\}\) with the unique covering \(\{\mathtt{pre}, \mathtt{post}\} \to \mathtt{program}\). The sheaf condition recovers the sequencing rule: gluing the pre-section and post-section along the unique intersection (the midpoint, i.e. the intermediate assertion) yields the composition rule of Hoare logic.
Separation Logic
Separation logic corresponds to judgments on the heap-partition site, whose objects are heap regions and whose covers are disjoint-union decompositions \(\{h_1, h_2\} \to h_1 * h_2\). The separating conjunction \(P * Q\) is precisely the gluing of sections \(P \in \mathcal{F}(h_1)\) and \(Q \in \mathcal{F}(h_2)\) across the disjoint cover. The sheaf condition encodes the frame rule.
Étale Cohomology
The obstruction groups \(\check{H}^p(\mathcal{S}_P, \mathcal{F})\) are the exact analogue of étale cohomology groups \(H^p_{\text{ét}}(X, \mathcal{F})\) in algebraic geometry. Étale cohomology detects torsion in Galois representations; Čech cohomology on \(\mathcal{S}_P\) detects verification torsion — the minimal perturbations needed to trivialise an obstruction class.
8.1 Galois Connections and Widening
The classical Galois connection of abstract interpretation, \(\alpha(\mathit{concrete}) \sqsubseteq \mathit{abstract} \iff \mathit{concrete} \sqsubseteq \gamma(\mathit{abstract})\), extends in JuGeo to a lax adjunction of sheaf categories that accounts for widening operators as natural transformations:
The widening operator \(\nabla\) is a natural transformation ensuring termination of fixed-point iterations; in sheaf-theoretic terms, it is a retraction that coarsens the site topology, collapsing infinitely many covering families into finitely many.
8.2 Type Theory and Dependent Types
The carrier component \(A \in \mathrm{Type}(c)\) of a judgment is drawn from a local type theory fibred over \(\mathcal{S}_P\). This fibration is the Grothendieck construction of the functor \(\mathrm{Type} : \mathcal{S}_P^{\op} \to \mathbf{Cat}\), assigning to each coordinate \(c\) its local type context. Dependent types — where the type \(A\) depends on a value \(v : B\) — correspond to sections of the total space:
The sections of this fibration are exactly the
dependently-typed propositions that JuGeo
can express and verify — a direct connection to Martin-Löf
type theory and, via the Curry-Howard correspondence,
to the Lean 4 proof language used by JuGeo's
Verified-level evidence channel.
Judgment Geometry unifies three previously separate traditions:
- Sheaf theory (Grothendieck, 1957–1972) provides the categorical machinery for local-to-global reasoning.
- Cohomological obstruction theory (Čech, 1932; Eilenberg-MacLane, 1945) provides the algebraic invariants that classify and diagnose failure.
- Proof-theoretic semantics (Prawitz, 1965; Martin-Löf, 1984) provides the logical backbone that connects sheaf sections to formal proofs.
The new contribution of Judgment Geometry is the identification of programs as sites, the judgment 4-tuple as the canonical section type, and the trust algebra as the coefficients of the sheaf — a synthesis that makes automated, graded, multi-evidence program verification both mathematically rigorous and computationally tractable.