{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp03_full320_20260801","cell_id":"computability_boundary_mapping__computer_science","trajectory_id":"R","attempt_index":0,"archetype_slug":"computability_boundary_mapping","domain_slug":"computer_science","decision":"CANDIDATE","problem_id":"universal_workflow_termination_gate","causal_lever_id":"model_relative_termination_routing","proposal":{"problem":"A workflow platform requires a preflight gate to answer YES or NO, with guaranteed termination, on whether every submitted arbitrary Turing-complete workflow will halt on its supplied input. Failed analysis or timeout is collapsed into a Boolean verdict. The unrestricted requirement is a halting decision problem, while executable bounds, restricted languages, and weaker one-sided guarantees are left unstated.","actors_substrate":["workflow-platform engineering team","security and reliability reviewers","workflow authors","operators and downstream services","arbitrary workflow programs, inputs, interpreter semantics, and external calls"],"observable_state":"The gate accepts unrestricted programs, sometimes times out, and still emits an authoritative Boolean; passing examples are treated as evidence of universal termination, while its exact input class and computation model are undocumented.","consequence":"Nontermination can be misclassified, terminating workflows can be rejected, implementation effort can chase an impossible total-exact gate, and downstream systems cannot distinguish NO from UNKNOWN or analyzer failure.","affected_objective":"Provide trustworthy preflight admission while preserving platform availability, useful workflow coverage, and truthful guarantees.","structural_mapping":[{"archetype_element":"implicit universal problem class","domain_realization":"All submitted workflows and supplied inputs are treated as one unrestricted class.","claim_kind":"HYPOTHESIS"},{"archetype_element":"total exact terminating answer","domain_realization":"The admission interface requires an unconditional Boolean termination verdict.","claim_kind":"HYPOTHESIS"},{"archetype_element":"model-relative impossibility boundary","domain_realization":"A computable translation from a machine-and-input halting instance to an equivalent workflow would refute a total decider for the unrestricted interpreter.","claim_kind":"INFERENCE"},{"archetype_element":"decidable restricted region","domain_realization":"A mechanically enforced structurally terminating DSL or an execution model with finite fuel admits a total decision procedure within its stated boundary.","claim_kind":"INFERENCE"},{"archetype_element":"one-sided fallback","domain_realization":"Sound termination proofs may yield YES; exhausted analysis yields UNKNOWN rather than NO.","claim_kind":"INFERENCE"},{"archetype_element":"governed weaker operation","domain_realization":"A router labels exact-fragment, sound-analysis, bounded-execution, and escalation results with distinct guarantees.","claim_kind":"HYPOTHESIS"},{"archetype_element":"reclassification trigger","domain_realization":"Interpreter, DSL, external-call, abstraction, or fuel-policy changes reopen the boundary decision.","claim_kind":"INFERENCE"}],"component_map":[{"component":"Problem-Class Specification","status":"direct","domain_realization":"Define instances as encoded workflow-and-input pairs under a named interpreter."},{"component":"Instance Representation Contract","status":"direct","domain_realization":"Version workflow syntax, input encoding, numeric domains, and external-call representation."},{"component":"Computation Model Contract","status":"direct","domain_realization":"State interpreter semantics, nondeterminism, resources, and any oracle-like services."},{"component":"Solvability Guarantee Profile","status":"direct","domain_realization":"Separate total exact, sound incomplete, bounded, and operational guarantees."},{"component":"Quantifier and Scope Map","status":"direct","domain_realization":"Distinguish each submitted pair from claims covering every valid pair."},{"component":"Computability Status Lattice","status":"adapted","domain_realization":"Classify lanes as decidable, recognizable, bounded, relative, or unresolved."},{"component":"Constructive Procedure Witness","status":"direct","domain_realization":"Require an algorithm plus correctness and termination proof for each exact lane."},{"component":"Reduction Preservation Contract","status":"direct","domain_realization":"Document the total computable halting-instance-to-workflow map and preserved answer."},{"component":"Computability Impossibility Certificate","status":"direct","domain_realization":"Retain the checked halting reduction for the unrestricted lane."},{"component":"Assumption Register","status":"direct","domain_realization":"Record interpreter, encoding, external-service, and fragment assumptions."},{"component":"Decidable Subclass Map","status":"direct","domain_realization":"List enforceable terminating DSL fragments and finite-fuel configurations."},{"component":"One-Sided Recognition Contract","status":"adapted","domain_realization":"A proof-bearing YES is sound; lack of proof provides no NO verdict."},{"component":"Unknown and Nontermination Policy","status":"direct","domain_realization":"Keep UNKNOWN, analysis timeout, out-of-scope, and observed runtime nontermination distinct."},{"component":"Fallback Solution Contract","status":"direct","domain_realization":"Specify guarantee labels and permitted uses for each routed lane."},{"component":"Computability Guarantee Record","status":"direct","domain_realization":"Version-link evidence, model, scope, and public interface language."},{"component":"Recheck Trigger","status":"direct","domain_realization":"Reassess after semantic, language, abstraction, oracle, or bound changes."},{"component":"Termination Condition","status":"adapted","domain_realization":"Bound the analyzer; return UNKNOWN when its budget is exhausted."},{"component":"Scope Boundary","status":"direct","domain_realization":"Mechanically reject or quarantine inputs outside an exact fragment."},{"component":"Decision Record","status":"direct","domain_realization":"Record which modes ship, why, and their supersession conditions."},{"component":"Uncertainty Residue","status":"direct","domain_realization":"Retain unproved obligations and abstraction imprecision as explicit residue."},{"component":"Independent Proof Review","status":"direct","domain_realization":"Independently check the reduction and exact-lane proofs against their formal statements."},{"component":"Complexity Follow-On Gate","status":"direct","domain_realization":"Assess scalability only after a lane is shown decidable."}],"mechanism_dispositions":[{"slug":"abstract_interpretation_or_model_checking","disposition":"selected_supporting","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Use a sound finite over-approximation to prove termination-related obligations for some workflows; imprecision produces UNKNOWN.","counterfactual_removal":"The unrestricted lane would lose a sound automated fallback beyond the exact fragment."},{"slug":"bounded_domain_exhaustive_search","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Exhaustively check tiny finite workflow, input, and fuel spaces to test routing and label invariants.","counterfactual_removal":"The first test would lose complete bounded coverage but the boundary argument would remain."},{"slug":"computability_boundary_decision_record","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Version the chosen boundary, evidence, shipped labels, and recheck triggers.","counterfactual_removal":"Guarantees could drift silently after interpreter or policy changes."},{"slug":"computational_complexity_analysis","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Evaluate cost only for exact restricted procedures already proved total.","counterfactual_removal":"Decidable but unusably expensive lanes could be shipped without feasibility review."},{"slug":"constructive_algorithm_and_correctness_proof","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Supply the decider and totality proof for each exact restricted lane.","counterfactual_removal":"The exact-lane guarantee would rest on examples rather than a class-wide witness."},{"slug":"diagonalization_impossibility_proof","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"A direct diagonal proof is valid in principle but redundant when a concrete halting reduction better matches the interpreter.","counterfactual_removal":"No material change; the selected reduction supplies the impossibility certificate."},{"slug":"enumeration_and_dovetailing","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Fair enumeration is unnecessary for checking one workflow-input execution; the bounded one-sided protocol is simpler.","counterfactual_removal":"No material change."},{"slug":"fallback_mode_router","disposition":"selected_load_bearing","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Route queries to exact-fragment, sound-analysis, bounded-execution, or escalation modes and attach guarantee labels.","counterfactual_removal":"Weaker results could again be presented as universal Boolean decisions."},{"slug":"halting_problem_reduction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Construct a workflow that halts exactly when an encoded source machine halts on its input.","counterfactual_removal":"The claim that the unrestricted Boolean gate is impossible would lack decisive evidence."},{"slug":"language_fragment_restriction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Provide a syntactically enforceable structurally terminating workflow fragment.","counterfactual_removal":"The platform would lack a useful region with a genuine total-exact guarantee."},{"slug":"many_one_reduction_proof","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Its obligations are incorporated into the selected halting reduction rather than maintained as a separate mechanism.","counterfactual_removal":"No material change if the reduction preservation contract remains checked."},{"slug":"promise_problem_restriction","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"An unenforced promise permits authoritative behavior outside accountability; enforceable syntax and fuel are safer.","counterfactual_removal":"No material change."},{"slug":"proof_by_counterexample","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Use legitimate workflows to refute over-broad implementation claims, without treating missing counterexamples as proof.","counterfactual_removal":"Pilot testing would be less able to expose scope or label overreach."},{"slug":"proof_checking","disposition":"selected_load_bearing","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Independently verify the reduction and restricted-lane proofs against the declared semantics.","counterfactual_removal":"A formalization or proof gap could authorize an unsound boundary."},{"slug":"reduction_direction_checklist","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Gate the impossibility verdict on source-to-target direction, totality, computability, and preservation.","counterfactual_removal":"A reversed or partial reduction could be mistaken for proof."},{"slug":"semi_decision_with_explicit_unknown","disposition":"selected_load_bearing","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Bound sound proof search and return YES with evidence or UNKNOWN, never fabricated NO.","counterfactual_removal":"Analyzer timeout would remain liable to collapse into a false negative verdict."},{"slug":"theorem_prover_guided_search","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Automated proof discovery is optional; constructive procedures and independent checking suffice for the first intervention.","counterfactual_removal":"No hard-gate change; proof discovery may be slower."},{"slug":"turing_reduction_analysis","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Relative oracle degrees are unnecessary and too permissive for the required direct impossibility transfer.","counterfactual_removal":"No material change."}],"causal_chain":["Specify the unrestricted workflow-input class and interpreter model.","Check a source-to-target halting reduction, establishing that no total exact gate covers that class.","Mechanically identify terminating fragments and finite-fuel configurations with constructive deciders.","Route remaining workflows to sound incomplete analysis or bounded execution.","Preserve UNKNOWN, out-of-scope, timeout, and observed nontermination as distinct states.","Version the guarantee and recheck it when model assumptions change."],"baseline":"Continue using an unrestricted preflight analyzer with timeouts, test-suite evidence, manual exceptions, and a Boolean admission interface.","nearest_rival":"Retain the universal specification but increase analyzer resources and heuristic sophistication; this may improve coverage without resolving the total-exact requirement.","authority_safety":{"affected_parties":["workflow authors","platform operators","downstream service owners","users affected by rejected or nonterminating workflows"],"decision_authority":"The platform owner may authorize only a sandboxed pilot; production guarantee changes require engineering, reliability, and security sign-off after independent proof review.","authorized_first_step":"On a non-production interpreter snapshot, formalize one workflow subset, check the halting reduction, implement an exact terminating fragment plus YES/UNKNOWN fallback, and exhaustively test all tiny programs within fixed syntax, input, step, and state bounds.","excluded_actions":["Relabel UNKNOWN or timeout as NO","Claim results beyond an enforced fragment or bound","Admit unrestricted workflows based solely on the pilot","Treat proof-checking success as validation of real-world semantic fidelity"],"halt_rollback":"Stop the pilot and restore the prior non-production gate if any exact-lane counterexample appears, the abstraction drops a concrete behavior, routing mislabels a guarantee, or scope enforcement is bypassable."}},"negative_tests":{"strongest_counterevidence":"The apparent unrestricted gate may already operate over an enforced finite-fuel semantics or a structurally terminating language, in which case a total algorithm can exist and the issue is complexity or documentation rather than computability.","analogy_break":"Real workflows may depend on nondeterministic schedulers, humans, sensors, or external services; a pure-program halting reduction governs only the declared computation model and may not faithfully represent operational completion.","failure_condition":"The intervention fails if fragment membership cannot be enforced, useful workload coverage collapses, the abstraction is unsound, or downstream consumers still interpret UNKNOWN as a Boolean verdict.","problem_falsifier":"An audit shows that all admitted workflows are mechanically bounded or restricted, the exact decision procedure is proved total and correct for that enforced class, and timeout, UNKNOWN, and NO are already distinct.","intervention_falsifier":"Within the bounded pilot, a well-formed counterexample violates an advertised exact guarantee, a concrete behavior is absent from the abstraction, or routing produces a stronger label than its evidence supports.","risks":["A checked proof may formalize the wrong interpreter semantics.","A decidable fragment may be computationally impractical.","Authors may escape to unrestricted extensions, eroding coverage and guarantees.","Frequent UNKNOWN results may encourage unsafe manual overrides.","External services may act as undeclared oracles with changing behavior."]},"null_rationale":null,"classification":{"candidate_kind":"MECHANISM_COMPOSITION","prior_art_status":"UNSEARCHED","evidence_maturity":"HYPOTHESIS"},"revision_change_log":{"revision_kind":"ORIGINAL","prior_problem_id":null,"prior_causal_lever_id":null,"problem_changed":false,"causal_lever_changed":false,"conceptual_changes":[],"operational_changes":[],"repairs_addressed":[]},"confidence":0.92,"generator_notes":"Closed-book structural inference from the supplied packet. The candidate targets a recognizable universal termination-gate problem; empirical prevalence, workload coverage, and pilot effects remain hypotheses."}