{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp03_full320_20260801","cell_id":"computability_boundary_mapping__neuroscience","trajectory_id":"R","attempt_index":0,"archetype_slug":"computability_boundary_mapping","domain_slug":"neuroscience","decision":"CANDIDATE","problem_id":"universal_neural_model_reachability_claim","causal_lever_id":"model_relative_reachability_boundary","proposal":{"problem":"A computational-neuroscience project promises an exact, always-terminating classifier that determines whether any executable neural-circuit model will ever reach a specified activity regime, while leaving model language, horizon, quantifiers, and admissible external inputs implicit. For sufficiently expressive unrestricted model languages, that universal reachability claim may be undecidable; for finite models or bounded horizons it may instead be decidable but costly (HYPOTHESIS).","actors_substrate":["computational neuroscientists specifying circuit models and target regimes","software engineers implementing simulators and analyzers","reviewers and institutions accepting model-based claims","experimental collaborators and downstream users interpreting verdicts","executable neural models, input streams, and compute infrastructure"],"observable_state":"Timeouts or failed simulations are reported as evidence that a regime is unreachable; bounded successes are generalized to arbitrary models; and analyzer outputs lack distinct false, unknown, timeout, and out-of-scope states.","consequence":"Resources are spent pursuing an impossible universal analyzer, or weaker evidence is presented as a definitive neuroscientific reachability result.","affected_objective":"Produce auditable claims about whether modeled neural dynamics can reach specified regimes without confusing undecidability, computational expense, simulation failure, and empirical validity.","structural_mapping":[{"archetype_element":"unrestricted class-wide exact terminating requirement","domain_realization":"Classify reachability for every model expressible in the declared neural-model language and every admissible input history.","claim_kind":"INFERENCE"},{"archetype_element":"explicit representation and computation model","domain_realization":"Fix model syntax and semantics, numeric representation, stochasticity, external-input access, target predicate, horizon, and machine capabilities.","claim_kind":"INFERENCE"},{"archetype_element":"constructive-versus-impossibility evidence","domain_realization":"Seek a total reachability algorithm for restricted classes and a valid reduction for the unrestricted executable class.","claim_kind":"HYPOTHESIS"},{"archetype_element":"decidable regions and honest fallback","domain_realization":"Route finite-state or bounded-horizon models to complete checking and other admissible models to sound abstraction, bounded witness search, or UNKNOWN.","claim_kind":"HYPOTHESIS"},{"archetype_element":"versioned reclassification","domain_realization":"Reassess guarantees when the modeling language, target predicate, bounds, numerical semantics, or external capabilities change.","claim_kind":"INFERENCE"}],"component_map":[{"component":"Problem-Class Specification","status":"direct","domain_realization":"Models and target-regime reachability questions covered."},{"component":"Instance Representation Contract","status":"direct","domain_realization":"Encoding of dynamics, parameters, inputs, initial states, and targets."},{"component":"Computation Model Contract","status":"direct","domain_realization":"Permitted arithmetic, randomness, interaction, precision, and oracle access."},{"component":"Solvability Guarantee Profile","status":"direct","domain_realization":"Exact decision, one-sided recognition, bounded completeness, or sound approximation."},{"component":"Quantifier and Scope Map","status":"direct","domain_realization":"Separate every-model claims from claims about named models, horizons, and inputs."},{"component":"Computability Status Lattice","status":"direct","domain_realization":"Record decidable, recognizable, relative, unresolved, or undecidable status."},{"component":"Constructive Procedure Witness","status":"direct","domain_realization":"Algorithm with correctness and termination argument for a restricted class."},{"component":"Reduction Preservation Contract","status":"adapted","domain_realization":"Computable embedding must preserve halting and target-regime reachability."},{"component":"Computability Impossibility Certificate","status":"adapted","domain_realization":"Checked reduction for the unrestricted neural-model language."},{"component":"Assumption Register","status":"direct","domain_realization":"Expressiveness, semantics, precision, horizon, and input assumptions."},{"component":"Decidable Subclass Map","status":"direct","domain_realization":"Finite-state, bounded-horizon, or enforceable restricted-language regions."},{"component":"One-Sided Recognition Contract","status":"direct","domain_realization":"A witnessed trajectory may establish reachability without establishing non-reachability."},{"component":"Unknown and Nontermination Policy","status":"direct","domain_realization":"Keep UNKNOWN, timeout, out-of-scope, and false distinct."},{"component":"Fallback Solution Contract","status":"direct","domain_realization":"Label abstraction, bounded search, and escalation guarantees."},{"component":"Computability Guarantee Record","status":"direct","domain_realization":"Version-linked statement of shipped analyzer guarantees."},{"component":"Recheck Trigger","status":"direct","domain_realization":"Language, semantic, horizon, target, or capability change."},{"component":"Termination Condition","status":"direct","domain_realization":"Finite state space or declared time, depth, and resource bounds."},{"component":"Scope Boundary","status":"direct","domain_realization":"Mechanically enforce accepted fragments and promises."},{"component":"Decision Record","status":"direct","domain_realization":"Record selected analyzer mode and rationale."},{"component":"Uncertainty Residue","status":"direct","domain_realization":"Unproved obligations and unresolved model classes."},{"component":"Independent Proof Review","status":"direct","domain_realization":"Independent check of reductions and constructive proofs."},{"component":"Complexity Follow-On Gate","status":"direct","domain_realization":"Assess feasibility only after decidability is established."}],"mechanism_dispositions":[{"slug":"abstract_interpretation_or_model_checking","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Sound finite abstraction for conservative regime-safety claims.","counterfactual_removal":"Fallback loses a sound approximate mode but boundary classification remains."},{"slug":"bounded_domain_exhaustive_search","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Complete checking for explicitly finite model, state, and horizon bounds.","counterfactual_removal":"Pilot cannot demonstrate bounded completeness."},{"slug":"computability_boundary_decision_record","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Version the boundary, guarantee, assumptions, and triggers.","counterfactual_removal":"Guarantees can drift without traceability."},{"slug":"computational_complexity_analysis","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Gate practical feasibility after solvability classification.","counterfactual_removal":"Decidable may be mistaken for deployable."},{"slug":"constructive_algorithm_and_correctness_proof","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Establish decidability of each claimed restricted class.","counterfactual_removal":"Positive boundary placements lack total-procedure evidence."},{"slug":"diagonalization_impossibility_proof","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Redundant unless a direct self-reference proof is simpler than reduction.","counterfactual_removal":"No change; reduction supplies the planned certificate."},{"slug":"enumeration_and_dovetailing","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Unbounded operation conflicts with the bounded first test.","counterfactual_removal":"No material change."},{"slug":"fallback_mode_router","disposition":"selected_load_bearing","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Dispatch by enforceable class and label each guarantee.","counterfactual_removal":"Weaker modes can be misread as universal decisions."},{"slug":"halting_problem_reduction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Test whether executable neural models can encode halting as target-state reachability.","counterfactual_removal":"The unrestricted impossibility claim lacks decisive evidence."},{"slug":"language_fragment_restriction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Enforce a neural-model syntax with a total reachability procedure.","counterfactual_removal":"No mechanically policed decidable service class remains."},{"slug":"many_one_reduction_proof","disposition":"selected_supporting","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Formalize total computable answer-preserving reduction obligations.","counterfactual_removal":"The halting reduction loses its preservation contract."},{"slug":"promise_problem_restriction","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Unchecked promises permit authoritative answers on violating inputs; syntactic restriction is safer.","counterfactual_removal":"No change to selected boundary."},{"slug":"proof_by_counterexample","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Refute overbroad analyzer claims using one in-scope failure.","counterfactual_removal":"Pilot loses a cheap universal-claim challenge."},{"slug":"proof_checking","disposition":"selected_load_bearing","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Independently verify the exact formal theorem and assumptions.","counterfactual_removal":"A flawed reduction could wrongly terminate research."},{"slug":"reduction_direction_checklist","disposition":"selected_supporting","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Require known-undecidable source to map into neural reachability.","counterfactual_removal":"Direction errors become easier to authorize."},{"slug":"semi_decision_with_explicit_unknown","disposition":"selected_load_bearing","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Return witnessed YES or bounded UNKNOWN, never timeout-as-NO.","counterfactual_removal":"The fallback can fabricate non-reachability."},{"slug":"theorem_prover_guided_search","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Optional proof-production tool; unnecessary for the bounded classification pilot.","counterfactual_removal":"No causal change if proofs receive independent review."},{"slug":"turing_reduction_analysis","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Relative degrees add no needed decision beyond the planned many-one reduction.","counterfactual_removal":"No change to the proposed guarantee."}],"causal_chain":["Make the neural reachability class, encoding, quantifiers, and machine model explicit.","Attempt constructive totality for enforceable restricted classes and a checked halting reduction for the unrestricted class.","Classify each region without treating timeout as evidence.","Route inputs to exact, bounded, sound-approximate, or explicit-UNKNOWN modes.","Publish only the guarantee justified for that route and recheck it after assumption changes."],"baseline":"Ordinary simulation or heuristic search over selected models, with a timeout and an informal yes/no interpretation.","nearest_rival":"Improve simulation, theorem-proving, or compute capacity while retaining the unrestricted exact-and-terminating claim.","authority_safety":{"affected_parties":["model authors","experimental collaborators","reviewers","downstream scientific or clinical interpreters"],"decision_authority":"The model-governance owner may authorize interface and claim changes; an independent methods reviewer must approve impossibility or totality claims.","authorized_first_step":"On a toy executable neural-model language, specify reachability formally; test a halting-to-reachability embedding and a finite restricted fragment; independently check both arguments; run bounded cases; expose YES, NO only where proved, UNKNOWN, timeout, and out-of-scope.","excluded_actions":["Declare real brains or neuroscience questions undecidable from a result about a formal model language.","Treat timeout or failed proof search as non-reachability.","Deploy clinical or experimental decisions from the pilot.","Generalize bounded results beyond their stated bounds."],"halt_rollback":"Halt any impossibility label if the reduction, formalization, or independent review fails; restore UNRESOLVED. Stop the pilot on output-label confusion or any downstream use beyond authorization; retain the prior simulator and decision record."}},"negative_tests":{"strongest_counterevidence":"The actual accepted model language may be finite-state with a fixed horizon and effectively enumerable, or may already have a proved total reachability procedure; then the issue is complexity rather than computability.","analogy_break":"A formal executable neural model is not a biological nervous system. Undecidability of reachability in an expressive model language neither proves that biological prediction is undecidable nor validates the model's empirical semantics.","failure_condition":"The mapping fails if the project concerns only finitely many bounded models, makes no reusable universal guarantee, or cannot define a stable reachability predicate.","problem_falsifier":"Audit shows every documented claim is explicitly bounded to an enforceable finite class, distinguishes UNKNOWN from NO, and makes no unrestricted exact terminating promise.","intervention_falsifier":"After formalization and independent review, neither a valid impossibility proof for the unrestricted class nor a total procedure for any useful restricted class can be established, and routing does not reduce false certainty or wasted universal-search effort in the pilot.","risks":["An incorrect formalization can yield a valid proof about the wrong neuroscientific question.","Restrictions may exclude scientifically important dynamics.","Sound abstractions may generate unusable false alarms.","An undecidability label may be rhetorically overextended to biological reality.","UNKNOWN may be coerced into NO by downstream interfaces."]},"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.82,"generator_notes":"Closed-book structural transfer. The target is a class-wide formal reachability claim about executable neural models, not a claim that biological brains themselves are computationally undecidable."}