Paper deep dive
Positive Topology and Feasible Refinement: Forcing Matrices, Positivity, and Information
Mirco A. Mannucci, Giovanni Sambin
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 9/20/2026, 3:19:27 AM
Summary
The paper develops a framework for Positive Topology based on a forcing relation between points (models) and observables (basic opens). It establishes two Galois adjunctions: one for universal refinement/cover (ext ⊣ □) and one for existential positivity/probing (◇ ⊣ rest). The positivity relation is derived as fixed points of a contractive operator. The framework supports information-theoretic and game-theoretic interpretations, where cover represents information refinement and positivity represents witnessed feasibility. The authors propose extending this to resource-sensitive contexts, considering budget constraints and verification costs, with applications in medical diagnosis, legal reasoning, and AI.
Entities (10)
Relation Signals (9)
Positive Topology → uses → Forcing Relation
confidence 97% · We develop a conceptual and operational account of Positive Topology starting from a basic relation between points or models and observable properties.
Galois Adjunction → captures → Positivity Relation
confidence 96% · The second captures positivity and witnessed existence... ◇ ⊣ rest
Forcing Relation → induces → Galois Adjunction
confidence 96% · Starting from a point–basic-open forcing relation... we obtain the canonical Galois adjunction ext ⊣ □
Galois Adjunction → captures → Cover Relation
confidence 95% · The first captures universal refinement and cover... ext ⊣ □
Positive Topology → appliedto → Medical Diagnosis
confidence 94% · Examples from medical diagnosis... illustrate the potential relevance of the approach
Positive Topology → appliedto → AI Systems
confidence 93% · Examples from... AI systems illustrate the potential relevance of the approach
Positivity Relation → interpretedas → Witnessed Feasibility
confidence 93% · The first is information-theoretic, viewing... positivity as witnessed feasibility.
Positivity Relation → interpretedas → Refinement Game
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:We develop a conceptual and operational account of Positive Topology starting from a basic relation between points or models and observable properties. From this relation, two complementary structures emerge. The first captures universal refinement and cover: what must hold across all relevant cases and how information can be systematically refined. The second captures positivity and witnessed existence: what can be positively realized and sustained without relying on classical complements. A central result shows that the underlying relation between points and observables can be reconstructed from either of these induced structures. We also clarify the distinction between point-based and pointfree formulations: when points are available, positivity can be derived from the underlying forcing relation, while in the formal pointfree setting positivity is taken as primitive and its compatibility with cover is imposed axiomatically. We develop two complementary interpretations of the framework. The first is information-theoretic, viewing cover as refinement of partial information and positivity as witnessed feasibility. The second is game-theoretic, viewing positivity as the ability of a witness or hypothesis to survive successive legitimate refinements. The final part of the paper is deliberately programmatic. We outline how resource constraints, verification costs, and finite budgets can be incorporated into the framework. This leads to resource-sensitive notions of forcing, cover, positivity, and refinement, and raises new questions about how these structures behave as available resources change. Examples from medical diagnosis, legal reasoning, and AI systems illustrate the potential relevance of the approach to grounded, explainable, and resource-aware inference.
Tags
Links
- Source: https://arxiv.org/abs/2609.13523v1
- Canonical: https://arxiv.org/abs/2609.13523v1
Trouble viewing inline? Open PDF directly →
Full Text
41,971 characters extracted from source content.
Expand or collapse full text
Positive Topology and Feasible Refinement: Forcing Matrices, Positivity, and Information Mirco A. Mannucci Email: mirco@holomathics.com Giovanni Sambin Email: sambin@math.unipd.it September 2026 Abstract Starting from a point–basic-open forcing relation x⊩ax a between a set of points/models X and basic opens/generators S, we obtain the canonical Galois adjunction ⊣□ \,ext\, between (S)P(S) and (X)P(X) encoding the “open/locale” (universal, cover/refinement) content [5]. Less standard, but equally canonical, is a second adjunction ◇⊣ \,rest\, encoding the “closed/positive” (existential, probe/meet) content; this yields a direct origin for Sambin-style positivity a⋉Ua U and “closed without complements” as fixed points of the contractive operator =◇∘ J= \,rest\, [1, 6]. We isolate a reconstruction principle: the forcing matrix is recovered uniquely from either residual pair via singleton tests. When points are given, positivity can be induced from forcing in this way; in the formal pointfree approach, positivity is instead taken as primitive and compatibility with cover is axiomatic. This distinction supports two operational readings [1, 4]: (i) an information-theoretic view, where covers express refinement of partial information and positivity expresses witnessed feasibility, and (i) a game view, where a positive witness supplies a strategy through successive cover refinements. The final part of the survey is deliberately programmatic. We sketch how resource annotations may refine ordinary forcing, how budget-indexed covers and positivity may then be studied, and how enriched variants suggest resource-aware semantics. We do not claim here a final resource logic: the interaction among budgeted forcing, cover, positivity, and logical connectives is deferred to a subsequent article [7]. Examples from medical diagnosis, legal reasoning, and AI systems illustrate the intended direction. Keywords: positive topology, formal topology, pointfree topology, locales and frames, overt locales (overtness), positivity relation a⋉Ua U, Galois connections and adjunctions, forcing semantics (forcing matrices), closed sets without complements, information refinement, game semantics, constructive mathematics, resource-/cost-aware semantics MSC 2020: 03F65 (Primary); 06D22, 06D20, 18B25, 18A40 (Secondary) ACM CCS: Theory of computation → Logic; Semantics and reasoning; Program semantics; Type theory; Software and its engineering → Software verification arXiv categories: math.LO (primary); math.CT, cs.LO (cross-list) Contents 1 Introduction: Why Positive Topology? 1.1 A motivating example: Medical diagnosis 1.2 The general pattern 2 The starting datum: a forcing/incidence relation 3 The first adjunction: opens via ext adjoint Box 3.1 Direct image and the universal residual 3.2 Cover and the pointfree (formal-cover) side 3.3 Extensional topology on points 4 The second adjunction: positivity via Diamond adjoint rest 4.1 Neighborhood sets and constraint-selected points 4.2 The existential “hit” map 5 Positivity and closed sets without complements 5.1 The positivity operator J = Diamond o rest 5.2 Elementary properties 5.3 The compatibility axiom 6 Information content and refinement games 6.1 The refinement game G(a,U) 7 Two adjunctions and four operators 8 Reconstruction of forcing from residuals 9 Feasible refinement and resources: a programmatic sketch 9.1 Truth first, cost second: a minimal baseline 9.2 Budget-indexed covers and positivity: the next problem 9.3 Enriched values: an outlook, not a final semantics 10 Conceptual summary and outlook 10.1 Outlook: toward budget-indexed truth A Application to AI engineering A.1 The AI analogue of forcing A.2 Two adjunctions = two engineering operations A.3 Positivity = safety envelopes A.4 LLM + PosTop: an illustrative architecture B Software and Reproducibility B.1 Environment setup B.2 Running the examples B.3 Notebooks and tests References 1 Introduction: Why Positive Topology? Before diving into the formal machinery, we motivate the key ideas through a concrete scenario. 1.1 A motivating example: Medical diagnosis Consider the task of diagnosing a patient based on observed symptoms. • X = patients (the “points” or “states of the world”) • S = symptoms, tests, conditions (the “observables” or “basic opens”) • x⊩ax a means “patient x exhibits symptom/condition a” A doctor observes that a patient has fever, cough, and fatigue. What can we infer? The cover relation: semantic entailment. Certain conditions imply certain symptoms. For instance: ⊲,,_, pneumonia \ fever, cough, chest\_pain, infiltrates\ This means: every patient with pneumonia exhibits at least one of fever, cough, chest pain, or lung infiltrates. More generally, a⊲Ua U says: whenever a holds, something in U holds. This is the universal/refinement side: covers encode what implies what. The positivity relation: witnessed consistency. Now consider the question: is the symptom cluster ,,\ fever, cough, fatigue\ a realizable profile? That is, does there exist a patient whose complete symptom profile is contained in this set? We write: ⋉,, fever \ fever, cough, fatigue\ to mean: there exists a patient with fever whose entire observable profile is contained in the displayed set. This patient is a witness — the symptom cluster is realizable, not a contradiction. Contrast with: ⋉ fever \ hypothermia\ This is false: no patient has both fever and only hypothermia. The combination is inconsistent. This is the existential/positivity side: positivity encodes what is consistent, what has witnesses. Why both matter. • Covers alone tell us what implies what, but not what’s realizable. • Positivity alone tells us what’s consistent, but not what follows from what. • Together they give us: grounded inference (every conclusion has a witness) with semantic structure (implications are tracked). The compatibility axiom. The key interaction between covers and positivity is: (a⊲U)∧(a⋉V)⟹∃u∈U.u⋉V(a U) (a V) ∃ u∈ U.\;u V In medical terms: if pneumonia implies fever, cough, infiltrates, and there exists a pneumonia patient confined to profile V, then there exists a fever patient (or cough patient, or infiltrates patient) also confined to V. Refinement preserves witnesses. This is the soundness condition that makes the framework coherent. 1.2 The general pattern The medical example instantiates a universal pattern: Domain Points X Observables S Medicine Patients Symptoms, tests, conditions Law Cases Evidence, claims, precedents Programming Program states Properties, assertions, tests Finance Portfolios Risk factors, exposures Science Hypotheses Experiments, observations AI agents Traces/executions Constraints, evaluations This operational reading follows the constructive-positivity tradition initiated by Sambin [1] and formalized via inductively generated formal topologies [6]. It abstracts the familiar locale/sheaf perspective of Mac Lane–Moerdijk [5] down to the level of the forcing matrix we use in code. In each domain: • a⊲Ua U encodes semantic entailment: a implies something in U • a⋉Ua U encodes witnessed consistency: there exists x with x⊩ax a and ◇x⊆U x U • The forcing x⊩ax a connects the abstract observables to concrete states The rest of this paper develops these ideas formally through the forcing/adjunction/positivity construction. The resource-aware part is intentionally an esquisse d’un programme: it records a plausible direction and isolates questions whose full treatment is left to the subsequent article [7]. 2 The starting datum: a forcing/incidence relation Definition 2.1 (Forcing table). Fix sets X (points/models) and S (basic opens/generators). A forcing relation is a subset R⊆X×SR X× S written x⊩afor (x,a)∈R.x a (x,a)∈ R. Remark 2.2 (Interpretation). Think of a∈Sa∈ S as a basic open (or observable, or test) and x∈Xx∈ X as a point (or state, or model). Then x⊩ax a reads: “x lies in the basic open a” or “x satisfies observable a”. No topology is assumed at the outset: we start from the incidence matrix. Example 2.3 (Medical diagnosis). Let X be a set of patients and S a set of symptoms/conditions. Then x⊩ax a means “patient x exhibits symptom a”. The forcing relation is the patient-symptom incidence matrix. Example 2.4 (Program verification). Let X be program states and S be assertions/properties. Then x⊩ax a means “state x satisfies property a”. Remark 2.5 (Boolean matrix viewpoint). The relation R⊆X×SR X× S is a Boolean-valued matrix R:X×S→0,1R:X× S→\0,1\. Much of what follows is “linear algebra over 0,1\0,1\”: joins are unions, meets are intersections. This matrix viewpoint also suggests the enriched, resource-sensitive direction sketched in Section 9. 3 The first adjunction: opens via ⊣□ \,ext\, 3.1 Direct image and the universal residual Definition 3.1 (Extension and interior-kernel). Define monotone maps :(S)→(X),U=x∈X:∃a∈U,x⊩a, \,ext\,:P(S) (X), \,ext\,U=\x∈ X:∃ a∈ U,\ x a\, □:(X)→(S),□E=a∈S:∀x∈X,(x⊩a⇒x∈E). :P(X) (S), E=\a∈ S:∀ x∈ X,\ (x a x∈ E)\. Example 3.2 (Medical: Extension and Interior). Continuing Example 2.3: • , \,ext\,\ fever, cough\ = patients who have fever OR cough (or both) • □E E where E = “patients over 65” gives: symptoms that only occur in patients over 65 Proposition 3.3 (Galois adjunction I). For all U⊆SU S and E⊆XE X, U⊆E⟺U⊆□E. \,ext\,U E U E. Equivalently, ⊣□ \,ext\, . Proof. (⇒ ) If a∈Ua∈ U, then a⊆U⊆E \,ext\,\a\ \,ext\,U E, hence a∈□Ea∈ E. (⇐ ) If x∈Ux∈ \,ext\,U, choose a∈Ua∈ U with x⊩ax a. Since a∈□Ea∈ E, we have x∈Ex∈ E. ∎ Remark 3.4 (Universal nature). □E E is defined by a ∀-condition; this is the “universal/refinement” side. This is exactly why the cover relation induced by forcing is a universal statement. 3.2 Cover and the pointfree (formal-cover) side Definition 3.5 (Induced preorder and cover). Define a preorder on S by a≤b:⟺∀x,(x⊩a⇒x⊩b),a≤ b : ∀ x,\ (x a x b), and define a cover relation ⊲ by a⊲U:⟺∀x,(x⊩a⇒∃b∈U,x⊩b).a U : ∀ x,\ (x a ∃ b∈ U,\ x b). Example 3.6 (Medical: Cover as symptom entailment). In the medical setting, a⊲Ua U means: every patient with condition a exhibits at least one symptom in U. For instance: flu ⊲,,, \ fever, cough, fatigue, myalgia\ _ bacterial\_infection ⊲,_ \ fever, elevated\_WBC\ These are diagnostic implications: the disease implies certain observable symptoms. Remark 3.7 (Extensional reading). Equivalently: a≤b⇔a⊆b,a⊲U⇔a⊆U.a≤ b \,ext\,\a\ \,ext\,\b\, a U \,ext\,\a\ \,ext\,U. So ⊲ is literally “inclusion in a union”. 3.3 Extensional topology on points Definition 3.8 (Generated opens on X). A subset E⊆XE X is extensional open (generated by S) if E=□E.E= \,ext\, E. Remark 3.9. The operator :=∘□ \,int\,:= \,ext\, is an interior operator on (X)P(X): it extracts the largest extensional open contained in a given subset. (Dually, :=□∘ A:= \,ext\, is the saturation operator, a closure/nucleus-like operator on (S)P(S).) Extensional opens are exactly the fixed points of \,int\,: “those subsets describable by generators”. Definition 3.10 (Extensional equivalence of points). Define x∼yx y if the induced neighborhood sets agree: x∼y:⟺∀a∈S,(x⊩a⇔y⊩a).x y : ∀ a∈ S,\ (x a y a). Example 3.11 (Medical: Indistinguishable patients). Two patients x∼yx y are symptomatically indistinguishable: they exhibit exactly the same symptoms. From a diagnostic standpoint, they are equivalent — the same inferences apply to both. Remark 3.12. Pointfree semantics does not distinguish points inside the same ∼ -class. This is the basic “quotient-to-locale” phenomenon: locale data sees neighborhood behavior, not point multiplicity. 4 The second adjunction: positivity via ◇⊣ \,rest\, The locale/cover side is universal; “closed without complements” needs an existential probe: “does a basic open hit a closed thing?”. This is the conceptual origin of Sambin-style positivity [1, 3, 4]. 4.1 Neighborhood sets and constraint-selected points Definition 4.1 (Neighborhood set). For x∈Xx∈ X, its neighborhood set (or observable profile) is ◇x:=a∈S:x⊩a⊆S. x:=\a∈ S:\ x a\ S. Example 4.2 (Medical: Symptom profile). For a patient x, the neighborhood set ◇x x is their complete symptom profile: the set of all symptoms/conditions they exhibit. Definition 4.3 (Selection by a constraint on neighborhoods). Define :(S)→(X),U:=x∈X:◇x⊆U. \,rest\,:P(S) (X), \,rest\,U:=\x∈ X:\ x U\. Thus U \,rest\,U consists of points all of whose basic neighborhoods lie in U. Example 4.4 (Medical: Patients confined to a symptom cluster). ,, \,rest\,\ fever, cough, fatigue\ = patients whose entire symptom profile is contained in ,,\ fever, cough, fatigue\. These are patients who have only fever, cough, and/or fatigue — no other symptoms. 4.2 The existential “hit” map Definition 4.5 (◇ -Hit). Define ◇:(X)→(S),◇D:=a∈S:∃x∈D,x⊩a,that is,a◇D↔a≬D. :P(X) (S), D:=\a∈ S:∃ x∈ D,\ x a\, is, a D\; \; \,ext\,a D. In words, a hits the set D if a has a witness inside D. Example 4.6 (Medical: Symptoms witnessed in a cohort). If D = patients in a clinical trial, then ◇D D = symptoms exhibited by at least one patient in the trial. Proposition 4.7 (Galois adjunction I). For all D⊆XD X and U⊆SU S, ◇D⊆U⟺D⊆U. D U D \,rest\,U. Equivalently, ◇⊣ \,rest\,. Proof. (⇒ ) Let x∈Dx∈ D. If a∈◇xa∈ x then a∈◇D⊆Ua∈ D U. Hence ◇x⊆U x U and x∈Ux∈ \,rest\,U. (⇐ ) If a∈◇Da∈ D, choose x∈Dx∈ D with x⊩ax a. Since x∈Ux∈ \,rest\,U we have a∈◇x⊆Ua∈ x U. ∎ Remark 4.8 (Meaning). ◇D D records which generators are witnessed in D. U \,rest\,U picks points whose entire neighborhood behavior is constrained by U. This is the “closed-without-complements” move: U acts as a code for a closed-like object by constraining neighborhoods, not by negation. 5 Positivity and closed sets without complements 5.1 The positivity operator =◇∘ J= \,rest\, Definition 5.1 (Positivity interior on codes). Define :(S)→(S),U:=◇U. J:P(S) (S), JU:= \,rest\,U. Equivalently, aU↔∃x∈X(x⊩a∧◇x⊆U)↔a≬U.a JU ∃ x∈ X\ (x a\ \ x U ) \,ext\,a \,rest\,U. Definition 5.2 (Positivity relation). Define ⋉⊆S×(S) S×P(S) by a⋉U:⟺a∈U.a U : a∈ JU. Remark 5.3 (One-line intuition). a⋉Ua U means: there exists a point x in basic open a such that all basic neighborhoods of x lie in U. So U behaves like a “closed neighborhood specification” and a hits it. Example 5.4 (Medical: Positivity as witnessed symptom clusters). The statement ⋉,, fever \ fever, cough, fatigue\ means that there exists a patient who has fever and whose complete symptom profile is contained in that set. This patient is a witness that fever is consistent with the symptom cluster. Contrast: ⋉ fever \ hypothermia\ is false because no patient has both fever and only hypothermia — the combination is contradictory. Positivity detects realizability: which symptom combinations actually occur in patients. Proposition 5.5 (A point forces positivity). Assume a point x∈Xx∈ X and a generator a∈Sa∈ S with x⊩ax a. Then a is positive in the unary sense, i.e. a⋉Sa S. More generally, if U⊆SU S satisfies ◇x⊆U x U, then a⋉Ua U. Proof. If ◇x⊆U x U then x∈Ux∈ \,rest\,U by definition, hence a∈◇U=Ua∈ \,rest\,U= JU, i.e. a⋉Ua U. Taking U=SU=S gives a⋉Sa S. ∎ 5.2 Elementary properties Proposition 5.6 (Contractive and monotone). For all U,V⊆SU,V S: (a) U⊆U JU U. (b) If U⊆VU V then U⊆V JU JV. Proof. (a) If a∈Ua∈ JU, choose x with x⊩ax a and ◇x⊆U x U. Then a∈◇x⊆Ua∈ x U. (b) If U⊆VU V then U⊆V \,rest\,U \,rest\,V, hence ◇U⊆◇V \,rest\,U \,rest\,V. ∎ Proposition 5.7 (Idempotence). =◇∘ J= \,rest\, is idempotent: U=U J JU= JU. Proof. Since ≤id J , we have U⊆U J JU JU. For the reverse, id≤∘◇id≤ \,rest\, implies U⊆U \,rest\,U \,rest\, JU; applying ◇ yields U⊆U JU J JU. ∎ Definition 5.8 (Formal closed (via positivity)). Call U⊆SU S formal closed if U=U JU=U. Example 5.9 (Medical: Complete symptom profiles). Because U⊆U JU U holds for every U, the fixed-point condition U=U JU=U amounts to the converse inclusion U⊆U JU. Thus a set U⊆SU S is formal closed iff, for every symptom a∈Ua∈ U, there exists a patient x such that x⊩aand◇x⊆U.x a x U. In other words, every observable admitted by the closed code U is actually realized by a witness whose complete observable profile stays inside U. This positive formulation is the useful constructive content of closedness here. 5.3 The compatibility axiom The key interaction between covers and positivity is captured by: Proposition 5.10 (Compatibility). If , A, J are defined as above from ⊩ , then for all U,V⊆SU,V S: U≬V→U≬V. AU JV\;→\;U JV. Proof. Suppose U≬V AU JV, that is, there exists a with aUa AU and a⋉Va V. By positivity (a⋉Va V), there exists x with x⊩ax a and ◇x⊆V x V. By aUa AU, i.e. a⊆U \,ext\,a \,ext\,U, since x⊩ax a there exists u∈Uu∈ U with x⊩ux u. Then u∈◇x⊆Vu∈ x V, so u⋉Vu V; hence U≬VU JV. ∎ Compatibility is provable when cover and positivity are defined via points. In a formal approach, it is assumed as an axiom. Remark 5.11 (Why compatibility matters). Compatibility is the soundness condition for refinement: if you refine a hypothesis (via covers), you don’t lose your witnesses (positivity). This is what makes the formal framework coherent for inference. Example 5.12 (Medical: Refinement preserves witnesses). Suppose ⊲,,, pneumonia \ fever, cough, infiltrates\, and there exists a pneumonia patient confined to profile V. Then there exists a fever patient (or cough patient, or infiltrates patient) also confined to V. The diagnostic refinement from “pneumonia” to its symptoms preserves the witness. 6 Information content and refinement games The formal relations ⊲ and ⋉ admit an interpretation closer to computation than to classical topology. Think of a generator a∈Sa∈ S as a partial information state. A cover a⊲Ua U says that to settle the information in a one must proceed to a feasible refinement and end up in one of the subcases in U. Positivity adds one crucial twist: existence is not classical negation of emptiness, but a witnessed possibility of continuing the refinement process. 6.1 The refinement game G(a,U)G(a,U) Fix a∈Sa∈ S and a set U⊆SU S of “acceptable outcomes”. Define an infinite two-player game G(a,U)G(a,U): • The current position is a generator b∈Sb∈ S (initially b=ab=a). • Refiner (“Devil”) chooses a cover b⊲Vb V. • Witness (“God”) responds by choosing some v∈Vv∈ V. • The next position is b:=vb:=v. • Witness wins if she can play forever while keeping every chosen position inside U. Proposition 6.1 (Positivity as a winning condition). If a⋉Ua U, then Witness has a winning strategy in G(a,U)G(a,U). Proof. By a∈Ua∈ JU there exists x∈Xx∈ X with x⊩ax a and ◇x⊆U x U. Whenever Refiner plays b⊲Vb V with x⊩bx b, there exists v∈Vv∈ V with x⊩vx v. Witness chooses such v. Since v∈◇x⊆Uv∈ x U, the position stays in U. ∎ Medical diagnosis as a refinement game. The game G(,U)G( fever,U) where U is a diagnostic profile: • Refiner (skeptic): “You say fever? What kind? Bacterial? Viral?” • Witness (diagnostician): “Bacterial fever” (chooses refinement in U) • Refiner: “What symptoms? Give me a cover.” • Witness: “Elevated WBC” (still in U) A real patient x witnessing positivity supplies Witness with a strategy that survives every refinement challenge. Legal reasoning as a refinement game. Let X = legal cases, S = claims/evidence/precedents. The game: opposing counsel (Refiner) demands finer distinctions; the advocate (Witness) must find precedents. Positivity = having a real case to cite at every challenge. 7 Two adjunctions and four operators The same forcing table gives two adjunctions, hence four operators: (S)⇄□(X)(⊣□),(X)⇄◇(S)(◇⊣).P(S)\ \,ext\, \ P(X) ( \,ext\, ), (X)\ \,rest\, \ P(S) ( \,rest\,). Operator Type Meaning \,ext\, (S)→(X)P(S) (X) Points satisfying some observable in U □ (X)→(S)P(X) (S) Observables universally valid on E ◇ (X)→(S)P(X) (S) Observables witnessed in D \,rest\, (S)→(X)P(S) (X) Points confined to profile U =□∘ A= \,ext\, (S)→(S)P(S) (S) Saturation (formal opens) =∘□ \,int\,= \,ext\, (X)→(X)P(X) (X) Interior (extensional opens) =◇∘ J= \,rest\, (S)→(S)P(S) (S) Reduction (formal closed codes) =∘◇ \,cl\,= \,rest\, (X)→(X)P(X) (X) Closure (on points) Remark 7.1 (Two sides of the same coin). Both adjunctions arise from the same forcing relation, but govern different semantics: • ⊣□ \,ext\, = universal refinement / locale / covers • ◇⊣ \,rest\, = existential probes / positivity / closed-without-complements 8 Reconstruction of forcing from residuals A central observation (cf. Ciraulo–Sambin [2]) is that the forcing table is recoverable from either left adjoint, since left adjoints preserve joins and are determined by their action on singletons. Theorem 8.1 (Singleton reconstruction). If F=F= \,ext\, arises from ⊩ , then ⊩ is uniquely determined by: x⊩a⟺x∈a.x a x∈ \,ext\,\a\. Similarly for ◇ : x⊩a⟺a∈◇x.x a a∈ \x\. Proof. Since \,ext\, preserves unions, U=⋃a∈Ua \,ext\,U= _a∈ U \,ext\,\a\. Thus x∈Ux∈ \,ext\,U iff ∃a∈U∃ a∈ U with x∈ax∈ \,ext\,\a\. ∎ Remark 8.2 (What is not reconstructible). The composites j=□∘j= \,ext\, or =◇∘ J= \,rest\, generally lose witness-level information. The residual pair determines forcing; a single composite does not. 9 Feasible refinement and resources: a programmatic sketch The preceding sections are the mathematically established core of this survey. We now turn to resources. This section is intentionally exploratory: its purpose is to identify a clean baseline and the questions that must be settled in a fuller theory of resource-bounded Positive Topology [7]. 9.1 Truth first, cost second: a minimal baseline A resource annotation should refine ordinary forcing rather than replace truth by affordability. We therefore retain the Boolean forcing relation x⊩ax a and annotate verified incidences with a cost. Definition 9.1 (Budget preorder). A budget preorder is a preorder (B,⪯)(B, ). We read b⪯b′b b as saying that anything feasible within budget b is also feasible within the more permissive budget b′b . Definition 9.2 (Cost annotation and budgeted forcing). Let c:(x,a)∈X×S:x⊩a⟶Bc:\(x,a)∈ X× S:x a\ B assign a verification cost to each true incidence. For b∈Bb∈ B define x⊩ba:⟺x⊩a and c(x,a)⪯b.x _ba :\!\! x a\ and \ c(x,a) b. Thus x⊩bax _ba means not merely that testing a costs at most b, but that a is true at x and that this truth can be verified within budget b. Example 9.3 (Medical: Verification costs). For illustration, suppose verified observations carry the following costs: Test/Observation Cost Notes Fever $0 Thermometer Cough $0 Observation Blood pressure $5 Standard equipment Blood test (WBC) $50 Lab work PCR test $100 Molecular X-ray $200 Imaging CT scan $500 Advanced imaging If patient x really has elevated WBC and that fact costs $50 to verify, then x⊩b_x _b elevated\_WBC for every budget b at least $50. A negative test result is not represented by a cheap positive incidence; it belongs to the underlying observational vocabulary only if we explicitly include a corresponding generator. Remark 9.4 (Filtration of forcing). For b⪯b′b b we have x⊩ba⟹x⊩b′a.x _ba x _b a. Hence the forcing relations form a monotone filtration in the budget. No corresponding monotonicity of induced covers or positivity relations is asserted here. 9.2 Budget-indexed covers and positivity: the next problem At each fixed budget b one may repeat the constructions of the Boolean case: a⊲bU:⟺∀x(x⊩ba⇒∃u∈Ux⊩bu),a _bU : ∀ x\, (x _ba ∃ u∈ U\;x _bu ), a⋉bU:⟺∃x(x⊩ba∧◇bx⊆U),◇bx:=a∈S:x⊩ba.a _bU : ∃ x\, (x _ba\ \ _bx U ), _bx:=\a∈ S:x _ba\. For every fixed b, these are simply the cover and positivity relations induced by the budget-restricted forcing table. The subtle question is how they vary with b. Although ⊩b _b is monotone in the budget, neither ⊲b _b nor ⋉b _b inherits a naive monotonicity law automatically. Increasing a budget may introduce new points satisfying the antecedent of a cover, new possible witnesses, and a larger observable profile ◇bx _bx; these effects need not point in the same direction. Characterizing conditions under which families ⊲bb∈B\ _b\_b∈ B and ⋉bb∈B\ _b\_b∈ B have useful coherence properties is one of the main tasks deferred to the next article [7]. 9.3 Enriched values: an outlook, not a final semantics A more ambitious route is to replace the Boolean matrix by a value object V carrying both logical and resource information. Schematically one seeks R:X×S⟶VR:X× S V together with suitable projections or threshold maps recovering ordinary and budget-indexed forcing. In particular, the Boolean content should remain recoverable from the enrichment rather than being identified with a numerical cost. If V is equipped with a sufficiently complete residuated monoidal order (V,≤,⊗,I,⊸)(V,≤, ,I, ), the familiar enriched formulas suggest the operators (Vϕ)(x)=⋁a∈Sϕ(a)⊗R(x,a),(□Vψ)(a)=⋀x∈X(R(x,a)⊸ψ(x)),( \,ext\,_Vφ)(x)= _a∈ Sφ(a) R(x,a), ( _Vψ)(a)= _x∈ X (R(x,a) ψ(x) ), (◇Vψ)(a)=⋁x∈Xψ(x)⊗R(x,a),(Vϕ)(x)=⋀a∈S(R(x,a)⊸ϕ(a)).( _Vψ)(a)= _x∈ Xψ(x) R(x,a), ( \,rest\,_Vφ)(x)= _a∈ S (R(x,a) φ(a) ). Under the usual completeness/residuation hypotheses these have the expected adjoint shape V⊣□V \,ext\,_V _V and ◇V⊣V _V \,rest\,_V, and suggest an enriched positivity operator V:=◇V∘V J_V:= _V \,rest\,_V. We record these formulas only as a bridge to the programme. The precise choice of V, the recovery of the underlying truth relation, the role of thresholds, and the interaction with logical structural rules are not fixed in this survey and will be treated separately [7]. 10 Conceptual summary and outlook Three layers, with different status in this survey. (i) forcing and the two adjunctions⇓(i) cover, positivity, and closedness without complements⇓(i) resource-aware refinement and logic array[]c(i) forcing and the two adjunctions\\[2.0pt] \\[2.0pt] (i) cover, positivity, and closedness without complements\\[2.0pt] \\[2.0pt] (i) resource-aware refinement and logic array Layers (i)–(i) are developed here. Layer (i) is the announced research programme. 10.1 Outlook: toward budget-indexed truth A future resource logic should introduce a new satisfaction judgement, say s⊩bφ,s _b , where s is an explicitly specified semantic state, φ belongs to a defined syntax, and b is a budget. This judgement is not the same object as the incidence relation x⊩bax _ba of Section 9; it would be a recursively defined logical semantics built on top of the resource-refined forcing structure. For example, if resources must be split between conjunctive subgoals, one might require a relation (b,b1,b2) Split(b;b_1,b_2) and adopt a clause of the schematic form s⊩b(φ∧ψ)⟺∃b1,b2((b;b1,b2)&s⊩b1φ&s⊩b2ψ).s _b( ψ) ∃ b_1,b_2\, ( Split(b;b_1,b_2)\ \&\ s _b_1 \ \&\ s _b_2ψ ). Likewise, existential truth should remain witnessed and budget-sensitive. But the syntax, semantic states, budget algebra, structural rules, and exact relation between logical satisfaction and positivity are deliberately left open here. They form part of the next article [7]. Appendix A Application to AI engineering This appendix explains why forcing/positivity/cost provides concrete engineering value for AI systems. A.1 The AI analogue of forcing In AI engineering, one evaluates systems against requirements: • X = executions / traces / agent rollouts • S = constraints (“tool-call succeeded”, “no disallowed content”, “latency <500<500ms”, etc.) • x⊩ax a = “execution x satisfies constraint a” The Boolean forcing table R⊆X×SR X× S is therefore an evaluation matrix. The resource-sensitive constructions of Section 9 should be read as possible refinements of this basic evaluation layer. A.2 Two adjunctions = two engineering operations (1) ⊣□ \,ext\, : specification refinement. • U \,ext\,U: which traces satisfy at least one check in U? • □E E: which checks are universally valid over traces E? • a⊲Ua U: whenever a holds, some b∈Ub∈ U holds This is specification management: what the system guarantees. (2) ◇⊣ \,rest\,: witness finding. • ◇D D: which checks are witnessed in trace-set D? • U \,rest\,U: which traces live entirely inside constraint envelope U? • a⋉Ua U: exists a trace satisfying a with profile ⊆U U This is counterexample search and safe operating region identification. A.3 Positivity = safety envelopes Engineers want “safe = complement of bad”. This fails because: (a) the complement is not observable (unknown unknowns) (b) violations are sparse and adversarial (c) safety is better defined by positive evidence of robustness Positivity gives a constructive alternative: • closed code U with U=U JU=U is a safety envelope • a⋉Ua U provides witness-based membership Safety is a robust region, not a complement. A.4 LLM + PosTop: an illustrative architecture Current LLM agents can fail by producing claims without witnesses, by combining inconsistent claims, or by spending verification resources poorly. The forcing/cover/positivity picture suggests an engineering discipline in which candidate outputs are checked against explicit observations, witnesses, and budgets. At this point, however, a typing distinction is essential. The present survey has defined cover and positivity for generators a∈Sa∈ S and subsets U⊆SU S; it has not identified arbitrary LLM hypotheses with generators. A concrete system must therefore provide an encoding of hypotheses into the formal structure – for example a map ι:H→S :H→ S or a richer syntax built over S – together with a representation of the current observation state. Only after that choice is made do expressions involving cover or positivity become well typed. One possible implementation pattern is then: 1. the LLM proposes candidate hypotheses H; 2. an explicit encoding maps each candidate into the PosTop structure; 3. cover checks test the chosen direction of semantic consequence, while positivity checks demand a witness; 4. a resource layer proposes an observation or test that best discriminates among the remaining candidates; 5. the process repeats until the task is resolved or the budget is exhausted. This is an architectural schema, not a theorem of the present paper. In particular, the direction of the cover check depends on how an observation state and a hypothesis are represented; the informal expression “h⊲observedh ” used in earlier drafts should not be read as defined notation. A fully typed account of hypotheses, observations, resource choice, and agent traces belongs to the subsequent development [7]. Comparison with knowledge graphs. The comparison with knowledge graphs is best understood as a difference of emphasis, not as an impossibility claim. A bare knowledge graph primarily records entities and relations; entailment procedures, provenance, costs, and verification policies may certainly be layered on top. Positive Topology contributes a native language for cover, positivity, witness preservation, and – in the proposed extension – feasible refinement. A knowledge graph is naturally a representation of structured facts. The PosTop programme aims to add a grammar of refinement: what follows, what remains witnessable, and eventually what can be verified within available resources. Appendix B Software and Reproducibility The LaTeX file you are reading lives in the same repository as the reference implementation of the forcing matrix, adjunctions, and notebooks. The codebase is organized as follows: • src/postop/core.py implements the data structures discussed in Sections 4–6, with the forcing relation encoded as a Python dictionary of point → observable sets, plus the cost-aware variants in src/postop/costs.py. • src/postop/operators.py and src/postop/llm.py provide tracing/explainability helpers that surface the cover witnesses/counterexamples required by the diagnostic examples. • examples/ mirrors the running medical and guardrail scenarios; tests/ exercises the adjunction identities via pytest. • docs/REPRODUCIBILITY.md gives a copy/paste runbook matching the commands below. The latest sources live at https://github.com/mirco-mannucci/postop; we snapshot paper+code together via the git tag v0.1.0 (and subsequent releases) so the commands below always map to a reproducible commit/DOI pair. B.1 Environment setup We keep the environment lightweight (pure Python + pytest). From the repository root:python3 -m venv .venv source .venv/bin/activate pip install -e .[dev] B.2 Running the examples The forcing table is serialized as ordinary Python dictionaries and can be inspected directly. To reproduce the medical walkthrough and the illustrative guardrail example discussed in this survey:python examples/medical.py python examples/llm_guardrail.py Each script prints the /□/◇/ \,ext\,/ / / \,rest\, results, the compatibility witnesses, and the guardrail counterexamples that correspond to the formal statements in the main text. B.3 Notebooks and tests The ActionList roadmap adds four short notebooks under notebooks/; they can be executed headlessly via:jupyter nbconvert --to notebook --execute \ notebooks/01_basics_ext_int_hit_sel_j.ipynb Swap in the remaining notebook filenames (medical diagnosis, costs, guardrails) to reproduce the figures in the extended version of the paper. Finally, run the test suite to check the adjunction/proof obligations:pytest -q These tests import the installed package so they are venv-friendly and catch regressions both in the mathematical invariants (idempotence/contractivity) and in the explainability helpers referenced by the notebooks. References [1] G. Sambin. Positive Topology: A New Practice in Constructive Mathematics. Oxford University Press, 2025. https://doi.org/10.1093/9780191746796.001.0001. [2] F. Ciraulo and G. Sambin. A constructive Galois connection between closure and interior. The Journal of Symbolic Logic, 77(4):1308–1324, 2012. https://doi.org/10.2178/jsl.7704150; arXiv:1101.5896. [3] S. Valentini. Relative formal topology: the binary positivity predicate comes first. Mathematical Structures in Computer Science, 22(1):69–102, 2012. https://doi.org/10.1017/S0960129511000466. [4] F. Ciraulo and S. Vickers. Positivity relations on a locale. Annals of Pure and Applied Logic, 167(9):806–819, 2016. https://doi.org/10.1016/j.apal.2016.04.009. [5] S. Mac Lane and I. Moerdijk. Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Springer-Verlag, New York, 1992. https://doi.org/10.1007/978-1-4612-0927-0. [6] T. Coquand, G. Sambin, J. Smith, and S. Valentini. Inductively generated formal topologies. Annals of Pure and Applied Logic, 124(1–3):71–106, 2003. https://doi.org/10.1016/S0168-0072(03)00052-6. [7] A. Meneghello, M. A. Mannucci, and G. Sambin. Resource-Bounded Positive Topology: Threshold Forcing, Feasible Refinement, and the TROPOS Programme. In preparation, 2026.