{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp03_full320_20260801","cell_id":"computability_boundary_mapping__behavioral_economics","trajectory_id":"R","attempt_index":0,"archetype_slug":"computability_boundary_mapping","domain_slug":"behavioral_economics","decision":"CANDIDATE","problem_id":"universal_adaptive_choice_outcome_prediction","causal_lever_id":"enforce_decidable_behavioral_model_scope","proposal":{"problem":"Behavioral-policy teams may demand an automated system that, for every finitely described adaptive choice architecture, behavioral model, and initial state, returns a correct, terminating verdict on whether a target behavior or welfare threshold will eventually occur. If the modeling language can encode unbounded state and arbitrary computation, implementation failures, simulations, or timeouts cannot settle that universal requirement; yet unrestricted outputs may still be presented as definitive policy predictions.","actors_substrate":["behavioral-policy designers","behavioral economists and modelers","decision-system vendors","reviewers and regulators","people subject to modeled interventions"],"observable_state":"A universal yes/no outcome predictor is specified or marketed, while its model language, quantifiers, termination guarantee, and treatment of timeout or out-of-scope cases remain implicit.","consequence":"An impossible or unsupported universal predictor can consume resources, convert unknowns into false conclusions, and authorize behavioral interventions under overstated guarantees.","affected_objective":"Provide useful behavioral-policy analysis without misrepresenting formal model reachability as universally decidable or model predictions as guaranteed human outcomes.","structural_mapping":[{"archetype_element":"Unrestricted problem class","domain_realization":"All encoded adaptive choice architectures and behavioral transition models, including unbounded histories and state.","claim_kind":"HYPOTHESIS"},{"archetype_element":"Total exact decider","domain_realization":"A predictor required to halt and correctly decide eventual target attainment for every valid encoding.","claim_kind":"INFERENCE"},{"archetype_element":"Computational embedding","domain_realization":"An expressive behavioral-rule language may simulate an arbitrary machine, making target attainment encode machine halting.","claim_kind":"HYPOTHESIS"},{"archetype_element":"Decidable region","domain_realization":"Mechanically enforced finite-state, bounded-horizon, or otherwise proven-total behavioral-model fragments.","claim_kind":"INFERENCE"},{"archetype_element":"Honest fallback","domain_realization":"Exact bounded results, sound model-relative results, or UNKNOWN, each labeled without claims about real people beyond the model.","claim_kind":"INFERENCE"},{"archetype_element":"Reclassification trigger","domain_realization":"Changes to behavioral-rule expressiveness, horizon, state, outcome semantics, or external information reopen the boundary decision.","claim_kind":"INFERENCE"}],"component_map":[{"component":"Problem-Class Specification","status":"adapted","domain_realization":"Encoded adaptive behavioral models and eventual-outcome queries."},{"component":"Instance Representation Contract","status":"adapted","domain_realization":"Grammar for model, initial state, intervention, target, and horizon."},{"component":"Computation Model Contract","status":"direct","domain_realization":"Effective procedures over those encodings; external experts are declared inputs."},{"component":"Solvability Guarantee Profile","status":"direct","domain_realization":"Exact-total, model-sound, bounded, or UNKNOWN."},{"component":"Quantifier and Scope Map","status":"direct","domain_realization":"Separate every-model guarantees from individual simulations."},{"component":"Computability Status Lattice","status":"direct","domain_realization":"Classify fragments as decidable, recognizable, partial, undecidable, or unresolved."},{"component":"Constructive Procedure Witness","status":"direct","domain_realization":"Algorithm plus correctness and termination proof for any claimed decidable fragment."},{"component":"Reduction Preservation Contract","status":"direct","domain_realization":"Computable source-to-behavioral-model map preserving halting and target attainment."},{"component":"Computability Impossibility Certificate","status":"direct","domain_realization":"Checked reduction for the unrestricted encoded-model class."},{"component":"Assumption Register","status":"direct","domain_realization":"Expressiveness, encoding, semantics, and model-human correspondence assumptions."},{"component":"Decidable Subclass Map","status":"adapted","domain_realization":"Enforceable finite-state and bounded-horizon fragments."},{"component":"One-Sided Recognition Contract","status":"adapted","domain_realization":"Witnessed attainment may return YES; failure to find it is not NO."},{"component":"Unknown and Nontermination Policy","status":"direct","domain_realization":"Keep UNKNOWN, timeout, out-of-scope, and NO distinct."},{"component":"Fallback Solution Contract","status":"direct","domain_realization":"Route to exact fragment analysis, bounded search, or abstention."},{"component":"Computability Guarantee Record","status":"direct","domain_realization":"Versioned statement of model-relative guarantees."},{"component":"Recheck Trigger","status":"direct","domain_realization":"Any language, horizon, semantics, or oracle change."},{"component":"Termination Condition","status":"direct","domain_realization":"Finite state, explicit horizon, or declared resource bound."},{"component":"Scope Boundary","status":"direct","domain_realization":"No extrapolation from formal models to guaranteed human behavior."},{"component":"Decision Record","status":"direct","domain_realization":"Record shipped modes, evidence, exclusions, and owners."},{"component":"Uncertainty Residue","status":"adapted","domain_realization":"Open proof obligations and empirical model error."},{"component":"Independent Proof Review","status":"direct","domain_realization":"Independent checking of reduction and fragment proofs."},{"component":"Complexity Follow-On Gate","status":"direct","domain_realization":"Assess cost only after a fragment is shown decidable."}],"mechanism_dispositions":[{"slug":"abstract_interpretation_or_model_checking","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"A sound abstraction of a formal model need not soundly over-approximate human behavior.","counterfactual_removal":"No change to the proposed boundary test."},{"slug":"bounded_domain_exhaustive_search","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Exhaust finite states and horizons with strictly bounded claims.","counterfactual_removal":"The fallback loses a terminating exact mode."},{"slug":"computability_boundary_decision_record","disposition":"selected_supporting","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Version the boundary, guarantee, assumptions, and triggers.","counterfactual_removal":"Guarantees can drift silently."},{"slug":"computational_complexity_analysis","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Gate feasibility analysis after decidability.","counterfactual_removal":"Decidable fragments may be mistaken for practical ones."},{"slug":"constructive_algorithm_and_correctness_proof","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Required for total-exact claims on restricted fragments.","counterfactual_removal":"Positive decidability claims lack a witness."},{"slug":"diagonalization_impossibility_proof","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Redundant if the domain-specific halting reduction succeeds.","counterfactual_removal":"No change."},{"slug":"enumeration_and_dovetailing","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Unbounded nontermination is unsuitable for policy operations.","counterfactual_removal":"No change."},{"slug":"fallback_mode_router","disposition":"selected_load_bearing","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Route by enforced scope and label each guarantee.","counterfactual_removal":"Weaker results can be mistaken for universal verdicts."},{"slug":"halting_problem_reduction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Test whether eventual behavioral-state attainment can preserve halting.","counterfactual_removal":"The proposed impossibility boundary lacks decisive evidence."},{"slug":"language_fragment_restriction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Enforce a decidable behavioral-rule grammar.","counterfactual_removal":"There is no mechanically policed exact-answer region."},{"slug":"many_one_reduction_proof","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Discharge totality, computability, and answer preservation of the halting embedding.","counterfactual_removal":"Reduction validity becomes ambiguous."},{"slug":"promise_problem_restriction","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Unenforced behavioral promises allow authoritative answers on violated inputs.","counterfactual_removal":"No change."},{"slug":"proof_by_counterexample","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Use in-scope failures to refute overbroad predictor claims, not prove impossibility.","counterfactual_removal":"Cheap falsification of universal claims is lost."},{"slug":"proof_checking","disposition":"selected_load_bearing","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Independently check the reduction and constructive proofs.","counterfactual_removal":"A subtle proof gap could authorize a false boundary."},{"slug":"reduction_direction_checklist","disposition":"selected_supporting","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Require known-undecidable source to target direction and registered assumptions.","counterfactual_removal":"A reversed reduction may be accepted."},{"slug":"semi_decision_with_explicit_unknown","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Bound witness search and return UNKNOWN rather than NO.","counterfactual_removal":"Timeouts may become false negatives."},{"slug":"theorem_prover_guided_search","disposition":"unused","contribution_type":"NONE","adaptation_or_rejection":"Optional tooling; not required for the bounded first test.","counterfactual_removal":"No causal change."},{"slug":"turing_reduction_analysis","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Relative degrees add no needed operational distinction here.","counterfactual_removal":"No change."}],"causal_chain":["An unrestricted behavioral-model language admits unbounded adaptive rules.","A universal eventual-outcome predictor must decide every encoded model and terminate.","If halting instances map computably to target-attainment instances, that predictor would decide halting.","A checked reduction therefore rejects the unrestricted total-exact requirement.","Enforced decidable fragments and bounded modes recover narrower guarantees.","Routing and explicit UNKNOWN prevent narrower model results from becoming universal policy claims."],"baseline":"Run simulations or heuristics on selected cases, stop at resource limits, and report binary predictions without a proved class boundary.","nearest_rival":"Treat the issue solely as bounded rationality or predictive-model calibration, improving data and heuristics without testing whether the formal universal decision requirement is computable.","authority_safety":{"affected_parties":["people exposed to behavioral interventions","policy clients","modelers and operators"],"decision_authority":"A joint behavioral-methods and formal-verification review owner may approve only model-analysis modes; accountable policy authorities retain intervention decisions.","authorized_first_step":"In a synthetic sandbox, formalize one adaptive behavioral language, attempt an independently checked halting reduction, define a finite-state restricted dialect, and compare exact, bounded, and UNKNOWN outputs on a small disclosed corpus.","excluded_actions":["No live behavioral intervention","No individual eligibility, benefit, enforcement, or clinical decision","No claim that formal-model correctness guarantees human behavior","No conversion of timeout or UNKNOWN into NO"],"halt_rollback":"Stop if the reduction, fragment-membership check, model semantics, or output labels fail review; withdraw universal language and revert to explicitly exploratory simulation."}},"negative_tests":{"strongest_counterevidence":"The practical requirement may only be probabilistic prediction on a finite population and horizon; empirical misspecification and stochastic behavior may dominate, making computability analysis irrelevant.","analogy_break":"A formal behavioral model is an encoding, not a person: proving model reachability decidable or undecidable neither establishes psychological truth nor welfare effects.","failure_condition":"The transfer fails if the behavioral language cannot encode the required computation, target attainment does not preserve halting, or the real requirement is bounded rather than universal.","problem_falsifier":"Show that the actual requirement covers a finite enforceable input set or asks only for calibrated probabilistic estimates, with no exact class-wide termination claim.","intervention_falsifier":"Show either a checked total correct procedure for the declared unrestricted class, or that the proposed restriction/router cannot enforce membership, terminate, preserve its stated guarantee, or produce useful coverage.","risks":["Formalism may distract from empirical validity and distributional welfare.","A restrictive fragment may exclude behaviorally important dynamics.","UNKNOWN may be suppressed by downstream incentives.","A correct model-level result may be marketed as a prediction about people.","Complexity may make a decidable fallback unusable."]},"null_rationale":null,"classification":{"candidate_kind":"DOMAIN_TRANSFER","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.78,"generator_notes":"Closed-book structural transfer; the central domain-specific undecidability premise requires proof in the declared behavioral-model language."}