# Validator Predicate Specification (SFT)

This file is the single source of truth for the **validator predicates** used in the declared-regime completeness contract.

## Role in the interface

Within a declared regime, SFT enforces a dichotomy:

- a **WSC** may be issued only when all *applicable* validator predicates hold on the declared target;
- otherwise the engine must emit a **WOB** whose `obstruction_code` is the canonical code associated to the first failed predicate.

The predicate-to-code mapping is **finite** and is treated as the formal content of the completeness claim.

## Canonical mapping

The canonical mapping is recorded in:

- `engine/contracts/validator_predicates.json` (machine-readable)
- `finish_ready/*/VALIDATOR_PREDICATE_SPEC.tex` (paper-facing table)
- `engine/contracts/wob_codebook.json` (the authoritative WOB code catalog)

## Artifact-level predicate ledger

WSC artifacts should include a **predicate ledger**:

```json
"validator_predicates": [
  {
    "predicate": "V06",
    "holds": true,
    "wob_code": "WOB-06-coupling-mismatch",
    "evidence_refs": ["engine/docs/coupled_atlas.md:Theorem 1 (CMT-SOL)"]
  }
]
```

Rules:

- `predicate` must be `V01`–`V15`.
- For a **WSC**, each listed entry must have `holds: true`.
- `wob_code` must be a canonical catalog code (see `wob_codebook.json`).
- `evidence_refs` are short pointers to where the check is justified (a theorem reference, benchmark output, or a file/section label).

The ledger is  lightweight: it is not a proof engine, it is an **audit interface**.

## Applicability

Predicates are only required when their mechanism is invoked.
If a predicate is not applicable to a certificate's mechanism/target type, it may be omitted from the ledger.

The audit logic implements the minimal applicability rules below:

- **Always required:** V01.
- **Embedded winding/loop mechanisms (LDW/HW):** V02 and V04; additionally V05 when `witness_value.kind == holonomy_multiple`.
- **Action-equivariant forcing (AWT):** V08 and V09.
- **Coupled target mechanisms (CMT or any target that is CST):** V06.
- **Mixing/convergence mechanisms (MXC):** V07.
- **CST/constraint inference (SFT III):** V13, V14, and V15 (reported by the inference tools as benchmark-auditable evidence).

## Predicate definitions (names are normative)

- **V01 → WOB-01-no-subsystem**: No admissible subsystem/observable exists in the declared regime.
- **V02 → WOB-02-trivial-winding**: The invoked loop mechanism has zero winding/holonomy multiple.
- **V03 → WOB-03-pinch**: The observable image misses a required arc neighborhood on the declared target.
- **V04 → WOB-04-tear**: The adopted model class does not support the regularity needed to define the witness invariant at the declared tolerance.
- **V05 → WOB-05-holonomy-defect**: The holonomy interface is inconsistent at tolerance, so the holonomy integer is not well-defined.
- **V06 → WOB-06-coupling-mismatch**: CTP/CHT violated — coupled setting declared but target/baseline is not CST + coupled Haar (ill-posed claim).
- **V07 → WOB-07-mixing-not-justified**: Statistical convergence asserted without an admissible hypothesis certificate (RNF or NDB+MXC).
- **V08 → WOB-08-orbit-collapse**: The required active orbit segment is not present on the declared evidence domain.
- **V09 → WOB-09-equivariance-defect**: Equivariance defect exceeds the declared tolerance.
- **V10 → WOB-10-resonant-locking**: Rank/constraint collapse makes the intended target too large.
- **V11 → WOB-11-disconnected-slice**: Evidence domain misses the component needed by the chosen mechanism.
- **V12 → WOB-12-slope-zero-quotient-nonsurjective**: Trivial homomorphism case but quotient factor is not surjective.
- **V13 → WOB-13-ambiguity**: Multiple incompatible constraint hypotheses fit within tolerance in the declared search; target inference is not uniquely determined.
- **V14 → WOB-14-insufficient-excitation**: Sample count or excitation is insufficient to support stable constraint/target-rank inference at the declared tolerance.
- **V15 → WOB-15-resonance-masking**: Near-relations or an insufficient stability margin make the inferred constraints unstable at the declared tolerance.

## Audit correspondence

The audits enforce the parts of the predicates that can be checked **from the artifact interface**:

- `engine/audit/audit_wsc.py` enforces:
  - presence and well-formedness of `validator_predicates` on WSCs,
  - minimal applicability coverage (V01 + mechanism-specific requirements),
  - coupled-target baseline correctness when CST is declared (V06),
  - convergence-certificate presence for MXC (V07),
  - holonomy margin presence when holonomy is invoked (V05).
- `engine/audit/audit_wob.py` enforces that every WOB code is in the canonical catalog.

Everything else (degree/holonomy recomputation, equivariance defect measurement, connectedness tests) is recorded as a **declared evidence reference**, and becomes fully machine-checkable as the evidence payloads are expanded.
