{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp03_full320_20260801","cell_id":"computability_boundary_mapping__physics","trajectory_id":"R","attempt_index":0,"archetype_slug":"computability_boundary_mapping","domain_slug":"physics","decision":"CANDIDATE","problem_id":"universal_physical_model_reachability_overclaim","causal_lever_id":"explicit_model_relative_reachability_contract","proposal":{"problem":"Computational-physics projects may promise a correct, terminating yes/no answer to whether any finitely specified dynamical model will ever enter a target observable region, while treating simulation timeout as “never.” Whether the unrestricted class is undecidable is a HYPOTHESIS requiring a valid encoding and proof; the independently recognizable problem is the unsupported universal guarantee and deceptive handling of non-results.","actors_substrate":["computational physicists and model authors","simulation and verification software","encoded dynamical models, initial conditions, and target observables","experimental planners and downstream users"],"observable_state":"Requirements say “all models” and “ever,” finite simulations are offered as universal evidence, and timeout, unknown, out-of-scope, and false share one output.","consequence":"Users can mistake finite computational evidence for a theorem, abandon reachable phenomena, or plan experiments from unjustified negative predictions.","affected_objective":"Trustworthy, experimentally meaningful claims about reachability and long-run behavior of physical models.","structural_mapping":[{"archetype_element":"unbounded problem class","domain_realization":"Finitely encoded dynamical laws, parameters, initial states, and target regions without a horizon or model-family bound.","claim_kind":"HYPOTHESIS"},{"archetype_element":"total exact guarantee","domain_realization":"Correct yes/no reachability verdict with termination for every admitted model-query pair.","claim_kind":"HYPOTHESIS"},{"archetype_element":"model-relative evidence","domain_realization":"Classification depends on encoding, arithmetic, precision, evolution semantics, and allowed oracle or measurement access.","claim_kind":"INFERENCE"},{"archetype_element":"constructive versus impossibility evidence","domain_realization":"A total algorithm with proof supports decidability; a valid reduction or diagonal proof supports impossibility.","claim_kind":"CORPUS"},{"archetype_element":"restricted decidable region","domain_realization":"Enforceable finite-state, finite-horizon, or syntactically restricted model families.","claim_kind":"INFERENCE"},{"archetype_element":"honest fallback","domain_realization":"Bounded, one-sided, or sound-abstract analysis returns guarantee-labelled YES, SAFE, UNKNOWN, or OUT_OF_SCOPE.","claim_kind":"INFERENCE"}],"component_map":[{"component":"Problem-Class Specification","status":"adapted","domain_realization":"Define the admitted physical model and reachability-query class."},{"component":"Instance Representation Contract","status":"adapted","domain_realization":"Fix encodings for laws, parameters, states, targets, and precision."},{"component":"Computation Model Contract","status":"adapted","domain_realization":"Declare arithmetic, resources, sensors, experts, and oracles."},{"component":"Solvability Guarantee Profile","status":"direct","domain_realization":"State exactness, soundness, completeness, and termination."},{"component":"Quantifier and Scope Map","status":"direct","domain_realization":"Separate every-model claims from instance and bounded claims."},{"component":"Computability Status Lattice","status":"direct","domain_realization":"Record decidable, recognizable, partial, relative, or unresolved."},{"component":"Constructive Procedure Witness","status":"direct","domain_realization":"Require an algorithm plus correctness and termination arguments."},{"component":"Reduction Preservation Contract","status":"direct","domain_realization":"Require total computable translation preserving the reachability answer."},{"component":"Computability Impossibility Certificate","status":"direct","domain_realization":"Retain a checked reduction or direct proof, if obtained."},{"component":"Assumption Register","status":"adapted","domain_realization":"List encoding, exact-semantics, precision, and model-family assumptions."},{"component":"Decidable Subclass Map","status":"adapted","domain_realization":"Map finite-state, bounded-horizon, and restricted-language regions."},{"component":"One-Sided Recognition Contract","status":"adapted","domain_realization":"Define which reachability witnesses can establish YES."},{"component":"Unknown and Nontermination Policy","status":"direct","domain_realization":"Keep UNKNOWN, timeout, false, and failure distinct."},{"component":"Fallback Solution Contract","status":"adapted","domain_realization":"Label abstraction, bounded search, and escalation guarantees."},{"component":"Computability Guarantee Record","status":"direct","domain_realization":"Version the shipped claim and supporting evidence."},{"component":"Recheck Trigger","status":"adapted","domain_realization":"Reclassify after language, precision, oracle, or model changes."},{"component":"Termination Condition","status":"adapted","domain_realization":"Set explicit time, depth, state, or proof-search bounds."},{"component":"Scope Boundary","status":"direct","domain_realization":"Mechanically reject or quarantine unclassified inputs."},{"component":"Decision Record","status":"direct","domain_realization":"Record chosen boundary, rationale, owner, and expiry."},{"component":"Uncertainty Residue","status":"direct","domain_realization":"List unresolved proof obligations and semantic mismatches."},{"component":"Independent Proof Review","status":"direct","domain_realization":"Have an independent reviewer check the exact formal claim."},{"component":"Complexity Follow-On Gate","status":"direct","domain_realization":"Assess cost only after establishing a decidable region."}],"mechanism_dispositions":[{"slug":"abstract_interpretation_or_model_checking","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Use finite over-approximations for sound safety claims, with false alarms labelled.","counterfactual_removal":"Some unbounded models would lose a terminating sound fallback."},{"slug":"bounded_domain_exhaustive_search","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Exhaust finite horizons or state bounds without extrapolation.","counterfactual_removal":"The pilot would lack a checkable bounded reference verdict."},{"slug":"computability_boundary_decision_record","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Version the boundary, evidence, guarantee, and triggers.","counterfactual_removal":"Guarantees could drift after model changes."},{"slug":"computational_complexity_analysis","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Gate resource analysis to classes first shown decidable.","counterfactual_removal":"Decidable but infeasible methods could be shipped unexamined."},{"slug":"constructive_algorithm_and_correctness_proof","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Supplies positive class-wide evidence.","counterfactual_removal":"Decidability could be inferred from examples alone."},{"slug":"diagonalization_impossibility_proof","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"No self-referential construction is supplied for this physical class.","counterfactual_removal":"No change; impossibility remains unresolved."},{"slug":"enumeration_and_dovetailing","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Unbounded running is unsuitable for the bounded first test; use explicit UNKNOWN.","counterfactual_removal":"No change to the selected terminating protocol."},{"slug":"fallback_mode_router","disposition":"selected_load_bearing","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Route each query to exact, abstract, bounded, or escalation modes.","counterfactual_removal":"Weak results could inherit the universal guarantee."},{"slug":"halting_problem_reduction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Attempt only with an explicit computable embedding into the target model class.","counterfactual_removal":"A negative boundary could not be established by this proof route."},{"slug":"language_fragment_restriction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Define an enforceable model grammar admitting a total procedure.","counterfactual_removal":"The intervention would lack a guaranteed decidable operating region."},{"slug":"many_one_reduction_proof","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Redundant with the selected, more specific halting reduction.","counterfactual_removal":"No change if the specific reduction discharges the same obligations."},{"slug":"promise_problem_restriction","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Unenforced physical promises could yield authoritative wrong answers; prefer syntactic admission.","counterfactual_removal":"No change to the enforceable boundary."},{"slug":"proof_by_counterexample","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Use one in-scope failure to refute an existing universal analyzer claim.","counterfactual_removal":"Over-broad claims would be slower to falsify."},{"slug":"proof_checking","disposition":"selected_supporting","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Independently check the exact formalized theorem and premises.","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":"Gate any hardness verdict on source-to-target direction and named assumptions.","counterfactual_removal":"A reversed reduction could be accepted."},{"slug":"semi_decision_with_explicit_unknown","disposition":"selected_load_bearing","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Return witnessed YES or bounded UNKNOWN, never timeout-as-NO.","counterfactual_removal":"Operational pressure would recreate deceptive Boolean outputs."},{"slug":"theorem_prover_guided_search","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Optional proof discovery adds no guarantee without a faithful formalization and certificate.","counterfactual_removal":"Manual constructive or reduction evidence remains available."},{"slug":"turing_reduction_analysis","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Relative degrees are unnecessary for the initial yes/no boundary and fallback.","counterfactual_removal":"The proposed classification remains intact."}],"causal_chain":["Freeze the physical query class, encoding, computation model, and universal quantifiers.","Seek a total constructive witness and a valid impossibility reduction in parallel.","Classify only what the checked evidence supports; leave mismatches unresolved.","Enforce a decidable fragment and route other inputs to labelled bounded, sound, or UNKNOWN modes.","Version the guarantee and recheck it when assumptions change.","Downstream users stop interpreting timeout or finite simulation as a universal negative."],"baseline":"Run numerical simulation or heuristic search until its budget expires, then report reached/not-reached or silently omit unresolved cases.","nearest_rival":"Increase compute and validation examples while retaining the unrestricted Boolean requirement.","authority_safety":{"affected_parties":["model authors","experimental teams","software users","subjects or environments affected by experiment selection"],"decision_authority":"The physics program lead may authorize a shadow pilot; changing published scientific claims requires the model owner and independent methods reviewer.","authorized_first_step":"For one model family and 30 archived queries, freeze the encoding and horizon, run exhaustive bounded checks plus shadow routing, and compare labels with the baseline; do not alter live experiments.","excluded_actions":["Claiming undecidability without a checked proof","Treating UNKNOWN or timeout as NO","Generalizing bounded results beyond their bound","Letting an unvalidated router gate experiments"],"halt_rollback":"Stop the pilot if an admitted input is misencoded, a supposedly sound verdict misses a bounded counterexample, or users cannot distinguish labels; revert to the baseline outputs with all unresolved cases explicitly marked unclassified."}},"negative_tests":{"strongest_counterevidence":"The actual production class may already be finite, enforceably bounded, and covered by a known total procedure; then this is complexity or implementation work, not a computability-boundary problem.","analogy_break":"Physical models are not automatically programs: continuous quantities, noisy measurements, approximate semantics, and laboratory interaction may defeat the effective encoding or answer-preservation required by a halting reduction.","failure_condition":"The model grammar cannot preserve the experimentally meaningful task, or most real queries fall outside the useful decidable fragment.","problem_falsifier":"Audit finds no universal guarantee, no timeout-as-false behavior, and only explicitly bounded single-instance claims.","intervention_falsifier":"Within the frozen pilot class, routing produces no fewer false negatives or misleading labels than baseline and adds predominantly UNKNOWN results without improving claim calibration.","risks":["A restricted language omits scientifically important dynamics.","A sound abstraction may create unusable false alarms.","Formal proof may certify a semantically wrong physical model.","Boundary labels may be mistaken for claims about nature rather than the encoded model."]},"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 mapping. The existence of a universal undecidability result for the proposed physics class is not asserted; it is an explicit proof obligation."}