Invariant Sets

A one-parameter variational symmetry yields a conservation law along solutions.

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

Consider a team adding a "popular" predicate to a catalog and then finding that a standing query has changed. The investigation reveals: "popular" triggered a derived rule that changed the operational semantics of "trending." In this hypothetical case, the formal theory is held fixed while the query procedure for trending(·) is changed to consult the new predicate. The formal theorems therefore remain unchanged, but the implemented answers do not. Merely adding no axioms written wholly in the old language would not suffice: new-language axioms can entail new old-language conclusions.

The invariant check must reach the changed evaluator, not stop at the unchanged formal theory. 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.

Theorem: Conservative Extension Safety

The following standard criterion gives one way to establish the logical condition².

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
• Ranking, retrieval and “best-of” queries belong in Q_stable when a standing contract depends on them; their operation can be consequential even when their output is a score.

A proof of logical conservativity can therefore coexist with a broken query. A migration witness must identify the preservation claim that failed, so its recipient can find the affected use.

Typed Invariants

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

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

The same invariant can thus appear under different declared enforcement regimes. The table makes those choices inspectable; a recipient still needs to know who can change the regime governing its use.

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 may be a soft cost for exploratory ranking, or a hard failure where the promised decision requires that parameter.

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). If those are exactly the required parameters, specifying all three gives c_context = 0 in this counting convention. The convention itself does not measure how well the preferences were elicited.

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, pending = [], []
  for inv in I where EnforcementMode(inv, scope, auth) = Reject:
    result = check(q, inv)  // Passed(proof) | Violated(evidence) | Inconclusive(reason)
    if result is Inconclusive:
      pending.append((inv, result.reason))
    if result is Violated:
      hard_violations.append((inv, result.evidence))
  
  if hard_violations.non_empty():
    return Invalid { 
      violated_hard: hard_violations,
      incomplete_checks: pending,
      obstruction_witness: failed_obligation_evidence(hard_violations)
      // An unsat core is appropriate only for a checked inconsistent encoding.
    }
  
  if pending.non_empty():
    return Inconclusive { outstanding: pending }

  // 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: A proved rejection includes the evidence for the violated obligation. For an unsatisfiable finite set, a core may explain the conflict. Call it subset-minimal only if removing any member restores satisfiability; that is different from minimum cardinality. A heuristic or incomplete search cannot certify either property by failing to find a smaller core.

A proved rejection identifies the violated invariant and the evidence of violation. It may give the proposer a repair to attempt. An unfinished check instead identifies work still owed; it has supplied neither a successful certificate nor a counterexample.

Valid {
  hard_ok: true,
  soft_cost: [(coverage, 0.1), (naming, 0.1)],
  admission_score: U(affordable) - λ(0.2)  // sum of the two recorded costs
}

Touchstones as Invariant Species

The touchstones illustrate different invariant species.

T1 (Contradiction) is inconsistent commitments.

An empty answer does not necessarily assert an inconsistent theory. A query for integers between 1 and 100 greater than 200 has no answer in that finite range, though integers greater than 200 exist. A query for a prime divisible by 4 has no integer answer at all under the usual definitions. So does prime(x) ∧ even(x) ∧ x > 2.

Neither impossible query makes number theory inconsistent. The contradiction would be asserting that an integer satisfying it exists. The query can instead be answered by establishing that none does. A retrieval returning no records, without this argument, proves less.

Where unsatisfiability is established, the refusal record can include an inconsistent constraint subset and its checked derivation³. Minimality requires a separate check; an incomplete search is not such a witness.

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 the refusal contract. Here the checked inconsistent constraint set supplies the particular reason an existential answer cannot be certified.

T4 (Exactness) concerns the grounds required by the contract.

A contract demanding an exact count or decision requires the corresponding exact grounds. A discrete codomain alone does not prohibit statistical estimation: a probability or estimated integer count may be appropriate when represented and used as such.

Invariant: contract(q).requires_exact_result ⇒ evaluation(q) has the required exact grounds

An exact count of "r" in "strawberry" can be supported by a trace of the character positions or another adequate counting procedure. 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). Whether missing context blocks evaluation depends on the declared use; it is not uniformly a soft cost.

Invariant: is_preference_predicate(q) ⇒ has_context_fiber(q)
EnforcementMode: Penalize(c_context)  // exploratory use only; required parameters still reject

In an exploratory contract allowing incomplete preference information, the proposal may be retained with a recorded penalty. A use requiring the missing parameters must still reject it or obtain them; paying a penalty supplies no substitute for those grounds.

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.

A breaking change can be deliberate or defective. Its record should let a recipient distinguish an authorized revision from a failed preservation promise and identify the work the transition requires. Writing that record does not complete the migration.

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 {
  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.

MigrationWitness(puffy alias v1 → v2) = {
  conservativity_failures: {
    logical: null,  // model-expansion argument under the assumptions above
    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
}

Consequence

The alias puffy can continue to look familiar while directing queries to a different evaluator. Keeping the old symbol is not enough; the receiving view must say which dependencies and results it promises to preserve. Where preservation fails, a migration witness makes the affected uses available for an authorized decision rather than disguising the change as an extension.

A completed dossier identifies the invariants checked, the evidence obtained and any migration it requires. A proved violation and an unfinished check lead to different responses, even when both prevent ordinary admission. The next chapter applies that distinction to another attractive shortcut: treating two similar items as interchangeable for a further operation.