Invariant Sets: Guardrails for invention

A18Prose proofWhat must be preserved when new structure is introduced.

Any continuous symmetry of the action leads to a conservation law.
— Emmy Noether, 'Invariante Variationsprobleme' (1918)

This chapter formalizes the internal structure of predicate invention's third obligation -- invariant preservation -- defining two anchors: A17b (Conservative Extension), which distinguishes logical conservativity (no new theorems in the old language) from operational conservativity (stable queries return unchanged results under evidence and absence policies), and A18 (Invariant Set), which classifies invariants into four typed species (integrity, semantic, computational, authority) with scope-relative enforcement modes. The chapter develops the invariant checker with locally minimal obstruction witnesses, soft-constraint cost scoring, the migration witness formalism for breaking changes, and the connection of touchstones T1 (contradiction), T4 (exactness), and T8 (preference) to specific invariant species. The reader seeking the motivating narrative for why vocabulary extension requires these guardrails should consult Vol I, Chapter 7 (The Witness Protocol).

The Failure Mode We Are Fixing

A team adds a "popular" predicate to their catalog. Six months later, half their queries return wrong answers. The investigation reveals: "popular" triggered a derived rule that changed the operational semantics of "trending." No one noticed because the formal theory over Σ was unchanged: they did not add axioms in the old language. What changed was the query procedure for trending(·), an operational definition compiled from rules that reference the new predicate. The formal Σ-theorems were stable; the implementation drifted.

This is the landmine that invariant discipline prevents. Chapter 15 introduced Obligation 3 (Invariant Preservation) as a gate in predicate invention. This chapter develops what that gate is made of, how it produces proofs, and how vocabulary evolves when the gate says no.

The Third Mode does not avoid invariant violations. It makes them visible, typed, and actionable.

Two Levels of Conservativity

When we say "adding vocabulary shouldn't break things," we mean two different things that are easy to conflate.

Logical conservativity is the model-theorist's concern. Let T := (Σ, I) be a theory over signature Σ with invariants I, and let T′ := (Σ′, I′) be an extension.

A17b

A17b: Conservative Extension

A17b-Logical (Primary Form)(Shoenfield 1967): T′ is logically conservative over T iff for every Σ-sentence φ:

T′ ⊨ φ implies T ⊨ φ

Equivalent Form: For all M ⊨ T, there exists M′ ⊨ T′ with M′|_Σ = M.

Both forms say the same thing: no new theorems in the old language. Adding vocabulary does not create new consequences about old concepts.

A17b-Operational: T′ is operationally conservative over T with respect to stable query set Q_stable iff for every q ∈ Q_stable and every relevant view U:

result(q, T′, E, P, U) = result(q, T, E, P, U)

where E is the evidence base, P is the absence policy (A15), and U is the view/scope. Equality here means status-equality after the A15 adapter translates both sides into the common status space (true/false/unknown/conflict). (Equality is defined per query's codomain: exact for discrete results; tolerance/metric for continuous results.)

Breaking change: Any extension that fails either conservativity requires a migration witness.

Theorem: Conservative Extension Safety

The following theorem, adapted from standard model theory(Shoenfield 1967), establishes that properly constructed extensions preserve all existing truths.

Theorem(Conservative Extension Safety)

Let $(\Sigma, I, L)$ be a theory (signature $\Sigma$ , constraints $I$ , logic $L$ ). Let $\Sigma' = \Sigma \cup \{q\}$ be an extension adding predicate $q$ with constraints $I' \supseteq I$ .

The extension is conservative over $(\Sigma, I, L)$ iff for every $\Sigma$ -sentence $\varphi$ :

(\Sigma', I', L) \vdash \varphi \quad \Longleftrightarrow \quad (\Sigma, I, L) \vdash \varphi

That is: the new predicate does not create new theorems in the old language.

Proof

Proof (model-theoretic):

Let $M \models (\Sigma, I)$ be a model of the original theory.
Extension: We must show $M$ extends to $M' \models (\Sigma', I')$ . Since $q$ is new (not in $\Sigma$ ), we can interpret $q^{M'}$ as any subset of the appropriate product of domains that satisfies the new constraints $I' \setminus I$ . If such an interpretation exists, $M$ extends.
Conservativity: Suppose $(\Sigma', I', L) \vdash \varphi$ for a $\Sigma$ -sentence $\varphi$ . By completeness (for the relevant logic), $\varphi$ holds in all models of $(\Sigma', I')$ . In particular, it holds in all extensions of models of $(\Sigma, I)$ . Since $\varphi$ is a $\Sigma$ -sentence, its truth depends only on the $\Sigma$ -reduct. Therefore $\varphi$ holds in all models of $(\Sigma, I)$ . By completeness, $(\Sigma, I, L) \vdash \varphi$ .
Converse: If $(\Sigma, I, L) \vdash \varphi$ , then every model of $(\Sigma', I')$ is an extension of some model of $(\Sigma, I)$ , so $\varphi$ holds.

Failure mode: The extension fails to be conservative if the new constraints $I' \setminus I$ entail $\Sigma$ -sentences not provable from $I$ alone. Example: adding $q$ with constraint $q(x) \to p(x)$ where $p$ is an existing predicate creates a conservative extension. Adding $q$ with constraint $\forall x.\, q(x)$ and $q(x) \to p(x)$ forces $\forall x.\, p(x)$ , which is non-conservative if $\forall x.\, p(x)$ was not previously provable.

∎

The "popular → trending" landmine is a failure of operational conservativity, not logical conservativity. The theory gained no new Σ-theorems (trending was an operational procedure, not a Σ predicate). But a derived rule activated, changing query results in ways that violated engineering expectations.

The key distinction: Logical conservativity is a property of theories. Operational conservativity is a property of implementations of those theories under evidence and absence policies.

Q_stable is the set of queries whose semantics you commit not to change without explicit migration:

Integrity checks, compliance flags, billing computations, safety gates, audit queries
Not included: ranking, retrieval, "best-of" queries (these are soft by design)

The distinction matters because logical conservativity is what enables formal reasoning about extension safety, while operational conservativity is what prevents production incidents. A migration witness must diagnose which kind failed.

Typed Invariants

Invariants are not a homogeneous mass. They come in types, and different types have different enforcement semantics.

A18

A18: Invariant Set

An invariant set I is a collection of typed invariants:

Invariant Types:

Integrity: first-order constraints (type, cardinality, mutual exclusion)
Semantic: equivalence/transport constraints (interacts with A16)
Computational: complexity/latency class
Authority: who may assert/promote

Enforcement: EnforcementMode(inv, scope, auth) ∈ (Reject, Penalize, Warn, Ignore)

Validity: A predicate q is valid relative to I in scope U with authority A iff:

All invariants with EnforcementMode = Reject are satisfied
Soft costs are computed for invariants with EnforcementMode ∈ (Penalize, Warn)

The key insight: hard versus soft is not metaphysical. It is enforcement mode, relative to scope and authority. Latency bounds might be hard in a trading system and soft in a batch pipeline. Authority bounds might be hard globally but warn-only in a sandbox scope.

Integrity invariants are about structure:

Type constraints: puffy : Dress → Score (not puffy : String → Float)
Cardinality constraints: primary_category is single-valued
Mutual exclusions: a dress cannot be both minimalist and maximalist (for merchandising purposes)
Logical consistency: no contradictory commitments (T1)

Semantic invariants are about equivalence:

Transport constraints: equivalence witnesses must exist for substitution (A16)
Overlap agreement: restrictions must be reconcilable on shared territory (A13)

Computational invariants are about resources:

Latency bounds: evaluation completes within T ms
Complexity class: evaluation is tractable
Resource bounds: memory, API calls, external dependencies

Authority invariants are about permission:

Scope bounds: user predicates cannot claim system authority
Promotion gates: org-level requires admin approval
Audit requirements: certain predicates require provenance

Scope-Relative Enforcement

Invariants are indexed by view. Some are global; some are local. This is Part III's context machinery in operation.

Consider the sustainable predicate from Chapter 15. Merchant A's sustainable (material-based) and Merchant B's sustainable (certification-based) operate under different invariant regimes:

A has an integrity invariant on material vocabulary: sustainable items must have material in (organic_cotton, recycled_polyester, linen)
B has an authority invariant on certification bodies: sustainable items must have a certification from an approved list

These are not just an overlap disagreement. They are different invariant sets. When the system tries to merge, it discovers not just value conflicts but invariant conflicts. The resolution requires either forking the predicate (sustainable_A, sustainable_B) or negotiating a shared invariant regime with authority approval.

The enforcement function takes three arguments:

EnforcementMode(inv, scope, auth) → Reject | Penalize(cost) | Warn | Ignore

A latency invariant with a 10ms bound might return:

Reject in trading_scope with any authority
Penalize(high) in realtime_search_scope with user authority
Warn in batch_scope with system authority
Ignore in sandbox_scope with any authority

This flexibility is essential. Without it, every new scope would require a new invariant, and the system would collapse under its own weight. With it, the same invariant expresses different enforcement regimes across the site of views.

Example(Latency Invariant Across Scopes)

Invariant: evaluation_latency(q) ≤ 10ms

Scope	Authority	EnforcementMode
trading	any	Reject
realtime_search	user	Penalize(100)
realtime_search	system	Reject
batch_pipeline	any	Warn
sandbox	any	Ignore

The same invariant, different enforcement. The trading system cannot tolerate latency violations; the sandbox exists precisely to test predicates that might violate production constraints.

Soft Constraints and Cost

Soft constraints accumulate cost rather than causing rejection. The cost is explicit:

soft_cost(q) = (c_coverage, c_latency, c_uncertainty, c_context, ...)
admission_score(q) = hard_ok(q) ? U(q) - λ · soft_cost(q) : -∞

Validity vs admission: Hard invariants decide validity (admissible or invalid). Soft constraints decide price. A separate admission policy may decline low-utility predicates even when valid. A predicate with high utility U(q) but moderate soft cost is valid and likely accepted. A predicate with low utility and high soft cost is valid but may be deferred by the admission policy. The invariant gate and the admission gate are distinct.

T8 (Preference) illustrates soft constraints. "Best restaurant in Berlin" is not a hard truth. The predicate is valid, but it lacks context. The soft cost c_context measures how much preference fiber is specified. Missing context does not reject the predicate; it penalizes it.

best : Restaurant × PreferenceContext → Score
c_context(best) = 1 - |specified_fiber| / |required_fiber|

A "best" predicate with no context specified has c_context = 1 (maximum penalty). A "best" predicate with cuisine, price_range, and ambiance specified has c_context ≈ 0.

The Invariant Checker

When a predicate candidate enters the system, the invariant checker evaluates it against the invariant set in the relevant scope with the declared authority.

InvariantChecker(q: PredicateSpec, I: InvariantSet, scope: Scope, auth: Authority):
  
  // Phase 1: Hard invariant checking
  hard_violations = []
  for inv in I where EnforcementMode(inv, scope, auth) = Reject:
    if violates(q, inv):
      hard_violations.append(inv)
  
  if hard_violations.non_empty():
    return Invalid { 
      violated_hard: hard_violations,
      obstruction_witness: compute_local_unsat_core(q, hard_violations)
    }
  
  // Phase 2: Soft constraint scoring
  soft_costs = []
  for inv in I where EnforcementMode(inv, scope, auth) ∈ (Penalize, Warn):
    cost = evaluate_cost(q, inv)
    soft_costs.append((inv, cost))
  
  return Valid { 
    hard_ok: true, 
    soft_cost: soft_costs,
    admission_score: utility(q) - λ · aggregate(soft_costs)
  }

Locally minimal obstruction witnesses: When rejection occurs, the witness includes a locally minimal set (with respect to the checker's heuristic) of invariants and facts sufficient to derive the violation. This makes the output actionable. Computing true minimal cores can be expensive or undecidable depending on logic and constraints, so the system returns a locally minimal core when available, otherwise a small witness set sufficient to diagnose the failure.

The output is not "no." The output is "no, because of these specific invariants and these specific facts, and here is the smallest proof I can find."

The distinction between rejection and actionable rejection is the difference between a wall and a door with a lock. The wall stops you; the door with a lock tells you what key you need.

Example(Invariant Checker in Action)

A user proposes a predicate affordable : Dress → Bool defined as price < $50.

Invariant check in catalog_view with user authority:

Invariant	Type	Enforcement	Result
type constraint	Integrity	Reject	✓ (Dress → Bool is valid)
price_unit_consistency	Integrity	Reject	✓ (USD assumed, matches catalog)
authority_bounds	Authority	Reject	✓ (user can define bool predicates)
coverage_target(0.8)	Computational	Penalize	cost = 0.3 (only 70% of dresses have price)
naming_convention	Authority	Warn	warning: consider "is_affordable"

Result:

Valid {
  hard_ok: true,
  soft_cost: [(coverage, 0.3), (naming, 0.1)],
  admission_score: U(affordable) - λ(0.4) = 0.72
}

The predicate is admitted with recorded costs. A different user in a compliance_view with stricter coverage requirements might see coverage enforced as Reject, not Penalize.

Touchstones as Invariant Species

The touchstones illustrate different invariant species.

T1 (Contradiction) is inconsistent commitments.

T1 is not merely an empty result set. Consider two queries:

"Integers 1–100 that are both prime and divisible by 4" has an empty result set but is not a contradiction. The constraints are consistent; they just have no solutions in that range.
"prime(x) ∧ even(x) ∧ x > 2" is a contradiction. The only even prime is 2, so the conjunction is unsatisfiable for x > 2.

These are different species:

Inconsistent: unsatisfiable in the theory (no model exists) → hard invariant violation
Empty: satisfiable but no solutions in the queried finite range → valid result, not a violation

Only inconsistency is a hard invariant violation. Emptiness is a valid result accompanied by a witness that the constraints are satisfiable even if the queried finite range has no solutions.

Contradiction (inconsistency) is about inconsistent commitments (A1). The system returns an unsat core(Bjørner 2008): a minimal inconsistent subset of constraints plus a short derivation chain showing why they conflict.

UnsatCore(T1_example) = {
  constraints: [prime(x), even(x), x > 2],
  derivation: [
    "The only even prime is 2 (number theory)",
    "x > 2 excludes 2",
    "Therefore no x satisfies all three constraints"
  ],
  type: "logical_contradiction"
}

Chapter 25 develops T1 fully. Here we establish that contradiction is a hard invariant with a specific artifact: the unsat core.

T4 (Exactness) is discrete codomain requires exact trace.

If a predicate's codomain is discrete (integer count, boolean, enumeration), the evaluation method must produce an exact trace. Statistical approximation is a hard invariant violation for discrete codomains.

Invariant: codomain(q) ∈ Discrete ⇒ evaluation(q) ∈ ExactTrace

Counting "r" in "strawberry" requires an exact trace: the character positions where "r" occurs. An embedding-based retrieval that returns "probably 3" violates this invariant. The enforcement is Reject in any scope where exactness matters.

T8 (Preference) is missing context fiber.

"Best restaurant in Berlin" is valid but incomplete. The invariant is not "best must have one answer" but "best must be fibered over preference context" (A14). Missing context is a soft cost, not a hard violation.

Invariant: is_preference_predicate(q) ⇒ has_context_fiber(q)
EnforcementMode: Penalize(c_context)

The predicate is admitted with a recorded penalty. Downstream systems can decide whether to use it based on the penalty magnitude.

Breaking Changes and Migration

When conservativity fails, the system produces a migration witness. A migration witness is not an apology but a map for how to update.

Breaking changes are not failures of the system. They are governed transitions. The system's job is not to prevent change but to make change auditable. Vocabulary evolution is a fact of life; the question is whether you discover the consequences six months later in a production incident or six seconds later in a migration witness.

Four migration strategies:

Rename is the simplest: old_name becomes new_name. No semantic change, just relabeling. The migration witness records the mapping and updates all references.

Version is the most common: old_v and new_v coexist with a compatibility witness. The compatibility witness (often a calibration or refinement witness) documents how values in one version relate to values in the other. Downstream consumers can choose which version to use based on their tolerance for change.

Deprecate is version with a timeline: the old symbol has a sunset date, after which it becomes unavailable. The migration witness includes a replacement and a transition plan.

Invalidate is the nuclear option: affected queries must be rewritten. The migration witness includes the list of affected queries and remediation guidance. This strategy is rare but necessary when the semantic change is too large for compatibility witnesses.

MigrationWitness

MigrationWitness {
  extension: Σ → Σ′,
  conservativity_failures: {
    logical: [(φ, derivation), ...] | null,
    operational: [(q, old_result, new_result, root_cause, view), ...] | null
  },
  affected_scopes: [Scope, ...],
  migration_strategy: MigrationStrategy,
  authority_approval: AuthorityRef,
  logic: L  // conservativity is logic-dependent (A15)
}

where MigrationStrategy =
  | Rename { old_name, new_name }
  | Version { old_v, new_v, compatibility_witness }
  | Deprecate { old_symbol, sunset_date, replacement }
  | Invalidate { affected_queries, remediation }

The migration witness diagnoses which conservativity failed. A logical failure means new theorems about old vocabulary. An operational failure means query results changed in some view. The root cause field explains why: a derived rule activated, an authority escalation reinterpreted existing claims, or a redefinition was disguised as an extension.

Example(puffy_v1 → puffy_v2 Evolution)

puffy_v1: volume_ratio / max_volume (measurement, deterministic) puffy_v2: learned_classifier trained on expanded exemplar set (new symbol in Σ′)

Question: Is puffy_v2 conservative over puffy_v1?

The key insight: puffy_v2 must be a new symbol, not a redefinition of puffy_v1. If we simply changed the interpretation of puffy, that would be theory revision, not extension, and could change Σ-consequences involving puffy.

Logical conservativity: Preserved, because Σ′ = Σ ∪ (puffy_v2) adds a new symbol rather than redefining puffy_v1. No new theorems about the old vocabulary.

Operational conservativity: Preserved for stable queries that reference puffy_v1. Violated only if the system aliases puffy := puffy_v2 without migration.

Breaking change trigger: The alias flip is what requires the migration witness.

MigrationWitness(puffy alias v1 → v2) = {
  conservativity_failures: {
    logical: null,  // Σ′ properly extends Σ
    operational: [<affected items with old/new scores, alias flip reason>]
  },
  affected_scopes: [catalog_view, search_view],
  migration_strategy: Version {
    old_v: puffy_v1,
    new_v: puffy_v2,
    alias_policy: "puffy := puffy_v2 after migration",
    compatibility_witness: <calibration witness linking old and new>
  },
  authority_approval: catalog_admin_ref,
  logic: classical_with_OWA
}

The migration witness records:

Logical conservativity holds (no new theorems)
Operational conservativity fails (query results differ)
The specific items that changed, by how much, in which views
A versioning strategy with a calibration witness showing 89% agreement within tolerance 0.15
Authority approval from catalog admin

Consequence

Invariants are not bureaucracy but the mechanism that makes vocabulary extension trustworthy.

Without invariant discipline, every new predicate is a potential landmine. The "popular → trending" failure happens silently, and you discover it six months later when half your queries are wrong.

With invariant discipline, every new predicate comes with a validity certificate:

Hard invariants verified (with locally minimal witnesses for any failures)
Soft constraints scored (and exposed to the admission policy)
Migration witness (if any) attached

The dossier from Chapter 15 now has a complete invariant section. Predicate invention is not just governed by three obligations; the third obligation has typed invariants, two-level conservativity, scope-relative enforcement, and actionable proofs when things go wrong.

The architecture is now complete:

Chapter 15: the three-obligation pipeline for predicate invention
Chapter 16: the internal structure of Obligation 3 (typed invariants, two-level conservativity, scope-relative enforcement, migration witnesses)

A predicate that passes all three obligations arrives with a dossier. A predicate that fails Obligation 3 arrives with a locally minimal obstruction witness explaining exactly what invariants were violated and what facts contributed to the violation. Neither outcome is silent. Both are auditable.

Chapter 17 asks the next question: what is the relationship between similarity (embeddings) and equivalence (witnesses)? If two items are "similar," can we use that for anything? The embedding empire claims similarity is useful. The Third Mode asks: useful for what operations? With what guarantees? Under what invariants?