Model-Theoretic Foundations

The metaphor

JacqOS is a physics engine for business logic. The engine is deterministic, observable, and replayable. This page is the precise version of what makes that physics engine actually compose: it explains why the simulation has a unique stable state, why debugging a bad fact is a neighborhood problem, and why independently authored agent domains are genuinely decoupled rather than coincidentally non-overlapping.

Every “the engine just figures it out” claim elsewhere in the docs is backed by one of the properties on this page.

What it means for your app

Three practical consequences carry down into the surfaces you use every day:

• jacqos verify is not a stylistic check. It reports rule shapes, monotonicity, and composition status because each one is a load-time guarantee — not a code-review opinion. An “unconstrained” warning is the platform telling you which rule will be expensive to debug because its witness is wider than the tuple.
• Studio’s drill inspector works the way it does on purpose. The Gaifman-neighborhood layer centers the graph on the tuple you selected, then expands outward, because the math says the witness for a bad fact almost always lives within a small radius. You are not seeing a designer’s UX preference; you are seeing the model theory determining what the UI surfaces by default.
• Multi-agent decoupling is analyzable, not aspirational. When two agents live in disjoint namespace reducts, the platform can mark them semantically separate within the fixed evaluator. Adding a third agent that shares no relations with either does not rely on a naming convention — it is checked by composition analysis.

If those three intuitions are what you came for, you can stop here and skim the headers below to see the underlying machinery.

The precise version

The containment architecture makes two promises: runtime agents are safe, and AI-generated rules are verifiable. Model theory is what makes both promises provable rather than aspirational.

When runtime agents coordinate through a shared derived model, you need guarantees that the model stays tractable as the ontology grows, that debugging a bad fact doesn’t require inspecting the entire world, and that independently authored agent domains are genuinely decoupled. When development-time AI generates rules, you need guarantees that the rules compose predictably and that the platform can check them efficiently.

JacqOS does not leave those questions to taste. The platform evaluates one ordered finite model, then exposes the structural properties that matter:

• Rule shapes tell you whether a rule is pivoted around one guard, tree-shaped, or fully unconstrained — and whether the platform can optimize its evaluation.
• Gaifman locality tells you why debugging a bad agent intent is a neighborhood problem, not a world-size problem.
• Namespace reducts tell you when agent domains are truly separate and when they only look separate on disk.

This is Model-Theoretic Simplicity in practice. The same mathematics that makes the containment boundary deterministic also gives you inspection surfaces for free.

Rule shapes

Every .dh rule has a positive join core. JacqOS classifies that join core into one of five shapes and surfaces the result in verification output, Studio, and exported artifacts.

The five shapes

Shape	What it means in practice	What to prefer
star query	Every positive clause shares one pivot variable	Best default for mapper-driven rules
guarded	One clause contains every variable used by the join	Still tightly grounded
frontier-guarded	One clause contains every shared join variable	Good when one relation anchors coordination
acyclic conjunctive	The join graph is tree-shaped	Usually fine, but less compact than a star
unconstrained	None of the above	Correct, but harder to optimize and explain

Star query

Star queries are the natural shape for observation-first rules. One variable, usually an observation ID or entity ID, anchors the whole rule.

rule booking_ready(req, email, slot) :-
  atom(req, "booking.email", email),
  atom(req, "booking.slot_id", slot),
  atom(req, "booking.intent", "request").

req is the pivot, so the evaluator never needs to guess which observation the other atoms belong to. Provenance stays compact because one concrete binding anchors the witness.

Guarded

A guarded rule does not need one shared pivot variable, but it does have one clause that contains every variable used anywhere in the join.

rule incident_assignment(incident, service, region, owner, escalation) :-
  triage_snapshot(incident, service, region, owner, escalation),
  service_primary(service, owner),
  incident_region(incident, region),
  region_escalation(region, escalation).

triage_snapshot(...) contains every variable in the rule body. That keeps the join grounded around one clause instance even though there is no single variable shared by every clause.

Frontier-guarded

Frontier-guarded rules relax that requirement slightly. One clause still contains all the shared join variables, even if it does not contain every local variable in the rule.

rule incident_coordination(incident, service, dependency, owner, runbook, priority) :-
  incident_scope(incident, service, dependency),
  service_owner(service, owner),
  dependency_runbook(dependency, runbook),
  incident_priority(incident, priority).

incident_scope(...) contains the shared coordination surface: incident, service, and dependency. That is enough to keep the rule tractable and the witness local.

Acyclic conjunctive

An acyclic conjunctive rule is not guard-centered, but its join graph is still a tree rather than a cycle.

rule incident_responder(service, owner) :-
  service_alert(service, alert),
  alert_dependency(alert, dependency),
  dependency_runbook(dependency, runbook),
  runbook_owner(runbook, owner).

This is a path, not a triangle. The evaluator can still walk it without cyclic backtracking.

Unconstrained

Unconstrained rules still evaluate correctly. They just do not come with an extra local tractability guarantee from the catalog.

rule unstable_triangle(service, alert, dependency) :-
  service_alert(service, alert),
  alert_dependency(alert, dependency),
  dependency_service(dependency, service).

This is the shape to watch. Cyclic joins are usually the first place where provenance gets wider and debugging gets more expensive.

What jacqos verify reports

jacqos verify always tells you whether your ontology stayed inside the friendly part of the catalog.

$ jacqos verify
Verified 3 fixture(s): 42 observations, 198 atoms. Shadow: 3/3. Bundle: generated/verification/my-app.json
Determinism:
  status: 3/3 fixture(s) passed fresh replay and repeated mapper/helper checks
  warnings: none
Candidate-authority lints:
  warnings: none
Rule Shape Report
  Star queries: 18  Guarded: 9  Unconstrained: 1
  ⚠ ontology/rules.dh:42:1 unstable_triangle(...) unconstrained - consider a guard variable

Two details matter:

• The CLI headline groups guarded, frontier-guarded, and acyclic conjunctive into one Guarded bucket so you can scan risk fast.
• Exported artifacts keep the exact five-way classification when you need the full breakdown. The per-relation rule-shape view inside Studio ships with the V1.1 rule-graph surface.

An unconstrained warning is not a correctness failure. It means “this rule is still legal, but the platform cannot attach an extra tractability guarantee to its join shape.” If that rule sits on a hot path or keeps showing up in debugging, refactor it toward a guard-centered shape.

On multi-agent apps, the same verify run also emits a composition report under generated/verification/composition-analysis-<evaluator_digest>.json. That report pins the namespace reduct partitions, cross-namespace dependencies, monotonic versus non-monotonic strata summary, and namespace-cycle severity for the current ontology. The visual rendering of namespace partitions and cross-namespace edges in Studio ships with the V1.1 rule-graph surface; in V1 the artifact is the canonical inspection surface, and the CLI report and the file you check into generated/verification/ are the same contract.

Monotonicity classification

Rule shape tells you how a join is anchored. Monotonicity tells you whether a part of the ontology only adds derived truth or whether it can also withdraw or arbitrate it.

JacqOS classifies both rules and strata as either monotonic or non_monotonic:

• Monotonic rules only add consequences when new evidence arrives.
• Non-monotonic rules rely on negation, aggregates, mutations, or other constructs that require arbitration rather than simple set growth.

That distinction matters because it tells you where future distribution, incremental recomputation, and namespace cycles stay cheap versus where the system must stay centralized and careful.

jacqos verify surfaces the classification directly:

Monotonicity Report
  Rules: 18 monotonic, 7 non-monotonic
  Strata: 3 monotonic, 1 non-monotonic
  Non-monotonic reasons: 3 negation, 2 aggregate, 2 mutation

In practice, read it like this:

• Many monotonic lower strata mean your ontology has large areas that only grow with new evidence.
• Non-monotonic strata are not bad. They are the places where the ontology decides, retracts, or enforces exclusivity.
• The reason counts tell you why a stratum is non-monotonic, so you can tell the difference between an intentional invariant boundary and an accidental modeling choice.

Composition analysis uses the same classification. A new monotonic cross-namespace cycle is a warning because it needs review. A new non-monotonic cycle is a failure because it couples agent domains through an arbitrating loop.

Gaifman locality

When one fact is wrong, the answer is not hidden somewhere in the whole worldview. It is in the fact’s neighborhood.

That is the intuition behind Gaifman locality. Facts that share entities sit near each other in the Gaifman graph, so most explanations stay inside a small radius around the tuple you care about.

In the incident-response example, the blast radius is derived like this:

rule triage.root_cause(root) :-
  infra.degraded(root),
  not infra.healthy(root).

rule triage.blast_radius(service, root) :-
  infra.transitively_depends(service, root),
  triage.root_cause(root).

If triage.blast_radius("frontend-web", "db-primary") looks wrong, you do not need to inspect every service, every alert, and every remediation proposal in the lineage. You start with that tuple and inspect the nearby facts that share frontend-web or db-primary.

In V1, the closest thing Studio offers is the drill inspector’s Atoms / Observations and Facts sections, which list local witnesses around a selected Activity row in text form. The visual Gaifman Neighborhood view — a graph centered on the selected tuple, with an adjustable radius — ships in V1.1 alongside the visual rule graph. Until then, the same neighborhood data lives in the verification bundle.

The intended debugging loop matches how people think:

1. Start from the bad tuple.
2. Look at the nearby evidence.
3. Widen only if the witness crosses the current boundary.

This is why Visual Provenance scales. The UI is not hiding the rest of the world from you. The model says you usually do not need it.

Namespace reducts

A namespace reduct is the part of the worldview that uses only one slice of the vocabulary. In JacqOS, that means namespaces like booking.*, billing.*, triage.*, or remediation.*.

If two namespaces have no dependency edges between them, the platform can mark them disjoint within the fixed evaluator. That is stronger than “these rules happen to live in different files.” It means their facts, rules, and invariants do not semantically couple, assuming deterministic mappers, an ordered observation lineage, compatible lower strata, and no hidden side effects outside declared capabilities.

Here is a tiny example:

rule booking.request(req) :-
  atom(obs, "booking.request_id", req).

rule billing.invoice(inv) :-
  atom(obs, "billing.invoice_id", inv).

Those namespaces do not touch, so jacqos stats surfaces two independent reduct partitions:

{
  "vocabulary_partitions": {
    "partition_count": 2
  },
  "namespace_reduct_partitions": [
    {
      "namespace_label": "billing.*",
      "namespaces": ["billing"],
      "relations": ["billing.invoice"]
    },
    {
      "namespace_label": "booking.*",
      "namespaces": ["booking"],
      "relations": ["booking.request"]
    }
  ],
  "reduct_partitions": {
    "disjoint_pairs": [["billing", "booking"]],
    "cross_namespace_edges": []
  }
}

That output means:

• these modules are separate in the ontology, not just in the folder tree
• the platform can inspect them independently
• future runtime work can use the same disjointness evidence to evaluate or scale them independently

If cross_namespace_edges is non-empty, that is useful too. It tells you exactly where the coupling lives and which relations form the shared coordination surface.

Composition analysis

Namespace reducts tell you what is connected. Composition analysis tells you whether those connections are still safe to evolve.

The portable composition report runs three static checks over the ontology plus fixture expectations:

• unconstrained cross-namespace rule failures
• cross-namespace dependency and cycle analysis
• invariant fixture coverage

You can materialize that report without replaying live store state:

$ jacqos export composition-analysis
generated/verification/composition-analysis-sha256-7c419e9ed11d37434c5936a9aafeb9f68dd9a24b2ff159e6a93e2ecc3779343d.json

$ jacqos composition check
Composition analysis passed: 0 failure(s), 0 warning(s). Digest: sha256:7c419e9ed11d37434c5936a9aafeb9f68dd9a24b2ff159e6a93e2ecc3779343d.

That report answers the questions you actually need when a multi-agent ontology grows:

• Which namespaces share one reduct partition?
• Which cross-namespace edges are positive coordination, negation, or aggregate pressure?
• Which namespace cycles are monotonic warnings versus non-monotonic failures?
• Which invariants still have explicit fixture coverage?

This is why Module Boundary Engine features matter to the docs site at all. They turn “we think the agents are decoupled” into a stable artifact that the CLI, Studio, and CI can all inspect.

Audit planes

The computed model is the truth surface. Audit planes are the inspection surface for how that truth changed across committed heads.

JacqOS exposes three derived audit planes:

• Fact plane records fact additions and removals by committed head.
• Intent plane records when intents enter and exit the active worldview.
• Attempt reports record each evaluation attempt and whether it committed or was rejected.

That gives you a bounded operational history without introducing hidden state.

$ jacqos audit facts --lineage default --from 12 --to 18
head | change | relation          | tuple
-----+--------+-------------------+--------------------
13   | add    | triage.root_cause | ["db-primary"]
18   | remove | triage.root_cause | ["db-primary"]

$ jacqos audit intents --lineage default --from 12 --to 18
head | transition | relation                  | tuple                      | request_id
-----+------------+---------------------------+----------------------------+-----------
14   | enter      | intent.notify_stakeholder | ["db-primary","sev1"]      | req-014

$ jacqos audit attempts --lineage default
head | outcome   | prior_committed_head
-----+-----------+---------------------
14   | committed | 13
15   | rejected  | 14

These views are especially useful when provenance tells you why one tuple exists, but you also need to know when the worldview changed shape. Audit planes answer that second question directly.

Connection to the North Stars

North Star 1 says JacqOS gives you Model-Theoretic Simplicity: one computed model, shared by every agent, with deterministic semantics.

Rule shapes, monotonicity classification, Gaifman locality, namespace reducts, composition analysis, and audit planes are the inspection side of that same promise.

• Rule shapes explain whether joins stay grounded.
• Monotonicity explains where derivation only grows versus where it arbitrates.
• Gaifman locality explains why a bad derivation has a small witness.
• Namespace reducts explain where module boundaries really are.
• Composition analysis explains whether multi-agent boundaries stay safe as the ontology grows.
• Audit planes explain how the worldview changed across committed heads.

These are not optional extras. They are what it looks like when application state is a computed model instead of a pile of hidden workflow state.

Next steps

• Multi-Agent Patterns shows these ideas in the incident-response app.
• Visual Provenance shows how locality becomes a debugging workflow in Studio.
• Invariant Review shows how the same model becomes a safety boundary.
• .dh Language Reference documents the syntax behind rule-shape-friendly authoring.
• CLI Reference covers jacqos verify and jacqos stats in detail.

Going deeper

Everything on this page stops at the named level — Gaifman locality, the guarded fragment, CALM, amalgamation. The formal treatment lives in MODEL_THEORY_REFERENCE.md at the repo root. That document covers:

• the precise definitions of monotonicity, stratification, and the least-fixed-point semantics JacqOS evaluates;
• the proofs that the guarded fragment of stratified Datalog is decidable and that JacqOS’s restrictions stay inside it;
• the locality theorems that justify Studio’s neighborhood-first debugging UI;
• the namespace-reduct analysis used by composition checks;
• the CALM theorem application that classifies which strata are safely distributable and which are not.

Read MODEL_THEORY_REFERENCE.md if you want the proofs themselves. Otherwise this page is the last layer you need before Studio and jacqos verify start telling you the same things in product language.