{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp03_full320_20260801","cell_id":"computability_boundary_mapping__geoengineering_planetary_science","trajectory_id":"R","attempt_index":0,"archetype_slug":"computability_boundary_mapping","domain_slug":"geoengineering_planetary_science","decision":"CANDIDATE","problem_id":"unrestricted_geoengineering_controller_safety_decision","causal_lever_id":"enforced_decidable_controller_fragment_with_labeled_fallbacks","proposal":{"problem":"A geoengineering assurance program may require an automated tool to return a correct, terminating safe/unsafe verdict for every adaptive intervention controller coupled to every admitted executable planetary model. If the controller or model language is unrestricted, finite successful simulations and timeouts cannot establish that universal guarantee, yet downstream approval workflows may still collapse timeout, unknown, and safe into a Boolean decision.","actors_substrate":["geoengineering modelers and controller designers","independent safety reviewers","research sponsors and regulators","communities exposed to modeled intervention risks","executable planetary models, controller programs, and verification infrastructure"],"observable_state":"The assurance interface accepts an open-ended controller/model class, promises universal termination and exactness, cites simulations or analyzer runs rather than a class-wide proof, and lacks distinct UNKNOWN, OUT_OF_SCOPE, and TIMEOUT states.","consequence":"A tool may clear an unsafe policy, reject a viable one, or consume indefinite resources while presenting a stronger assurance claim than its evidence supports.","affected_objective":"Obtain auditable pre-deployment safety evidence without converting bounded simulation or incomplete analysis into universal planetary-safety certification.","structural_mapping":[{"archetype_element":"unrestricted input class","domain_realization":"Arbitrary encoded geoengineering controllers coupled to admitted executable planetary models and threshold specifications.","claim_kind":"HYPOTHESIS"},{"archetype_element":"total exact decider requirement","domain_realization":"For every admitted controller/model pair, terminate and decide whether any execution violates a stated safety property.","claim_kind":"HYPOTHESIS"},{"archetype_element":"model-relative computability boundary","domain_realization":"The verdict depends on controller expressiveness, model semantics, nondeterminism, finite bounds, sensors, and external expert inputs.","claim_kind":"INFERENCE"},{"archetype_element":"decidable restricted region","domain_realization":"Mechanically enforced finite-state or otherwise proven-decidable controller/model fragments with explicit property semantics.","claim_kind":"HYPOTHESIS"},{"archetype_element":"honest weaker fallback","domain_realization":"Sound abstraction, bounded exploration, or witness-producing search that returns labeled alarms or UNKNOWN without claiming exact unrestricted safety.","claim_kind":"INFERENCE"},{"archetype_element":"reclassification trigger","domain_realization":"Changes to model language, controller expressiveness, property semantics, bounds, or external information sources reopen the guarantee.","claim_kind":"INFERENCE"}],"component_map":[{"component":"Problem-Class Specification","status":"adapted","domain_realization":"Define the admitted controller/model/property triples."},{"component":"Instance Representation Contract","status":"adapted","domain_realization":"Version grammars, numeric semantics, initial states, disturbances, and encodings."},{"component":"Computation Model Contract","status":"adapted","domain_realization":"Declare machine model, precision, nondeterminism, oracle-like sensors, and expert interaction."},{"component":"Solvability Guarantee Profile","status":"adapted","domain_realization":"Separate exact decision, one-sided soundness, bounded completeness, and approximation."},{"component":"Quantifier and Scope Map","status":"adapted","domain_realization":"State whether claims cover every controller, state, disturbance, trace, and horizon."},{"component":"Computability Status Lattice","status":"adapted","domain_realization":"Classify fragments as decidable, recognizable, partial, relative, or unresolved."},{"component":"Constructive Procedure Witness","status":"adapted","domain_realization":"For each decidable fragment, retain the verifier plus correctness and termination arguments."},{"component":"Reduction Preservation Contract","status":"adapted","domain_realization":"Require any impossibility transfer to preserve the target safety question under a computable encoding."},{"component":"Computability Impossibility Certificate","status":"adapted","domain_realization":"Treat unrestricted undecidability as unproved until a matching reduction or direct proof exists."},{"component":"Assumption Register","status":"direct","domain_realization":"Record semantics, bounds, determinism, abstraction soundness, and external capabilities."},{"component":"Decidable Subclass Map","status":"adapted","domain_realization":"List enforceable finite-state or otherwise decidable controller/model fragments."},{"component":"One-Sided Recognition Contract","status":"adapted","domain_realization":"Specify which verdict has sound witnesses and which side may remain unresolved."},{"component":"Unknown and Nontermination Policy","status":"direct","domain_realization":"Keep UNKNOWN, TIMEOUT, OUT_OF_SCOPE, FALSE, and TOOL_FAILURE distinct."},{"component":"Fallback Solution Contract","status":"adapted","domain_realization":"Label the guarantee attached to abstraction, bounded search, or escalation."},{"component":"Computability Guarantee Record","status":"adapted","domain_realization":"Version-link each public assurance statement to its model, scope, and evidence."},{"component":"Recheck Trigger","status":"adapted","domain_realization":"Reassess after language, semantics, bounds, property, or oracle changes."},{"component":"Termination Condition","status":"direct","domain_realization":"Set explicit resource or horizon bounds for every operational analysis."},{"component":"Scope Boundary","status":"adapted","domain_realization":"Mechanically reject or quarantine controller/model inputs outside the certified fragment."},{"component":"Decision Record","status":"direct","domain_realization":"Record the chosen assurance mode and why stronger language is unavailable."},{"component":"Uncertainty Residue","status":"adapted","domain_realization":"Publish unproved obligations, abstraction alarms, and model-reality mismatch."},{"component":"Independent Proof Review","status":"direct","domain_realization":"Have an independent reviewer check formal statements, proofs, and encodings."},{"component":"Complexity Follow-On Gate","status":"adapted","domain_realization":"After decidability, test whether verification fits operational time and memory budgets."}],"mechanism_dispositions":[{"slug":"abstract_interpretation_or_model_checking","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Use a finite over-approximation with a proved simulation relation; only the sound verdict inherits a real-system claim.","counterfactual_removal":"The proposal loses its scalable sound fallback for admitted but large models."},{"slug":"bounded_domain_exhaustive_search","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Exhaustively compare the pilot verifier against all cases in a small encoded fragment.","counterfactual_removal":"Early completeness and label tests become sampling-based."},{"slug":"computability_boundary_decision_record","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Version the shipped guarantee, assumptions, and recheck triggers.","counterfactual_removal":"Scope and guarantee can drift without traceability."},{"slug":"computational_complexity_analysis","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Apply only after a fragment has a total procedure.","counterfactual_removal":"A decidable but unusable fragment could pass the gate."},{"slug":"constructive_algorithm_and_correctness_proof","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Require a total, correct verifier for each certified fragment.","counterfactual_removal":"The decidable-zone guarantee would rest on tests rather than a witness."},{"slug":"diagonalization_impossibility_proof","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"No target-specific self-referential construction is supplied.","counterfactual_removal":"No current causal or safety claim changes."},{"slug":"enumeration_and_dovetailing","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Operational bounded witness search is covered by explicit-UNKNOWN protocol; indefinite running is unsuitable.","counterfactual_removal":"No selected guarantee changes."},{"slug":"fallback_mode_router","disposition":"selected_load_bearing","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Route to exact-fragment, sound-abstraction, bounded-search, or escalation modes and label each result.","counterfactual_removal":"Weaker outputs could be mistaken for unrestricted certification."},{"slug":"halting_problem_reduction","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Do not invoke unless the domain encoding and safety-property preservation are proved.","counterfactual_removal":"The unrestricted class remains unresolved rather than declared undecidable."},{"slug":"language_fragment_restriction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Enforce a syntactic controller/model fragment with a known terminating verifier.","counterfactual_removal":"There is no enforceable boundary supporting total exact verdicts."},{"slug":"many_one_reduction_proof","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Reserve for a future target-specific impossibility argument.","counterfactual_removal":"No present verdict changes."},{"slug":"promise_problem_restriction","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"A syntactically enforced fragment is safer than unchecked semantic promises for approval use.","counterfactual_removal":"Scope remains enforced by parsing and typing."},{"slug":"proof_by_counterexample","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Use one in-scope failure to refute an overbroad analyzer claim, not to establish impossibility.","counterfactual_removal":"Universal overclaims become harder to retire cheaply."},{"slug":"proof_checking","disposition":"selected_supporting","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Independently check termination, soundness, and statement-model alignment.","counterfactual_removal":"Subtle proof or assumption gaps can enter the assurance record."},{"slug":"reduction_direction_checklist","disposition":"selected_supporting","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Gate any future undecidability claim before it affects program scope.","counterfactual_removal":"A reversed or assumption-mismatched reduction may be trusted."},{"slug":"semi_decision_with_explicit_unknown","disposition":"selected_load_bearing","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Bound witness search and return UNKNOWN, never NO or SAFE, when unconfirmed.","counterfactual_removal":"Timeout can be laundered into a false negative or safety clearance."},{"slug":"theorem_prover_guided_search","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Optional proof discovery adds no guarantee without a validated formalization and certificate checker.","counterfactual_removal":"Manual construction and independent checking remain sufficient for the first test."},{"slug":"turing_reduction_analysis","disposition":"incompatible","contribution_type":"NONE","adaptation_or_rejection":"No oracle-relative classification is needed for the bounded assurance interface.","counterfactual_removal":"The selected boundary and fallback remain unchanged."}],"causal_chain":["Specify controller, model, property, quantifiers, and computation model.","Mechanically separate a certified decidable fragment from unrestricted or unresolved inputs.","Run a proved total verifier inside the fragment; route other inputs only to sound, bounded, explicitly labeled fallbacks.","Preserve UNKNOWN, TIMEOUT, and OUT_OF_SCOPE through downstream approval interfaces.","Record assumptions and triggers, preventing bounded evidence from becoming universal certification."],"baseline":"Run scenario ensembles and expert review, impose a timeout, and convert the available result into a practical safe/unsafe recommendation without a formal class-wide termination or completeness claim.","nearest_rival":"Require larger simulation ensembles and conservative safety margins while retaining a Boolean approval interface.","authority_safety":{"affected_parties":["populations in potentially affected regions","future generations","ecosystems","geoengineering researchers and operators","regulators and independent reviewers"],"decision_authority":"The pilot team may define an analysis interface and recommend assurance language; it may not authorize environmental deployment or waive applicable scientific, public, or regulatory review.","authorized_first_step":"Offline pilot on toy and archived synthetic controller/model pairs: define one finite fragment, prove its verifier contract, exhaustively test a small bound, and compare result labels with the baseline.","excluded_actions":["physical geoengineering deployment","treating UNKNOWN or timeout as SAFE","claiming unrestricted undecidability without a valid target-specific proof","silently accepting out-of-fragment inputs","using verifier output as sole deployment authorization"],"halt_rollback":"Halt if any concrete admitted trace is omitted by the claimed sound abstraction, an out-of-scope input receives an exact verdict, labels are collapsed downstream, or proof review finds a material gap; withdraw the guarantee record and revert to non-certifying research use."}},"negative_tests":{"strongest_counterevidence":"The packet provides no evidence that a real program demands universal exact verification. Existing assurance work may already use finite horizons, restricted controller languages, probabilistic claims, and explicit model uncertainty, in which case the proposed computability diagnosis adds little.","analogy_break":"Planetary behavior is not identical to program semantics. A fixed discretized simulator, controller set, horizon, and finite-precision encoding may be decidable by enumeration, while the dominant real-world obstacle may be model error and unobserved physics rather than computability.","failure_condition":"The approach fails operationally if the enforceable fragment excludes most decision-relevant controllers or sound abstraction produces so many alarms that reviewers bypass it.","problem_falsifier":"No independently recognizable problem remains if stakeholders require only bounded or probabilistic analysis, never claim universal exact termination, and already preserve UNKNOWN, timeout, and scope labels.","intervention_falsifier":"Reject the intervention if, on the bounded pilot, the certified verifier misses any admitted unsafe trace, mislabels any out-of-fragment case, or provides no useful assurance coverage over the nearest rival at comparable resources.","risks":["A formally sound result may concern a planetary model that is semantically unfaithful to reality.","Restriction may exclude novel but important intervention policies.","False alarms may create alert fatigue.","Formal labels may acquire unwarranted political authority.","Complexity may make a decidable fragment operationally 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.74,"generator_notes":"Closed-book structural transfer. The domain problem and empirical prevalence are hypotheses; no target-specific undecidability result is claimed."}