Epharmoge Protocol

── FLOW ──
Epharmoge(R, X) → Eval(R, X) → Mᵢ? →
  Mᵢ = ∅: → deactivate (no aspect ¬warranted; execution stands as-is)
  Mᵢ ≠ ∅: ∀m ∈ Mᵢ: bind_kind(m) → certify(m, graph.json) → keep(status = pass) → Mᵢ_passed →
    Mᵢ_passed = ∅ ∧ no deferred-pending ∧ adjudicated(R, X) (every flagged aspect resolved to ROUTED or TERMINAL-RESIDUAL via the typed routed(a)/terminal_residual(a) predicates — deferred mismatches first get their one bounded re-assessment to pass→registered, route→Λ.routed, or terminal-residual→Λ.residual): → emit routing recommendations + surface any terminal-residual (each flagged aspect either routed to a sibling deficit or terminal-residual/unattributable) → deactivate (trivial convergence: adjudicated by routing/terminal-residual, R unadapted)
    Mᵢ_passed ≠ ∅: AssessFit(R, X, Mᵢ_passed) → F → Register(Mᵢ_passed) → SelectNext(pending, F, Σ) → Mₛ → Q(F-scoped Mₛ) → A →[mutating: A ∈ {Confirm, Adapt}] adapt → R' → Eval(R', X) → Mₑ? (Dismiss: R' := R, no re-scan, no Mₑ) → ∀m ∈ Mₑ: bind_kind(m) → certify(m, graph.json) → keep(status = pass) → Mₑ_passed → Register(Mₑ_passed) → AssessFit(R', X, pending) → F' → (loop: SelectNext → Q → A → adapt → re-scan until contextualized)

── MORPHISM ──
(R, X)
  → evaluate(result, context)          -- detect applicability mismatch
  → bind_kind(mismatch) → certify(mismatch, registry) -- shared meta-backbone: bind each mismatch as a kind, certify deficit fit (fail-closed) at REGISTRATION, BEFORE it enters the pending/adaptation flow
  → assess_fit(result, context, mismatches) -- sort applicability fit before user judgment
  → surface(fit_scoped_mismatch, as_inquiry) -- present mismatch with fit basis and evidence
  → adapt(result, direction)           -- adapt result to context (transformative revalidation: mutates Eval target → may breed Mₑ)
  → ContextualizedExecution
requires: mismatch_detected(R, X)       -- runtime checkpoint (Phase 0)
deficit:  ApplicationDecontextualized    -- activation precondition (Layer 1/2); certificate.owner for in-scope mismatches
preserves: X                             -- application context is fixed reference; morphism transforms R only
invariant: Applicability over Correctness
invariant: certificate-before-registration  -- DeficitFitCertificate.status = pass strictly precedes registering a mismatch into pending(Σ) (shared meta-backbone order, at registration of both Mᵢ and Mₑ)
invariant: transformative revalidation (NON-MONOTONE) -- adapting R' mutates the Eval(R, X) target, breeding emergent mismatches Mₑ; re-scan mandatory; progress(Λ) may regress. Opposite of distill's read-only-of-source monotone side (the contextualize ↔ distill boundary)

── TYPES ──
R      = Result to be evaluated (source-agnostic: AI output, analysis conclusion, decision outcome, or any completed work product)
           -- Input type: morphism processes R uniformly; enumeration scopes the definition, not behavioral dispatch
X      = Application context (environment, constraints, user situation)
Eval   = Applicability evaluation: (R, X) → Set(Mismatch)
Mismatch = { aspect: String, description: String, evidence: String, severity: Severity, origin: Origin, kind_binding: KindBinding, certificate: DeficitFitCertificate }
                 -- object_ref: the per-mismatch anchor the certificate evaluates and the value-space binds over (epharmoge-local instantiation of the shared backbone's object_ref)
                 -- the mismatch's kind/domain is carried by kind_binding.label (Axis = String, emergent); no separate dimension field (single source of the kind label)
Origin ∈ {Initial, Emerged(aspect)}                            -- mismatch provenance: initial scan or spawned by adapting parent aspect
Severity ∈ {Critical, Significant, Minor}                      -- Significant requires demonstrable behavioral impact (current-session task graph / downstream protocol activations); see Rule 12

-- Shared meta-backbone (KIND dispatch, registration-time / cycle-emergent). One canonical schema; epharmoge-local instantiation ONLY for object_ref (= Mismatch), local_value_space (= the answer coproduct {Confirm, Adapt, Dismiss}), and guard routing targets.
KindBinding    = { label: Axis, positive_predicate: String, evidence: Set(Evidence), origin ∈ {seed, emergent}, atomicity ∈ {atomic, non-atomic} }
                 -- captures the mismatch as a kind; if atomicity = non-atomic (the mismatch bundles two distinct aspects) → split BEFORE certify (no registration, no surfacing on a compound mismatch)
DeficitFitCertificate = { owner: Deficit, in_scope_if: String, route_if: List<RoutePair>, evidence: Set(Evidence), status ∈ {pass, route, ambiguous} }
                 -- fail-closed: status ≠ pass BLOCKS registration into pending(Σ) AND surfacing this mismatch for answer. Generated at registration time (Phase 0 for Mᵢ, Phase 2 re-scan for Mₑ) by fitting KindBinding.positive_predicate against the documented sibling-deficit scopes — each sibling protocol's deficit: declaration (its SKILL.md deficit: line + the CLAUDE.md protocol-pair table), with .claude/skills/verify/graph.json supplying the deficit inventory (which sibling deficits exist as nodes; epharmoge has no outgoing routing edge, so the fit rests on the deficit-scope declarations, not on edge topology).
                 -- owner = ApplicationDecontextualized when the mismatch is in-scope; status = pass iff the mismatch's positive_predicate fits ApplicationDecontextualized and no sibling deficit claims it
                 -- status = route: a sibling deficit owns the mismatch (backward misfit) → emit RoutePair target, drop the mismatch from registration (it never enters pending(Σ))
                 -- status = ambiguous: overlapping deficit fit → defer the mismatch for ONE bounded re-assessment at the fixed detection state ((R, X) for Mᵢ at Phase 0, (R', X) for Mₑ at the Phase 2 re-scan; AI-side, no user interaction; Phase 0 stays silent for Mᵢ) → pass / route / terminal-residual; never register/surface under ambiguous fit
RoutePair      = (route_if_predicate: String, target: Protocol)
                 -- epharmoge-local guard routing targets — BACKWARD misfit the loop routes away rather than adapting in-place:
                 --   an unnoticed decision gap rather than a context-fit question        → /gap        (GapUnnoticed)
                 --   a missing pre-execution fact (no observable value, requires supply)  → /inquire    (ContextInsufficient)
                 --   undefined convention/dependency ownership for the decision           → /bound      (BoundaryUndefined)
                 --   portability to an absent zero-memory recipient (not present fit)      → /distill    (ContextTethered) -- the contextualize ↔ distill boundary guard
Evidence       = { source: ContextChannel, content: String }
ContextChannel ∈ {Result, Context, Convention, Environment, Session}  -- observable sources for the certificate's deficit-fit basis (R itself + observable X)
V              = bind_value_space : Mismatch → ValueSpace       -- the mismatch's answer constructors; generated ONLY after certificate.status = pass; frozen for the cycle (relay / dead-signal test applied)
ValueSpace     = the mismatch's answer coproduct (local_value_space; epharmoge-local instantiation point) = {Confirm, Adapt, Dismiss}
Deficit        = the sibling-deficit label a mismatch may belong to (sourced from each protocol's documented deficit: declaration; the protocol that OWNS the deficit is a node in graph.json and the deficit/edge relations are its edges — the deficit label itself is NOT a graph.json node); owner = ApplicationDecontextualized for in-scope mismatches
Protocol       = downstream protocol slash target a routed mismatch is handed to (e.g., /gap, /inquire, /bound, /distill)
Axis           = String                                        -- emergent kind label; examples: "convention", "environment", "audience", "dependency"
Mᵢ_passed = { m ∈ Mᵢ : certificate(m).status = pass }          -- initial mismatches that passed the fail-closed certificate at registration
Mₑ_passed = { m ∈ Mₑ : certificate(m).status = pass }          -- emerged mismatches that passed the fail-closed certificate at re-scan registration
AssessFit = Applicability fit assessment: R × X × Set(Mismatch) → F
           -- classifier over input_mismatches; does not generate new Mismatch objects
F      = ApplicabilityFitMap { fit_justifications, conflicts, depends, adaptation_options, open }
fit_justifications = Set(AspectFit) where aspect(R) is warranted in X
AspectFit = { aspect: String, evidence: String }
conflicts = Set(Mismatch) where evidence shows result behavior or meaning conflicts with X
           -- invariant: conflicts ⊆ input_mismatches
depends = Set(ContextCondition) where fitness hinges on an observable but unverified condition that could change adaptation or dismissal
ContextCondition = { target: Mismatch, condition: String, evidence: String, consequence: String }
                 -- invariant: target ∈ input_mismatches
adaptation_options = Set(AdaptationOption) where each option is tied to a conflict or dependency
AdaptationOption = { target: Mismatch ∪ ContextCondition, direction: String, effect: String }
open   = Set(ApplicabilityQuestion) where the answer could materially change the next adaptation judgment
ApplicabilityQuestion = { target: Mismatch, condition: String, reason: String, evidence_needed: String }
                       -- invariant: target ∈ input_mismatches
fit_category(m, F) =
  Conflict if m ∈ F.conflicts
  Dependent if ∃d ∈ F.depends : d.target = m
  Open if ∃q ∈ F.open : q.target = m
  Supported otherwise
FitRank = Conflict > Dependent > Open > Supported
SelectNext = Set(Mismatch) × F × Σ → Mₛ
           -- priority: severity(Critical > Significant > Minor), then FitRank, then oldest registered task
Mₛ     = Selected mismatch
Mᵢ     = Identified mismatches from Eval(R, X)                 -- origin = Initial; each bind_kind'd + certified at registration (Phase 0)
Mₑ     = Newly emerged mismatches from Eval(R', X)             -- origin = Emerged(adapted_aspect); each bind_kind'd + certified at re-scan registration (Phase 2)
Register = { m ∈ Set(Mismatch) : certificate(m).status = pass } → Set(Task) [Tool: TaskCreate] -- registration of ONLY certificate-passing mismatches as tracked tasks; status ≠ pass blocks registration (fail-closed)
pending(Σ) = Set(Mismatch) where registered task status ∉ {completed, dismissed}  -- a routed/ambiguous mismatch never enters pending(Σ); only certificate-passing mismatches are registered
Q      = Applicability inquiry over F-scoped mismatch (gate interaction)
A      = User answer ∈ {Confirm(mismatch), Adapt(direction), Dismiss}  -- A ∈ V; answer drawn from the mismatch's value-space (local_value_space = {Confirm, Adapt, Dismiss})
R'     = Adapted result (contextualized output)
ContextualizedExecution = R' where (∀ task ∈ registered: task.status = completed) ∨ user_esc
                 -- registered = certificate-passing mismatches only; routed/ambiguous mismatches are handed forward, not adapted in-place

── PHASE TRANSITIONS ──
Phase 0: R → Eval(R, X) → Mᵢ? → ∀m ∈ Mᵢ: bind_kind(m) → certify(m, graph.json) → (status = pass) → Mᵢ_passed → AssessFit(R, X, Mᵢ_passed) → F → Λ.fit_map := F  -- applicability checkpoint + registration-time KIND dispatch (fail-closed) + fit map (silent); certify runs WITHIN Phase 0, at registration, not as a separate phase
Phase 0 → route_away (mismatch-local): certify(m).status = route        -- a sibling deficit owns the mismatch (backward misfit) → emit RoutePair.target (/gap, /inquire, /bound, /distill), drop m from registration (m never enters pending(Σ)); scan continues with remaining mismatches
Phase 0 → split (pre-certify): KindBinding.atomicity = non-atomic  -- a compound mismatch bundles two distinct aspects → split into atomic sub-mismatches and re-run bind_kind + certify on each (same Phase 0 pass, before any pass/route/defer decision); recursive until atomic (well-founded: each split strictly decreases the number of bundled aspects — atomic = exactly one aspect — so the recursion terminates). A non-atomic mismatch is NEVER deferred or registered as a compound
Phase 0 → defer (mismatch-local): certify(m).status = ambiguous  -- overlapping deficit fit on an ATOMIC mismatch → ONE narrowed-scope re-assessment at the fixed Phase-0 (R, X) (AI-side, no user interaction — Phase 0 stays silent), then re-certify. (R, X) is fixed in Phase 0, so a re-assessment is deterministic-identical → the bound is ONE attempt: resolves to pass (→ registered), route (→ Λ.routed), or — if it STAYS ambiguous — TERMINAL-RESIDUAL: record m in Λ.residual (an unattributable mismatch: never registered into pending(Σ), adjudicated by terminal_residual(aspect(m)), surfaced as residual, non-blocking). deferred-pending therefore always clears (no Phase-0 loop)
Phase 0 → deactivate (no in-scope mismatch): Mᵢ ≠ ∅ ∧ Mᵢ_passed = ∅ ∧ adjudicated(R, X) ∧ no deferred-pending ∧ pending(Σ) = ∅  -- mismatches WERE detected but EVERY one resolved to ROUTED or TERMINAL-RESIDUAL (both typed CONVERGENCE disjuncts — routed(a): a ∈ Λ.routed; terminal_residual(a): a ∈ Λ.residual; via aspect(m) = a, NOT raw Mismatch-in-list membership) — no in-scope (ApplicationDecontextualized-owned) mismatch enters the adaptation loop → trivial convergence: emit the routing recommendations (/gap, /inquire, /bound, /distill) and deactivate without adapting R (R stands as-is for the in-scope check; contextualized(R) holds vacuously — adjudicated(R, X) with every aspect routed or terminal-residual). DEFERRED mismatches (atomic, status = ambiguous; a non-atomic mismatch is split pre-registration, never deferred) are NOT terminal and do NOT satisfy this path: they first get their ONE bounded re-assessment via Phase 0 → defer until each resolves to pass (→ registered into pending(Σ)), route (→ Λ.routed), or terminal-residual (still ambiguous at the fixed Phase-0 (R, X) → unattributable residual, excluded from pending(Σ), non-blocking); the bound (one re-assessment per mismatch, (R, X) fixed in Phase 0) guarantees deferred-pending always clears. Trivial convergence fires once NONE remain deferred-pending and every flagged aspect is routed or terminal-residual (none in-scope/pending). Distinct from the zero-mismatch-detected case (Mᵢ = ∅, no aspect ¬warranted): here aspects WERE flagged but all belong to sibling deficits. The per-mismatch-certificate analogue of elicit's all-projections-routed exit
Phase 1: Mᵢ_passed → TaskCreate[all certificate-passing initial mismatches] → pending(Σ) → SelectNext(pending, F, Σ) → Mₛ → Qc(F-scoped Mₛ, evidence) → Stop → A  -- register all certificate-passing initial mismatches, surface selected mismatch with fit basis [Tool]; reached only when Mᵢ_passed ≠ ∅
Phase 2: A → (A ∈ {Confirm, Adapt}: adapt(A, R) → R' [mutating — transformative revalidation] | A = Dismiss: R' := R [non-mutating adjudication — no adapt]) → TaskUpdate → (mutating branch only: Eval(R', X) → Mₑ? → ∀m ∈ Mₑ: bind_kind(m) → certify(m, graph.json) → (status = pass) → Mₑ_passed → TaskCreate[all Mₑ_passed] → pending(Σ) → AssessFit(R', X, pending) → F' → Λ.fit_map := F') -- adapt mutates the Eval target (transformative revalidation) and triggers the re-scan + registration-time certify of emerged mismatches; Dismiss leaves R unchanged and breeds no Mₑ (no re-scan on the Dismiss branch) [Tool]
Phase 2 → route_away (mismatch-local): certify(m).status = route        -- an emerged mismatch a sibling deficit owns → emit RoutePair.target, drop m from registration; re-scan continues
Phase 2 → split (pre-certify): KindBinding.atomicity = non-atomic  -- emerged compound mismatch → split into atomic sub-mismatches, re-bind_kind + certify each (same re-scan pass); never deferred/registered as a compound
Phase 2 → defer (mismatch-local): certify(m).status = ambiguous  -- emerged overlapping (atomic) mismatch → ONE bounded narrowed-scope re-assessment at the fixed re-scan (R', X) (deterministic-identical → one attempt) → pass (→ registered) / route (→ Λ.routed) / terminal-residual (record m in Λ.residual), re-certify BEFORE registration

── LOOP ──
Transformative revalidation (NON-MONOTONE): this loop mutates the very object its detector evaluates. adapt produces R', and Eval(R', X) re-targets the detector at the mutated result — so an adaptation can BREED new mismatches Mₑ that did not exist before. This is the opposite of distill's read-only-of-source monotone side (the contextualize ↔ distill boundary). "Transformative revalidation" labels the ADAPT path; non-mutating adjudication (Dismiss, or routing a mismatch to a sibling deficit) is contextualize-internal — it does not mutate R — and is distinct from distill's read-only-of-source territory.
After Phase 2 (mutating branch only — A ∈ {Confirm, Adapt}): re-scan R' against X for remaining AND newly emerged mismatches. The Dismiss branch is non-mutating (R' := R), breeds no Mₑ, and triggers no re-scan.
Bind + certify each newly emerged mismatch at registration (fail-closed): only certificate-passing emerged mismatches (Mₑ_passed) are registered into pending(Σ); a routed mismatch is handed to its sibling deficit (/gap, /inquire, /bound, /distill); a non-atomic compound mismatch is split into atomic sub-mismatches and re-certified; an atomic ambiguous mismatch gets its one bounded re-assessment at the fixed re-scan (R', X) → pass / route / terminal-residual, before registration. AssessFit classifies tracked mismatches but never suppresses them.
Recompute F over pending(Σ) before selecting the next surfaced mismatch, even when Mₑ_passed = ∅.
If pending(Σ) non-empty: return to Phase 1 (SelectNext by severity, then FitRank, then oldest registered task).
If adjudicated(R', X): all tasks completed → convergence.
progress(Λ) MAY REGRESS: because re-scan over a mutated R' can register newly certified mismatches, the completed/total ratio is non-monotone — this is the signature of the transformative-revalidation side, not an error.
User can exit at Phase 1 (early_exit option or Esc).
Continue until: contextualized(R') OR user ESC.
Mode remains active until convergence.
Convergence evidence: At adjudicated(R', X), present transformation trace ranging over ALL dispositioned mismatches — Σ.history ∪ Λ.routed ∪ Λ.residual (routed and terminal-residual mismatches never enter pending(Σ)/Σ.history, so the trace must range over all three): for each (m, _) ∈ Λ.state.history (adapted/dismissed), show (ApplicationDecontextualized(m) → adaptation_result(m)); for each (m, target) ∈ Λ.routed, show (m → routed_to(sibling_deficit, target)) — NOT ApplicationDecontextualized(m), since status = route means a sibling deficit owns m (it was never in-scope for ApplicationDecontextualized); for each m ∈ Λ.residual, show (m → terminal_residual(unattributable)) — surfaced for the user as a residual the certificate could not attribute. Convergence is demonstrated, not asserted.

── CONVERGENCE ──
applicable(R', X) = ∀ aspect(a, R', X) : warranted(a, R', X)
warranted(a, R, X) = correct(R) ∧ fits(R, X)                -- correctness AND contextual fit required (not material conditional)
adjudicated(R', X) = ∀ aspect(a, R', X) : warranted(a, R', X) ∨ dismissed(a) ∨ routed(a) ∨ terminal_residual(a)
routed(a)          = ∃ m ∈ Λ.routed : aspect(m) = a    -- the mismatch on aspect a failed the certificate (status = route) and was handed to a sibling deficit; backward misfit is adjudicated by routing, not by in-place adaptation. aspect is a String label, so this disjunct discharges by label equality — it assumes aspects stay stable and uniquely labelled across the R→R' trajectory; a transformative re-scan could in principle surface a new R'-aspect colliding on a routed label, a documented low-probability assumption, not foreclosed by the type
terminal_residual(a) = ∃ m ∈ Λ.residual : aspect(m) = a  -- the mismatch on aspect a stayed ambiguous after its ONE bounded re-assessment at the fixed detection state ((R, X) for Mᵢ, (R', X) for Mₑ); unattributable (neither cleanly ApplicationDecontextualized-owned nor a sibling's), excluded from pending(Σ), adjudicated by being surfaced as a non-blocking residual (not adapted in-place, not silently dropped — Surfacing over Deciding)
contextualized(R') = adjudicated(R', X) ∨ user_esc
trivial convergence (all-routed): when Mᵢ ≠ ∅ but Mᵢ_passed = ∅ AND every flagged aspect resolved to ROUTED or TERMINAL-RESIDUAL — aspect-keyed via routed(a)/terminal_residual(a) over the atomic (post-split) aspects, not raw Mᵢ membership — (no deferred-pending, pending(Σ) = ∅), adjudicated(R, X) holds by the routed(a)/terminal_residual(a) disjuncts for every flagged aspect (and warranted for the rest) — R is unadapted and contextualized(R) holds. This is the Phase 0 → deactivate (all-routed) path. DEFERRED mismatches do NOT satisfy this: they are not in Λ.routed, so the routed(a) disjunct does not cover them; a deferred mismatch first gets its one bounded re-assessment (Phase 0 → defer) to pass (→ pending(Σ)), route (→ Λ.routed), or terminal-residual before any convergence claim. Distinct from the no-mismatch case (Mᵢ = ∅, every aspect warranted from the start) — here aspects were flagged but all belong to sibling deficits
certificate gate:  every registered mismatch carried certificate.status = pass (fail-closed, at registration) — routed/ambiguous mismatches never entered pending(Σ), so a contextualized R' is assembled only from in-scope (ApplicationDecontextualized-owned), fit-certified adaptations; backward misfit was handed forward (/gap, /inquire, /bound, /distill), not adapted in-place
-- stratification: applicable(R', X) ⊆ adjudicated(R', X)
-- operational proxy: ∀ task completed ⟹ adjudicated(R', X) ⟹ contextualized(R')
progress(Λ) = |completed_tasks| / |total_tasks|              -- NON-MONOTONE: may regress when re-scan over the mutated R' registers newly certified mismatches (transformative-revalidation signature)

── TOOL GROUNDING ──
-- Realization: Constitution → TextPresent+Stop; Extension → TextPresent+Proceed
Eval   (sense)   → Internal analysis (no external tool)
bind_kind (sense)   → Internal analysis (capture each detected mismatch as a KindBinding {label, positive_predicate, evidence, origin ∈ {seed, emergent}, atomicity}; non-atomic mismatch → split before certify)
certify (extension) → Internal analysis (fail-closed DeficitFitCertificate; fit of KindBinding.positive_predicate against the documented sibling-deficit scopes — the documented sibling-deficit scopes — each sibling protocol's deficit: declaration plus the .claude/skills/verify/graph.json deficit inventory (sibling-deficit nodes; epharmoge has no outgoing routing edge, so the fit rests on the deficit-scope declarations, not edge topology): owner = ApplicationDecontextualized when in-scope; status = pass | route | ambiguous; basis = the cited deficit-scope fit, shown at the mismatch's Phase 1 surfacing. Relay (Extension) because the fit is grounded in a citable source and an unclear fit returns status = ambiguous → defer, never a user gate. Runs at registration time — within Phase 0 for Mᵢ, within Phase 2 re-scan for Mₑ — BEFORE the mismatch enters pending(Σ))
AssessFit (sense) → Internal analysis (no external tool)
Qc     (constitution)    → present (mandatory; Esc key → loop termination at LOOP level, not an Answer)
adapt  (transform) → Edit, Write (result adaptation based on user direction)
                    -- (transform): tool call that changes existing artifacts; medium-agnostic (files, analysis text, generated content)
route  (extension)   → TextPresent+Proceed (certificate.status = route → emit the matching RoutePair.target as a backward-misfit recommendation: decision gap → /gap, missing pre-execution fact → /inquire, undefined convention/dependency ownership → /bound, portability to an absent recipient → /distill; the routing target is read off the matched sibling-deficit scope, basis cited)
Mᵢ/Mₑ (track)   → TaskCreate/TaskUpdate (mismatch tracking with framing visibility; only certificate-passing mismatches are registered)
converge (extension)  → TextPresent+Proceed (convergence evidence trace; proceed with contextualized execution)

── MODE STATE ──
Λ = { phase: Phase, R: Result, X: Context,
      fit_map: F, state: Σ, active: Bool, cause_tag: String,
      routed: List<(Mismatch, Protocol)>,   -- backward-misfit mismatches handed forward (never entered pending(Σ))
      deferred: Set(Mismatch),   -- ATOMIC mismatches with certificate.status = ambiguous, parked for their ONE bounded narrowed-scope re-assessment against the fixed detection state — (R, X) for an initial mismatch (Phase 0), (R', X) for an emerged mismatch (Phase 2 re-scan) (a non-atomic mismatch is split pre-registration, never parked here; status ≠ pass — never entered pending(Σ)). After the bounded attempt each resolves to pass / route / terminal-residual, so "no deferred-pending" (≡ no mismatch still awaiting its bounded re-assessment) always becomes reachable
      residual: Set(Mismatch) }   -- TERMINAL-residual mismatches: stayed ambiguous after their one bounded re-assessment (unattributable). Never entered pending(Σ); adjudicated by terminal_residual(a), surfaced as a non-blocking residual at convergence
Σ = { history: List<(Mismatch, A)>, scan_count: Nat }
                 -- each Mismatch in history carries its kind_binding + certificate (object_ref = Mismatch)
-- Certificate invariant: ∀ m ∈ pending(Σ) : m.certificate.status = pass (fail-closed — routed/ambiguous mismatches never enter pending(Σ))

── COMPOSITION ──
*: product — (D₁ × D₂) → (R₁ × R₂). graph.json edges preserved. Mismatch-domain resolution emergent via session context.
certificate-before-registration ∘ transformative-revalidation: the fail-closed certificate order composes with the NON-MONOTONE loop — when a Confirm/Adapt answer mutates R and Eval(R', X) breeds emergent mismatches Mₑ, EACH Mₑ is independently bind_kind'd + certified at re-scan registration (Phase 2) before it can enter pending(Σ). So only in-scope (ApplicationDecontextualized-owned) Mₑ_passed register, even as R mutates across cycles; the certificate gate holds under mutation-induced revalidation. Dual to elicit's "Monotonicity ∘ shared-backbone": elicit composes the order with an IMMUTABLE substrate, contextualize with a MUTATING R — both preserve certificate-before-commit.

decontextualized(R, X) ≡ correct(R) ∧ ∃ aspect(a, R, X) : ¬warranted(a, R, X)

TaskCreate({
  subject: "[Mismatch:aspect] description",
  description: "Evidence and context for this mismatch (severity: X)",
  activeForm: "Surfacing [aspect] mismatch"
})

How would you like to handle this applicability mismatch?

Options:
1. **Confirm** — yes, this needs adaptation: [brief direction prompt]
2. **Dismiss** — acceptable as-is: [stated assumption about context fit]

3. **[Specific adaptation]** — [what would change and why]