{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp03_full320_20260801","cell_id":"computability_boundary_mapping__sport_science","trajectory_id":"R","attempt_index":0,"archetype_slug":"computability_boundary_mapping","domain_slug":"sport_science","decision":"CANDIDATE","problem_id":"universal_adaptive_training_safety_verification","causal_lever_id":"model_relative_training_verification_boundary","proposal":{"problem":"Sport-science teams may require an analyzer to decide, exactly and with guaranteed termination, whether any adaptive training program paired with any admissible executable athlete model will ever enter a prohibited physiological or biomechanical state. The unrestricted model language, universal quantifiers, and treatment of timeout are often implicit, so simulations may be overgeneralized into safety clearances or failed searches mistaken for evidence of safety.","actors_substrate":["sport scientists building athlete and training-controller models","coaches and performance staff using analyzer outputs","athletes represented by or exposed to resulting prescriptions","sports-medicine and research-governance reviewers","software teams implementing simulation and verification"],"observable_state":"A Boolean safe/unsafe interface covers open-ended executable models; passing finite simulations is cited as universal evidence; timeouts become safe or false; model restrictions drift without corresponding changes to the published guarantee.","consequence":"Resources are spent pursuing an unsupported universal verifier, while false safety clearance, excessive blanket rejection, and opaque unknown states can distort training decisions.","affected_objective":"Obtain useful automated safety evidence without overstating which athlete-model and controller classes can be decided exactly or allowing analysis output alone to authorize athlete exposure.","structural_mapping":[{"archetype_element":"Open-ended problem class","domain_realization":"Pairs of adaptive training controllers and executable athlete-response models with a reachability question over prohibited states.","claim_kind":"HYPOTHESIS"},{"archetype_element":"Universal exact terminating requirement","domain_realization":"Return a correct safe/unsafe answer for every admissible pair and every possible modeled trajectory.","claim_kind":"INFERENCE"},{"archetype_element":"Computability boundary","domain_realization":"Classify verification relative to the model language, state representation, allowed observations, and required guarantee.","claim_kind":"INFERENCE"},{"archetype_element":"Decidable region","domain_realization":"Mechanically enforceable finite-state, bounded-horizon, or otherwise proven-total model fragments.","claim_kind":"HYPOTHESIS"},{"archetype_element":"Honest fallback","domain_realization":"Route to exact, sound one-sided, bounded, or human-reviewed modes while preserving UNKNOWN and OUT_OF_SCOPE.","claim_kind":"INFERENCE"},{"archetype_element":"Reclassification trigger","domain_realization":"Recheck whenever model expressiveness, horizon, sensors, external expertise, or the safety predicate changes.","claim_kind":"INFERENCE"}],"component_map":[{"component":"Problem-Class Specification","status":"adapted","domain_realization":"Define controller–athlete-model pairs and prohibited-state reachability."},{"component":"Instance Representation Contract","status":"adapted","domain_realization":"Version model code, initial states, uncertainty sets, horizon, and safety predicate."},{"component":"Computation Model Contract","status":"adapted","domain_realization":"Declare execution semantics, numeric assumptions, nondeterminism, sensors, and external experts."},{"component":"Solvability Guarantee Profile","status":"direct","domain_realization":"Separate exact decision, one-sided evidence, bounded checking, and approximation."},{"component":"Quantifier and Scope Map","status":"direct","domain_realization":"Expose every-program, every-model, every-state, and unbounded-time quantifiers."},{"component":"Computability Status Lattice","status":"direct","domain_realization":"Record decidable, recognizable, partial, relative, unresolved, or unsupported."},{"component":"Constructive Procedure Witness","status":"adapted","domain_realization":"Require an algorithm plus correctness and termination arguments for any decidable fragment."},{"component":"Reduction Preservation Contract","status":"adapted","domain_realization":"Require a computable, property-preserving translation before transferring undecidability."},{"component":"Computability Impossibility Certificate","status":"adapted","domain_realization":"Retain a checked reduction or direct proof scoped to the formal model class."},{"component":"Assumption Register","status":"direct","domain_realization":"Register encoding, model fidelity, arithmetic, horizon, and oracle assumptions."},{"component":"Decidable Subclass Map","status":"adapted","domain_realization":"Map enforceable finite-state and bounded-horizon fragments."},{"component":"One-Sided Recognition Contract","status":"adapted","domain_realization":"Permit confirmed unsafe witnesses without interpreting absence as safe."},{"component":"Unknown and Nontermination Policy","status":"direct","domain_realization":"Keep UNKNOWN, TIMEOUT, OUT_OF_SCOPE, SAFE, and UNSAFE distinct."},{"component":"Fallback Solution Contract","status":"direct","domain_realization":"Label each result with the actual mode and guarantee."},{"component":"Computability Guarantee Record","status":"direct","domain_realization":"Version-link formal class, evidence, guarantee, and public wording."},{"component":"Recheck Trigger","status":"direct","domain_realization":"Trigger review when model language, predicate, horizon, or external capability changes."},{"component":"Termination Condition","status":"direct","domain_realization":"Set explicit bounds for operational modes and return UNKNOWN when exhausted."},{"component":"Scope Boundary","status":"direct","domain_realization":"Mechanically reject or quarantine inputs outside guaranteed fragments."},{"component":"Decision Record","status":"direct","domain_realization":"Record the shipped boundary, reasons, owner, and supersession history."},{"component":"Uncertainty Residue","status":"direct","domain_realization":"List unproved obligations and model-to-athlete validity gaps."},{"component":"Independent Proof Review","status":"direct","domain_realization":"Have an independent reviewer check reductions and constructive proofs."},{"component":"Complexity Follow-On Gate","status":"direct","domain_realization":"After decidability, assess state explosion and operational resource cost."}],"mechanism_dispositions":[{"slug":"abstract_interpretation_or_model_checking","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Use a conservative finite abstraction to produce sound model-relative safety conclusions, with false alarms explicit.","counterfactual_removal":"No sound scalable fallback would bridge unrestricted models and finite verification."},{"slug":"bounded_domain_exhaustive_search","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Exhaustively check a small, fully enumerated controller-model library in the first test.","counterfactual_removal":"The pilot would lack a terminating reference set with complete within-bound coverage."},{"slug":"computability_boundary_decision_record","disposition":"selected_load_bearing","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Version the boundary, guarantee, assumptions, and recheck triggers.","counterfactual_removal":"Guarantees could drift when models or predicates change."},{"slug":"computational_complexity_analysis","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Apply only after a fragment is shown decidable.","counterfactual_removal":"Decidable but unusable fragments could be mistaken for deployable ones."},{"slug":"constructive_algorithm_and_correctness_proof","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Require totality and correctness evidence for exact fragment verifiers.","counterfactual_removal":"Exact-decider claims would rest on tests rather than class-wide obligations."},{"slug":"diagonalization_impossibility_proof","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"A direct self-reference proof is unnecessary if a simpler scoped reduction is available.","counterfactual_removal":"No material change; it duplicates the impossibility route."},{"slug":"enumeration_and_dovetailing","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Unbounded recognition is unsuitable for operational safety decisions; use bounded explicit UNKNOWN.","counterfactual_removal":"No change to the bounded interface."},{"slug":"fallback_mode_router","disposition":"selected_load_bearing","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Route each instance to exact, conservative, bounded, or escalation modes and label the guarantee.","counterfactual_removal":"Weaker outputs could be laundered into universal safety verdicts."},{"slug":"halting_problem_reduction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Attempt a formal source-to-target reduction only for an unrestricted Turing-complete model language; until checked, status remains unresolved.","counterfactual_removal":"There would be no justified basis for retiring the unrestricted exact-decider requirement."},{"slug":"language_fragment_restriction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Enforce a syntactic model fragment admitting total verification.","counterfactual_removal":"The project could not convert the boundary into an enforceable exact-service scope."},{"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 second mechanism.","counterfactual_removal":"No change if the selected reduction still proves totality, computability, and preservation."},{"slug":"promise_problem_restriction","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Unenforced athlete-model promises could yield authoritative-looking wrong answers; prefer checkable syntax.","counterfactual_removal":"No loss because fragment membership supplies a safer boundary."},{"slug":"proof_by_counterexample","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Use an in-scope adversarial model to refute any overbroad verifier claim.","counterfactual_removal":"Universal overclaims would be harder to falsify cheaply."},{"slug":"proof_checking","disposition":"selected_load_bearing","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Independently check the exact formal theorem and exposed assumptions.","counterfactual_removal":"A flawed proof could authorize an invalid safety guarantee."},{"slug":"reduction_direction_checklist","disposition":"selected_supporting","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Gate the impossibility certificate on source-to-target direction and named assumptions.","counterfactual_removal":"A reversed or incomplete reduction could be accepted."},{"slug":"semi_decision_with_explicit_unknown","disposition":"selected_load_bearing","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Confirm UNSAFE only with a witness; at the resource bound return UNKNOWN, never SAFE.","counterfactual_removal":"Timeout could again masquerade as safety."},{"slug":"theorem_prover_guided_search","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Optionally seek checkable certificates while retaining open obligations on failure.","counterfactual_removal":"Evidence may be slower or manual, but the causal design remains viable."},{"slug":"turing_reduction_analysis","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Relative computability degrees do not answer the immediate shipped-guarantee question.","counterfactual_removal":"No material change to the boundary decision."}],"causal_chain":["Specify the represented verification class, quantifiers, computation model, and exact guarantee.","Seek both a total constructive verifier and a scoped impossibility reduction; classify unresolved gaps honestly.","Enforce decidable fragments and conservative finite abstractions rather than silently narrowing scope.","Route instances by applicable guarantee and preserve UNKNOWN, TIMEOUT, and OUT_OF_SCOPE.","Record assumptions and independently review proofs so model changes trigger reclassification.","This reduces unsupported universal safety claims while retaining useful bounded evidence."],"baseline":"Run simulations and heuristic searches, apply a timeout, and issue or imply a Boolean safety verdict from observed cases.","nearest_rival":"A conventional validation program that benchmarks prediction accuracy and calibration on recorded athlete data without classifying whether the formal universal verification requirement is computable.","authority_safety":{"affected_parties":["athletes whose training could change","coaches and performance staff","sports-medicine clinicians","sport-science researchers and software operators"],"decision_authority":"The sports-medicine or research-governance authority retains athlete-exposure authority; the verifier owner may classify model-relative evidence but not clear training independently.","authorized_first_step":"Shadow-test the classification and router on a finite synthetic and previously reviewed model library; compare labels with exhaustive within-bound results without changing training.","excluded_actions":["autonomous prescription changes","claiming real-world injury prevention from model verification","treating UNKNOWN or timeout as SAFE","including athlete data or exposure without existing consent and governance","generalizing beyond the checked model fragment"],"halt_rollback":"Halt the pilot and withdraw its guarantee if any known unsafe bounded case is labeled SAFE, an input bypasses scope enforcement, proof review finds a gap, or outputs influence training; revert to non-authoritative simulation reports."}},"negative_tests":{"strongest_counterevidence":"The deployed model language may already be finite, bounded, and effectively enumerable, with a known total reachability procedure; then the issue is complexity and model validity, not computability.","analogy_break":"Athletes and physiology are not programs. An impossibility result applies only to the chosen executable representation and guarantee; it neither proves physical unpredictability nor validates the model's safety predicate.","failure_condition":"The approach fails if the real requirement cannot be formalized faithfully, fragment membership cannot be enforced, or conservative analysis produces too many UNKNOWN or false-alarm results to support decisions.","problem_falsifier":"Inventory shows every admitted controller-model pair has a fixed finite representation and horizon, scope enforcement is complete, and an existing total correct procedure covers the exact claimed class; no universal open-ended claim or timeout-as-verdict practice remains.","intervention_falsifier":"In the bounded shadow test, boundary mapping and routing do not reduce false SAFE labels or guarantee ambiguity relative to the rival, or they make the usable-answer rate fall below a predeclared threshold without improving safety.","risks":["A formally correct result may be unsafe because the athlete model or prohibited-state predicate is wrong.","Conservative abstraction may overwhelm staff with false alarms.","Scope restrictions may exclude common cases while marketing preserves broad language.","Human escalation may be treated as an infallible oracle.","The impossibility analogy may discourage useful bounded or statistical work."]},"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.78,"generator_notes":"Closed-book structural transfer. The candidate is conditional on the analyzer accepting an open-ended executable model class; no claim is made that current sport-science systems actually use that class or that undecidability has been proved."}