{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp03_full320_20260801","cell_id":"computability_boundary_mapping__performing_arts_theatre","trajectory_id":"R","attempt_index":0,"archetype_slug":"computability_boundary_mapping","domain_slug":"performing_arts_theatre","decision":"CANDIDATE","problem_id":"unbounded_interactive_stage_score_verification","causal_lever_id":"enforceable_score_fragment_with_labeled_fallbacks","proposal":{"problem":"A theatre company claims that a pre-performance checker can always determine whether any programmable, sensor-responsive stage score will terminate and avoid forbidden performer, machinery, or cue states. The accepted score language, environmental inputs, and guarantee are unbounded or implicit, so timeouts and unexamined cases can be reported as safe or impossible.","actors_substrate":["performers and stage crew","directors and dramaturgs","stage-management and automation teams","interactive cue software, sensors, machinery, and encoded performance scores","audiences and venue operators"],"observable_state":"The checker publishes Boolean safe/unsafe results for arbitrary interactive scores, while documentation does not distinguish bounded coverage, abstraction alarms, timeout, out-of-scope input, or unresolved status.","consequence":"Productions may rely on unsupported safety or completion claims, discard viable scores after inconclusive searches, or keep investing in an unjustified universal checker.","affected_objective":"Truthful and operationally safe verification of interactive theatrical performances without silently sacrificing artistic expressiveness.","structural_mapping":[{"archetype_element":"open-ended problem class","domain_realization":"All encoded performance scores with loops, branching, sensors, improvisational input, and stage-device actions.","claim_kind":"HYPOTHESIS"},{"archetype_element":"total exact decision requirement","domain_realization":"Always decide whether every possible live execution terminates without reaching a forbidden stage state.","claim_kind":"HYPOTHESIS"},{"archetype_element":"decidable region","domain_realization":"Mechanically enforceable finite-state score fragments and explicitly bounded performance horizons.","claim_kind":"INFERENCE"},{"archetype_element":"honest weaker fallback","domain_realization":"Sound finite abstraction, bounded exploration, or witness search returning SAFE, VIOLATION-WITNESS, or UNKNOWN with its guarantee.","claim_kind":"INFERENCE"},{"archetype_element":"reclassification trigger","domain_realization":"Changes to score grammar, sensor model, device semantics, improvisation interface, or verification bound.","claim_kind":"INFERENCE"}],"component_map":[{"component":"Problem-Class Specification","status":"direct","domain_realization":"Define the class of interactive performance scores and queried properties."},{"component":"Instance Representation Contract","status":"direct","domain_realization":"Version the score grammar, cue semantics, sensors, devices, and initial state."},{"component":"Computation Model Contract","status":"adapted","domain_realization":"State what environmental information and interaction the checker may use."},{"component":"Solvability Guarantee Profile","status":"direct","domain_realization":"Separate total exact, sound incomplete, bounded, and unresolved guarantees."},{"component":"Quantifier and Scope Map","status":"direct","domain_realization":"Distinguish one run, all runs within a horizon, and all possible executions."},{"component":"Computability Status Lattice","status":"direct","domain_realization":"Classify score/property pairs as decidable, recognizable, relative, or unresolved."},{"component":"Constructive Procedure Witness","status":"adapted","domain_realization":"Retain an executable checker plus termination and correctness arguments for each safe fragment."},{"component":"Reduction Preservation Contract","status":"omitted","domain_realization":"Required only if an impossibility claim is later based on reduction."},{"component":"Computability Impossibility Certificate","status":"omitted","domain_realization":"No impossibility verdict without a matching proof."},{"component":"Assumption Register","status":"direct","domain_realization":"Record device, sensor, performer-input, and semantic assumptions."},{"component":"Decidable Subclass Map","status":"direct","domain_realization":"Map enforceable finite-state and bounded-horizon score classes."},{"component":"One-Sided Recognition Contract","status":"adapted","domain_realization":"A found unsafe trace is confirmatory; failure to find one is not safety."},{"component":"Unknown and Nontermination Policy","status":"direct","domain_realization":"Keep UNKNOWN, TIMEOUT, OUT_OF_SCOPE, and tool failure distinct."},{"component":"Fallback Solution Contract","status":"direct","domain_realization":"Route eligible scores to exact, abstract, bounded, or human-reviewed modes."},{"component":"Computability Guarantee Record","status":"direct","domain_realization":"Version the shipped claim with its evidence and limitations."},{"component":"Recheck Trigger","status":"direct","domain_realization":"Reassess after semantic, language, hardware, or interaction changes."},{"component":"Termination Condition","status":"direct","domain_realization":"Publish finite-state completion or explicit resource bounds."},{"component":"Scope Boundary","status":"direct","domain_realization":"Mechanically reject or quarantine scores outside a guaranteed fragment."},{"component":"Decision Record","status":"direct","domain_realization":"Record why each verification mode and public claim was chosen."},{"component":"Uncertainty Residue","status":"direct","domain_realization":"List unproved obligations, abstraction alarms, and uncovered behaviors."},{"component":"Independent Proof Review","status":"direct","domain_realization":"Have an independent reviewer check formal claims and semantic fidelity."},{"component":"Complexity Follow-On Gate","status":"direct","domain_realization":"Assess runtime and state explosion only after decidability is established."}],"mechanism_dispositions":[{"slug":"abstract_interpretation_or_model_checking","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Over-approximate score, machinery, and sensor behavior on a finite model; SAFE is trusted only under checked abstraction soundness.","counterfactual_removal":"The fallback loses a terminating sound safety verdict for scores not exhaustively concrete-checkable."},{"slug":"bounded_domain_exhaustive_search","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Explore every trace inside a declared cue-count, time, and input bound.","counterfactual_removal":"The pilot loses complete within-bound evidence but retains the core boundary policy."},{"slug":"computability_boundary_decision_record","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Version scope, guarantee, assumptions, and recheck triggers per production.","counterfactual_removal":"Guarantees can drift silently between rehearsal, venue, and software revisions."},{"slug":"computational_complexity_analysis","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Measure state growth after a fragment is classified decidable.","counterfactual_removal":"Correct fragments may still be operationally unusable without warning."},{"slug":"constructive_algorithm_and_correctness_proof","disposition":"selected_supporting","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Require a terminating correct checker witness for any total-exact claim.","counterfactual_removal":"A decidability claim could rest on demonstrations rather than a class-wide witness."},{"slug":"diagonalization_impossibility_proof","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"No domain-specific diagonal construction is supplied.","counterfactual_removal":"No change; the proposal makes no impossibility verdict."},{"slug":"enumeration_and_dovetailing","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Witness search is useful, but unbounded operation is unsuitable around live-production decisions.","counterfactual_removal":"No change because bounded tri-state search is used."},{"slug":"fallback_mode_router","disposition":"selected_load_bearing","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Dispatch each score to exact, abstract, bounded, or manual review and label the resulting guarantee.","counterfactual_removal":"Weaker evidence could again be presented as a universal Boolean verdict."},{"slug":"halting_problem_reduction","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"No property-preserving encoding from halting instances is established.","counterfactual_removal":"No change; unrestricted status remains unresolved."},{"slug":"language_fragment_restriction","disposition":"selected_load_bearing","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Provide a mechanically checkable finite-state score grammar for total verification.","counterfactual_removal":"The system cannot enforce the boundary on which its strongest guarantee depends."},{"slug":"many_one_reduction_proof","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"No status-transfer claim is needed in the first test.","counterfactual_removal":"No change."},{"slug":"promise_problem_restriction","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Unenforced promises are weaker than syntactic fragment enforcement for safety-facing use.","counterfactual_removal":"No change."},{"slug":"proof_by_counterexample","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Use one in-scope misclassified score to refute an advertised universal checker claim.","counterfactual_removal":"Universal overclaims become harder to falsify cheaply."},{"slug":"proof_checking","disposition":"selected_supporting","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Independently check termination, correctness, and abstraction-soundness arguments.","counterfactual_removal":"Formal-looking but defective guarantees can pass into production."},{"slug":"reduction_direction_checklist","disposition":"unused","contribution_type":"NONE","adaptation_or_rejection":"Activate only if a reduction-based impossibility certificate is proposed.","counterfactual_removal":"No current effect."},{"slug":"semi_decision_with_explicit_unknown","disposition":"selected_load_bearing","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Bound witness search and return UNKNOWN rather than NO or SAFE when unconfirmed.","counterfactual_removal":"Timeout can again be laundered into a false safety conclusion."},{"slug":"theorem_prover_guided_search","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Formal proof search is not necessary for the bounded first test.","counterfactual_removal":"No change; independent review remains."},{"slug":"turing_reduction_analysis","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Relative computability degrees do not answer the operational theatre decision.","counterfactual_removal":"No change."}],"causal_chain":["Make score syntax, execution semantics, environment, quantifiers, and guarantee explicit.","Mechanically separate an enforceable finite-state fragment from unrestricted or changed scores.","Apply exact checking inside that fragment and labeled abstract or bounded modes elsewhere.","Preserve UNKNOWN, TIMEOUT, and OUT_OF_SCOPE instead of coercing them into safe/unsafe.","Review and version evidence, assumptions, and triggers before rehearsal reliance.","Unsupported universal claims shrink while safety-relevant outputs become auditable."],"baseline":"Ordinary practice is ad hoc rehearsal, finite scenario testing, timeouts, and expert judgment presented through a Boolean readiness decision.","nearest_rival":"More rehearsal and simulation coverage without a formal scope contract; it can find defects but cannot justify a class-wide termination or safety guarantee.","authority_safety":{"affected_parties":["performers","crew","audiences","venue operators","artists whose work is excluded by the restricted fragment"],"decision_authority":"The production safety lead and stage-management authority approve operational reliance; artists control whether a score is altered, simplified, or withdrawn.","authorized_first_step":"On one non-public rehearsal system, encode ten representative scores plus seeded unsafe variants; compare exact fragment checking, finite abstraction, and bounded search against witnessed traces and expert review.","excluded_actions":["No autonomous control of live machinery based solely on the pilot.","No SAFE label for UNKNOWN, timeout, abstraction failure, or out-of-scope scores.","No claim that unrestricted interactive theatre scores are undecidable without a checked proof.","No silent rewriting of artistic scores to fit the restricted fragment."],"halt_rollback":"Stop reliance immediately on a false SAFE, missing concrete behavior in the abstraction, unclassified input, or semantic mismatch; revert to existing rehearsal interlocks and manual stage-management authority."}},"negative_tests":{"strongest_counterevidence":"The accepted score language and environment may already be finite, fully specified, and covered by a proven total checker; then this is complexity or assurance work, not computability-boundary mapping.","analogy_break":"Live performers and physical environments are not merely program states; formal verification is relevant only to the encoded score-and-environment model, not to all theatrical meaning, improvisation, or real-world safety.","failure_condition":"The fragment excludes routine artistic practices, membership cannot be enforced, or outputs are relabeled without changing production decisions.","problem_falsifier":"Audit shows no universal or total claim: staff already distinguish bounded results, unknowns, out-of-scope cases, and manual authority, with scope-linked evidence.","intervention_falsifier":"During the bounded pilot, the new routing and labels do not reduce false Boolean conclusions or reveal any scope/assumption mismatch relative to baseline review.","risks":["A finite abstraction may omit real performer or machinery behavior and produce false confidence.","Restricting the score language may suppress artistically essential interaction.","Frequent UNKNOWN results may invite informal override.","Formal records may acquire authority beyond the model they document.","Verification effort may displace physical rehearsal and established interlocks."]},"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":"Candidate depends on an expressive programmable performance-score system and an actual universal terminating verification claim. It deliberately leaves unrestricted computability unresolved pending a domain-faithful proof."}