{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp04_retrieval_first_paired20_20260802","cell_id":"computability_boundary_mapping__public_administration_policy","arm":"PROPOSAL_FIRST","candidate_id":"cbm_pap_policy_rule_preflight_001","hypothesis_id":null,"version":0,"title":"Guarantee-Typed Preflight for Executable Public-Benefit Rules","problem":"A public-benefit agency is considering a pre-deployment checker promised to determine, for every executable policy-rule package and every possible applicant record or interagency response sequence, whether processing will terminate and comply with specified procedural invariants. The rule language permits branching, reusable calculations, repeated requests, external-service calls, and potentially unbounded case histories, but the claimed input class, computation model, external capabilities, and meaning of compliance are not fixed. Failed searches and timeouts are consequently liable to be reported as violations or impossibility, while passing tests may be presented as universal assurance.","actors":["benefit applicants","eligibility caseworkers","agency policy authors","agency rule-engine engineers","program administrators","agency general counsel","oversight and appeals personnel","external data-service operators"],"observable_state":"The proposed checker exposes only PASS or FAIL; its documentation refers to arbitrary policy packages, while implementations impose undocumented depth or time limits. A timeout, unavailable external response, genuine counterexample, malformed package, and unresolved analysis can reach the same output. Test-suite success is used to support claims about all applicant records and future case histories.","consequence":"Administrators may deploy a rule package under an assurance that does not cover its actual behavior, reject a valid package because search did not finish, or keep investing in an unsupported universal checker. Applicants can face delayed, inconsistent, or procedurally defective determinations, while caseworkers and reviewers cannot reconstruct what guarantee a reported result carried.","affected_objective":"Make pre-deployment assurance for executable benefit rules accurate, terminating where promised, operationally usable, and traceable without converting unknown results into eligibility or compliance judgments.","intervention":"Before procuring or deploying a universal checker, create a model-relative computability boundary for the rule language. Specify the encoded policy-package class, admissible case histories, external-service model, property being checked, quantifiers, and required termination guarantee. Seek a constructive total procedure or a scope-matched impossibility argument and have either independently checked. Enforce a decidable syntactic fragment for automatic certification; within that fragment use finite over-approximating models and bounded exhaustive trace checks with explicitly limited claims. Route unrestricted, external-dependent, or resource-exhausted cases to distinct OUT_OF_SCOPE, UNKNOWN, or HUMAN_REVIEW states. Publish the selected boundary, guarantees, assumptions, and recheck triggers in a versioned decision record.","structural_mapping":[{"archetype_element":"Assumed universal automation goal","domain_realization":"A checker is expected to issue an exact terminating compliance verdict for every executable benefit-rule package and every possible case history."},{"archetype_element":"Implicit problem class and representation","domain_realization":"Policy text, executable rules, applicant records, event histories, and external responses are treated as one class despite different encodings and bounds."},{"archetype_element":"Unstated computation model or oracle","domain_realization":"External registries, discretionary caseworker judgments, and legal interpretation are invoked without defined availability, latency, refusal, or accountability behavior."},{"archetype_element":"Constructive-versus-impossibility evidence","domain_realization":"A total checker with termination and correctness arguments is sought in parallel with a scope-matched proof that the unrestricted requirement cannot be met; neither timeouts nor test results settle the question."},{"archetype_element":"Decidable restricted region","domain_realization":"A mechanically enforceable rule fragment forbids or bounds recursion, iteration, external waiting, and history length, permitting a declared total analysis."},{"archetype_element":"Weaker honest fallback","domain_realization":"Finite abstraction, bounded trace exploration, and human escalation return guarantee-labelled SAFE_WITHIN_MODEL, COUNTEREXAMPLE, UNKNOWN, or OUT_OF_SCOPE results instead of an unrestricted Boolean verdict."},{"archetype_element":"Version-linked boundary record","domain_realization":"Each rule-language or external-capability change triggers review of the recorded scope, proof, bounds, and public assurance language."}],"mechanism_mapping":[{"mechanism_slug":"language_fragment_restriction","role":"Define an enforceable policy-rule subset for which a terminating checker can be constructed, while rejecting or quarantining unsupported constructs before analysis.","counterfactual_removal":"Without syntactic restriction, the automatic-certification claim can silently extend to expressive or externally dependent packages for which its guarantee has not been established."},{"mechanism_slug":"abstract_interpretation_or_model_checking","role":"Over-approximate applicant states and workflow transitions in a finite model so absence of a modeled procedural violation supports a one-directional safety verdict relative to the formalization, while possible violations remain reviewable alarms.","counterfactual_removal":"Without the finite over-approximation, the proposal lacks a sound automated fallback between unrestricted exact analysis and case-by-case manual review."},{"mechanism_slug":"bounded_domain_exhaustive_search","role":"Enumerate every trace inside declared limits on record fields, transition count, and external-response alternatives, producing complete results only within those limits.","counterfactual_removal":"Without exhaustive bounded checking, finite test examples could be mistaken for coverage of the entire declared bounded region."},{"mechanism_slug":"fallback_mode_router","role":"Dispatch each package to exact fragment checking, abstract or bounded analysis, or human review and attach the applicable guarantee to every output.","counterfactual_removal":"Without routing and labels, weaker analyses can be consumed downstream as if they inherited the universal exact guarantee."},{"mechanism_slug":"computability_boundary_decision_record","role":"Record the chosen class boundary, evidence, shipped guarantees, unknown behavior, and triggers such as new rule constructs or external services.","counterfactual_removal":"Without a versioned record, later language changes can preserve obsolete assurance language and erase why the boundary was drawn."},{"mechanism_slug":"proof_checking","role":"Have an independent reviewer verify the totality or impossibility argument and expose every assumption linking the formal rule model to agency practice.","counterfactual_removal":"Without independent checking, a direction error, hidden premise, or proof of the wrong formal statement can authorize an incorrect boundary."}],"causal_chain":["The agency permits increasingly expressive executable rules and external interactions while requesting one exact, terminating verdict for every package and case history.","Because the input class, computation model, quantifiers, and guarantee are implicit, timeouts and finite test outcomes are interpreted as semantic answers.","A boundary analysis separates restricted decidable packages, bounded analyzable cases, externally relative cases, and unresolved unrestricted cases.","An enforceable fragment supplies the scope for a constructive total checker, while finite abstraction and bounded enumeration provide explicitly weaker evidence outside the strongest tractable region.","A router preserves distinctions among verified safety, witnessed violation, unknown, out-of-scope, timeout, and system failure and prevents automatic eligibility action from weaker results.","A versioned decision record links each verdict to its model, proof, limits, and recheck triggers, allowing administrators and reviewers to audit what was actually established.","Consequently, procurement and deployment decisions can rely on scoped assurances without treating implementation failure as impossibility or bounded success as a universal proof."],"baseline":"The ordinary baseline is conventional requirements review followed by unit tests, selected scenario simulations, fixed execution timeouts, and legal or caseworker review of exceptions. The checker emits a Boolean release recommendation, while undocumented resource limits and informal expert intervention absorb cases that do not finish.","nearest_rivals":["A conventional policy-as-code validation suite with schema checks, unit tests, regression cases, and execution timeouts; it can detect known defects but does not establish class-wide termination or preserve unknown as a distinct semantic state.","A finite-state workflow model checker applied after manually translating a rule package; it can provide strong model-relative assurance but, without an enforceable language boundary and routing contract, does not govern packages omitted or mistranslated from the model.","Mandatory legal and caseworker sign-off for every rule package; it addresses interpretation and accountability but does not itself classify algorithmic guarantees, bound external dependencies, or prevent timeout from being read as a negative verdict."],"remaining_contrastive_claim":"The candidate's remaining contrastive claim is organizational and structural: pre-deployment review should classify each policy package against an enforceable computability boundary and issue a version-linked, guarantee-typed result before any release recommendation. Testing, standalone model checking, or expert sign-off alone does not supply that combined scope classification, fallback routing, and non-collapsing output contract.","authority_safety":{"decision_authority":"The agency program executive and chief information officer may jointly authorize the analysis process; any production guarantee language or rule-language restriction requires concurrence from general counsel and the accountable benefit-program owner. Existing statutory eligibility and appeal authority remains unchanged.","authorized_first_step":"Analyze one frozen, non-production rule package using synthetic records: inventory its constructs and dependencies, draft the formal input and guarantee contracts, identify a candidate decidable fragment, and exercise the proposed output states without influencing a live case.","excluded_actions":["making or recommending an applicant eligibility determination","changing enacted policy, benefit criteria, deadlines, or appeal rights","blocking or delaying benefits based on an UNKNOWN, timeout, or OUT_OF_SCOPE result","claiming legal compliance or unrestricted decidability from a bounded or model-relative check","treating a human reviewer as an infallible or always-available oracle","deploying the checker into production during the first evidence step"],"halt_rollback":"Stop the exercise if synthetic-only isolation fails, the formal model cannot be reconciled with the frozen rule package, an output could enter a live case workflow, or reviewers cannot distinguish UNKNOWN from FAIL. Remove the prototype from operational interfaces, preserve the audit record, and revert to the existing authorized review process; no eligibility or policy record is altered."},"negative_tests":{"strongest_counterevidence":"The frozen production-representative rule language may already have a finite, enforceable state space and a documented total checker with a checked termination and correctness argument covering all declared external behaviors. If so, a new computability-boundary layer adds little beyond ordinary verification and complexity assessment.","problem_falsifier":"The problem is falsified for the scoped agency if no universal or open-ended guarantee is actually claimed, every analyzed package has an effectively enumerable finite input and transition space, and timeout, false, unknown, out-of-scope, and system failure are already separately represented and governed.","intervention_falsifier":"The intervention is falsified if independent review shows that fragment membership cannot be enforced safely, the abstraction omits a feasible real behavior, bounded enumeration does not cover its declared finite encoding, or downstream systems continue treating weaker and unknown outputs as release approval despite the routing contract.","risks":["The formal policy model can omit discretionary, legal, or operational semantics and certify the wrong task.","An unsound abstraction can miss a real procedural violation; an overly coarse sound abstraction can produce unusable false alarms.","A restrictive fragment can exclude necessary exceptions or encode them through opaque workarounds, reducing semantic fidelity.","Human-review routing can create delay, inconsistent judgments, or an unaccountable shadow oracle.","Bounds selected for tractability can be mistaken for substantive limits on real applicant histories.","Guarantee labels can be stripped or ignored by procurement dashboards and downstream release workflows.","A correct decidability result can still be operationally infeasible because of computational cost."]},"next_evidence_step":"On one frozen non-production benefit-rule package, conduct a two-week paper-and-sandbox boundary audit using only synthetic inputs. Produce: a grammar and dependency inventory; one precisely stated universal property; a candidate enforceable fragment; a finite abstraction with documented over-approximation obligations; an exhaustive check over one explicitly enumerated small bound; and sample outputs for SAFE_WITHIN_MODEL, COUNTEREXAMPLE, UNKNOWN, OUT_OF_SCOPE, TIMEOUT, and SYSTEM_FAILURE. Have one policy lawyer and one technically independent reviewer try to find a semantic mismatch or unjustified guarantee. The step succeeds only as evidence of feasibility if every output is traceable to its scope and no synthetic result can affect a live case.","prior_art_status":"UNSEARCHED","revision_record":{"parent_version":null,"progress_targets_addressed":["Initial complete proposal"],"conceptual_changes":["Instantiated computability-boundary mapping in executable public-benefit policy administration."],"operational_changes":["Defined a synthetic, non-production first evidence step with explicit authority and rollback conditions."],"evidence_changes":["No external or prior-art evidence consulted; proposed only a bounded internal feasibility check."],"claim_changes":["Limited all assurance claims to declared fragments, formal models, or finite bounds and made no novelty, prevalence, demand, or effect-size claim."]}}