Bitspark constellation

THEORY · EXPLORATORY

0002 — what a theory is, and the two tests

exploratory

2026-06-07

  • Status: exploratory
  • Date: 2026-06-07
  • Governed-by: ADR 0012
  • Builds on: 0001

The question is never "should artifacts be a primitive?" or "should runners get a repo?" Those are noun questions. The sharp question is: is there a checkable judgment about this that must be shared for safe late-bound use? — and, if so, can it be defined from the judgments we already have? Two tests, and a discipline rule that keeps the substrate narrow.

Four categories — keep them distinct

Most of the confusion dissolves once four things stop being called the same thing:

  • Primitive — a protected effect surface: facts, CAS/artifact binding, cell, wire. Uniform across spaces and not composable from existing primitives (the arche RFC 0001 test). A vault is not primitive — it is ciphertext in CAS plus metadata in facts; cell and wire are primitive because each adds a new protected-effect family.
  • Vocabulary — predicates and descriptors a population agrees to use. Cheap. Most things should start here and never leave.
  • Profile / interface — a concrete contract for a surface: operations, DTOs, an authority mapping, conformance vectors (arche RFC 0002 already separates resource class, interface profile, and revision).
  • Theory — a checkable family of judgments the system relies on across implementations. thesmos is not a permission vocabulary; it gives meaning to authorized. horos is not a schema registry; it gives meaning to v : T.

A theory is the heavyweight category. The bar to enter it is the two tests below.

Test 1 — when a theory is required (the challenge test)

A theory is required iff there is a rightful challenge to some admissible act that no existing theory can discharge.

You find theories by finding challenges, not by introspecting on goals. Walk the verb-on-operand admissions of admissible (0001) and ask what objection could rightfully block each: "by what right?" → authority. "in what form?" → form. "is that even a real, usable thing — and can it run here?" → the candidates of 0003. If every challenge to an act is already answered, you have enough; if one is not, something is missing.

The operational form of the same test — a theory is required if removing it forces one of these five bad outcomes:

  1. Hidden decider — some service decides with private code instead of a checkable account.
  2. Out-of-band registry — participants must trust a central catalog or a docs site.
  3. Semantic overload — an existing theory gets abused to carry a different kind of meaning.
  4. No late binding — a future system cannot be used without bespoke integration.
  5. No enforcement — the system can describe the concept but cannot gate on it.

And the four standing conditions a candidate must meet: it answers a substrate-level question (not a domain one — "may this actor do this?" qualifies; "is this invoice approved?" does not, unless it becomes an authority rule inside a space); the answer is needed before independent parties can compose; the answer is checkable, not merely asserted; and there is a gate (a service, runner, or host acting as a gate) whose operation depends on it.

Test 2 — when a theory is irreducible (the definability test)

A theory is irreducible iff its central judgment is not a definitional (conservative) extension of the others — it cannot be derived from the existing vocabulary via logos rules.

This is the logician's conservativity notion, and it is mechanical in principle: try to define the candidate judgment using only what you already have; if you can, it is not a new theory — push it back down to vocabulary or profile. authorized is not definable from v : T (permission is not a fact about shape), and v : T is not definable from authorized (form is not a fact about who may act). That mutual non-definability is exactly why authority and form are two theories and not one. The modal reading — may vs is — is the same observation: you cannot reduce one modality to the other.

Irreducible does not mean orthogonal — theories are a DAG

The subtle correction that prevents both over- and under-counting: a higher theory may use lower ones and still be irreducible over them. Capability (0003) leans on horos for the shapes in its operation signatures and on thesmos for the authority its effects require — yet "this entity affords this operation / requires this cell / emits on this wire" is not definable from shape-plus-permission. It is a non-conservative extension over {horos, thesmos}, not an addition beside them.

So "irreducible" must read as "adds a judgment not derivable from the lower layers, even while referencing them." Two consequences:

  • It dissolves the cheap dismissal "isn't capability just horos + thesmos + facts?" — it references them; it does not reduce to them.
  • The theories form a dependency DAG (ontos/logos are the medium; thesmos and horos are the mutually-irreducible base; capability and realization sit above), which fixes the build order: base before higher.

The discipline rule

Do not make a theory for a noun. Make a theory only for an irreducible judgment.

Not "artifact theory because artifacts exist," but "realization theory because participants must check whether artifact A under manifest M on host H can produce capability C and yield observation O." Not "runner theory because runners exist," but "runtime theory because participants must check that a desired declaration was validly turned into a running instance." The noun is a symptom; the judgment is the thing. This rule is what keeps the category from inflating.

Where this goes

0003 applies both tests to the live candidates and reads them off the modal structure of admissible. 0004 turns "required + irreducible" into the promotion path and shows what completeness can and cannot mean.

Open edges

  • The definability test is only as sharp as the logos rule-set you test against; "derivable" is relative to a fixed base, so the test answers "reducible to this base?", not "reducible in principle?".
  • The five-bad-outcomes form is goal-relative (it presumes the central goal of 0001); the conservativity form is formal. They usually agree; a case where they diverge would be worth recording.

The Bitspark constellation — how the systems are built and relate.

GitHub