# ADR-0201.1 — Principled Out-of-Regime Detector (`out_of_decidable_regime`)

**Status:** Accepted (additive hardening of ADR-0201; phase-1 canonicalizer)
**Date:** 2026-06-02
**Relates to:** **ADR-0201** (propositional canonicalizer — this hardens it; see
§amend-vs-additive), ADR-0202 §3 (the contract that names this typed refusal),
ADR-0203 (the prior additive-not-amend precedent).

---

## Context

GPT-5.5's independent proof-chain corpus (the separate-author oracle for
`logic_canonical.py`) cross-checked **22/22** cases against the *real*
canonicalizer. Twenty agreed exactly; two — the out-of-regime probes
`forall x. rains(x) -> wet(x)` and `exists x. wet(x)` — agreed on **outcome**
(both refused) but disagreed on the **reason**:

- ADR-0202 §3 names a typed refusal: quantified/predicate input "must REFUSE
  (`out_of_decidable_regime`)."
- The keystone refused, but with a generic `LogicError: "unexpected character
  '.' at position 8"` — it had **no regime detector**. It refused these inputs
  only because the tokenizer incidentally chokes on the `.` (or trips on the
  predicate `(`).

That is a **by-luck-not-by-design refusal** — the exact failure mode the
`wrong == 0` discipline rejects. The propositional-only boundary that ADR-0202
declares load-bearing was being enforced by accident, not on purpose. Blessing
it (relaxing the contract) would write the accident into the contract. The
corpus caught precisely the thing an independent oracle exists to catch.

## Decision

Make the boundary principled. Add a typed regime refusal, checked **before** the
generic grammar error:

- **`LogicRegimeError(LogicError)`** carrying the typed reason
  `OUT_OF_DECIDABLE_REGIME = "out_of_decidable_regime"`. A `LogicError` subclass,
  so callers refusing on `LogicError` still refuse — but the regime boundary is
  now distinguishable from a malformed-propositional-formula grammar error.
- **`_reject_out_of_regime_text(formula)`** — a raw-text pre-scan (before
  tokenizing) for quantifier markers: the words `forall`/`exists` (word-boundary,
  case-insensitive) and the symbols `∀`/`∃`. `forall`/`exists` are thereby
  reserved — not usable as atom ids.
- **`_reject_out_of_regime_tokens(tokens)`** — a token-stream scan for
  **predicate-application shape**: an `ATOM` immediately followed by `(`. In the
  propositional grammar an atom is never followed by `(`, so `ATOM (` is a
  predicate (`rains(x)`), not a well-formed formula. Keyword operators (`not`,
  `and`, …) are not `ATOM` tokens, so `not (P)` is unaffected.
- `canonicalize` runs `_reject_out_of_regime_text` → `_tokenize` →
  `_reject_out_of_regime_tokens` → parse. `check_equivalence` surfaces the typed
  reason via a `LogicRegimeError` branch placed before its generic `LogicError`
  branch.

This is a **refusal**, not new capability: the engine still does no
predicate/FOL reasoning. It now refuses it **on purpose**, with an inspectable
typed reason, instead of by tokenizer accident.

## amend-vs-additive

**This is a new additive sub-ADR (ADR-0201.1), not an amendment of the landed
ADR-0201** — same discipline as ADR-0203-vs-0132: the regime detector became
load-bearing only when the corpus surfaced the incidental-refusal gap; recording
it additively preserves that *why-added-later* history rather than rewriting the
closed canonicalizer record.

Chosen as a **sub-number (0201.1), not a fresh top-level number**, for two
reasons: (a) it is specifically a hardening of the ADR-0201 canonicalizer (same
module, same phase-1 keystone), which the sub-number communicates precisely; and
(b) a top-level `ADR-0204` would collide with the forward references in the
already-merged ADR-0203 and the recorded phase-2 plan (`0204` = wiring, `0205` =
modus_ponens, `0206` = grounding). The sub-number keeps those intact.

## Honesty boundary (load-bearing — carried by every phase-2 ADR, 0203–0205)

Through phase 2.3, `proof_chain` is **sound over its declared atoms**, not
grounded in recognized input (grounding is phase 2.4). This ADR does **not**
soften that, and it does not add predicate/FOL reasoning — it makes the
**propositional-only** boundary principled by refusing out-of-regime input with a
typed reason. The boundary is enforced by design, never "reasons over input."

## Evidence

- `tests/test_logic_canonical.py` — 43 tests (33 keystone + 10 new): quantifier
  words/symbols and predicate application refuse with `LogicRegimeError` /
  `out_of_decidable_regime`; the equivalence path surfaces the typed reason;
  genuine grammar errors (`P &`, `P @ Q`, `(P`) still raise *plain* `LogicError`
  (detector does not over-fire); `not (P)` is not mistaken for predicate
  application.
- **Mutation-verified by-design:** neutering both detectors makes
  `forall x. …` fall through to the generic grammar error
  (`unexpected character '.'`) instead of the typed reason —
  `test_out_of_regime_refuses_with_typed_reason` would fail. The boundary holds
  on purpose, not by luck.
- **Corpus now 22/22:** the two OOR cases (PC-OOR-001/002) now agree on the
  principled `out_of_decidable_regime` reason.
- Full canonicalizer suite green; smoke: 67 passed.

## Note carried to the corpus (rule-reasons pending 2.3)

The 3 `modus_ponens` corpus cases were validated only at the **entailment** level
the canonicalizer provides (`(⋀premises) → conclusion` is/ isn't a tautology).
Their typed *rule* reasons (`modus_ponens_conclusion_mismatch`,
`modus_ponens_missing_implication`) are **deferred to ADR-0205** (phase 2.3), when
the `modus_ponens` rule is built. The corpus should carry an explicit
"rule-reasons pending 2.3" marker on those cases so the deferral is recorded, not
assumed validated.

## Scope

Phase-1 canonicalizer hardening only. Does **not** build `modus_ponens`,
binding-graph wiring, or any predicate/FOL support.
