{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp03_full320_20260801","cell_id":"computability_boundary_mapping__logistics_supply_chain","trajectory_id":"R","attempt_index":0,"archetype_slug":"computability_boundary_mapping","domain_slug":"logistics_supply_chain","decision":"CANDIDATE","problem_id":"unbounded_fulfillment_policy_safety_decision","causal_lever_id":"enforceable_policy_fragment_and_honest_fallback_routing","proposal":{"problem":"A supply-chain platform promises a correct, terminating yes/no answer to whether every policy expressible in an open-ended fulfillment-rule language will avoid deadlock, non-delivery, or rule cycling under all admissible event sequences. Timeouts are treated as unsafe or safe, although the language, queue bounds, external actors, and required universal guarantee are unspecified. If policies permit unbounded state or general computation, the total-exact analyzer may be impossible; if the operational model is finite, the issue may instead be ordinary state-space complexity. Both remain hypotheses until the representation and model are fixed.","actors_substrate":["supply-chain platform owner","policy authors and planners","warehouse and transport operators","suppliers and carriers","customers awaiting fulfillment","compliance and audit teams","rule DSL, event streams, queues, inventories, and external-service responses"],"observable_state":"Analyzer outcomes labeled safe/unsafe despite timeout, silent scope narrowing, or unresolved external calls; repeated failures on larger or cyclic policies; no distinct unknown or out-of-scope state.","consequence":"Policies may be falsely cleared, falsely rejected, or subjected to endless universal-automation investment, causing stranded orders, excess buffers, avoidable manual work, and misleading assurance.","affected_objective":"Reliable order fulfillment with auditable safety guarantees and proportionate analysis cost.","structural_mapping":[{"archetype_element":"unrestricted universal decision demand","domain_realization":"Decide termination and fulfillment safety for every admitted policy and event sequence.","claim_kind":"HYPOTHESIS"},{"archetype_element":"implicit representation and computation model","domain_realization":"Rule expressiveness, queue bounds, event semantics, fairness, and external-service power are unstated.","claim_kind":"HYPOTHESIS"},{"archetype_element":"class-wide constructive or impossibility evidence","domain_realization":"Require either a total correct analyzer for the declared class or a valid reduction establishing its boundary.","claim_kind":"INFERENCE"},{"archetype_element":"decidable regions and weaker honest fallbacks","domain_realization":"Enforce a finite/restricted policy fragment; otherwise return sound warnings, bounded results, or UNKNOWN.","claim_kind":"INFERENCE"},{"archetype_element":"status-preserving operations","domain_realization":"Keep false, unsafe, unknown, timeout, out-of-scope, and system failure distinct in planning interfaces.","claim_kind":"INFERENCE"}],"component_map":[{"component":"Problem-Class Specification","status":"adapted","domain_realization":"Formal class of policies, network states, events, and safety/liveness questions."},{"component":"Instance Representation Contract","status":"adapted","domain_realization":"Grammar, numeric encoding, queue bounds, initial state, and event trace format."},{"component":"Computation Model Contract","status":"adapted","domain_realization":"Machine resources plus declared carrier, supplier, human, sensor, and service capabilities."},{"component":"Solvability Guarantee Profile","status":"direct","domain_realization":"Exact-total, one-sided, bounded, approximate, or relative guarantee per mode."},{"component":"Quantifier and Scope Map","status":"adapted","domain_realization":"Separate one shipment from all policies, networks, and event sequences."},{"component":"Computability Status Lattice","status":"direct","domain_realization":"Classify fragments as decidable, recognizable, relative, unresolved, or undecidable."},{"component":"Constructive Procedure Witness","status":"direct","domain_realization":"Analyzer plus correctness and termination arguments for any decidable fragment."},{"component":"Reduction Preservation Contract","status":"direct","domain_realization":"Total computable source-to-policy encoding preserving the target answer."},{"component":"Computability Impossibility Certificate","status":"direct","domain_realization":"Checked reduction or direct proof for the unrestricted class, if obtainable."},{"component":"Assumption Register","status":"adapted","domain_realization":"Record bounds, fairness, service reliability, policy semantics, and environment assumptions."},{"component":"Decidable Subclass Map","status":"adapted","domain_realization":"Map finite-state, bounded-queue, acyclic, or restricted-rule fragments."},{"component":"One-Sided Recognition Contract","status":"adapted","domain_realization":"Specify which violations or successes have checkable witnesses."},{"component":"Unknown and Nontermination Policy","status":"direct","domain_realization":"Timeout returns UNKNOWN, never an invented safe/unsafe verdict."},{"component":"Fallback Solution Contract","status":"direct","domain_realization":"Route to exact, sound-approximate, bounded, or human-reviewed modes with labels."},{"component":"Computability Guarantee Record","status":"direct","domain_realization":"Versioned statement of shipped scope and guarantee."},{"component":"Recheck Trigger","status":"adapted","domain_realization":"Reclassify after grammar, bounds, environment, or external-capability changes."},{"component":"Termination Condition","status":"adapted","domain_realization":"Explicit analysis budget or finite-state exhaustion criterion."},{"component":"Scope Boundary","status":"direct","domain_realization":"Mechanically enforce admitted fragment and mark all other inputs out-of-scope."},{"component":"Decision Record","status":"direct","domain_realization":"Retain chosen boundary, evidence, fallback, and accountable approver."},{"component":"Uncertainty Residue","status":"direct","domain_realization":"List unproved obligations and unmodeled operational behavior."},{"component":"Independent Proof Review","status":"direct","domain_realization":"Independent check of reductions, termination, correctness, and formal-task fidelity."},{"component":"Complexity Follow-On Gate","status":"adapted","domain_realization":"Only after decidability, assess state explosion and operational feasibility."}],"mechanism_dispositions":[{"slug":"abstract_interpretation_or_model_checking","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Sound finite over-approximation supplies a labeled safety fallback.","counterfactual_removal":"No sound approximate mode remains for policies outside exact analysis."},{"slug":"bounded_domain_exhaustive_search","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Exhaust bounded networks and traces in the pilot.","counterfactual_removal":"Pilot loses complete within-bound evidence."},{"slug":"computability_boundary_decision_record","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Version boundary, guarantee, assumptions, and triggers.","counterfactual_removal":"Guarantees can drift without provenance."},{"slug":"computational_complexity_analysis","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Gate feasibility analysis after solvability classification.","counterfactual_removal":"Decidable but unusable modes may be shipped."},{"slug":"constructive_algorithm_and_correctness_proof","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Required witness for an exact fragment.","counterfactual_removal":"Exact decidability would rest only on examples."},{"slug":"diagonalization_impossibility_proof","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Reject unless the policy semantics support the necessary self-reference; reduction is nearer.","counterfactual_removal":"No change to the proposed evidence path."},{"slug":"enumeration_and_dovetailing","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Unbounded running is operationally inferior to bounded recognition with UNKNOWN.","counterfactual_removal":"No change; bounded protocol remains."},{"slug":"fallback_mode_router","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Dispatch by enforced class to exact, approximate, bounded, or escalation modes.","counterfactual_removal":"Weaker results can be mistaken for universal decisions."},{"slug":"halting_problem_reduction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Attempt only if general computation can be faithfully embedded in policies.","counterfactual_removal":"No decisive impossibility route for the unrestricted claim."},{"slug":"language_fragment_restriction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Define a mechanically enforceable decidable rule fragment.","counterfactual_removal":"Exact guarantees lack a safely policed scope."},{"slug":"many_one_reduction_proof","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Supplies preservation obligations for any impossibility transfer.","counterfactual_removal":"A hardness analogy could replace a valid mapping."},{"slug":"promise_problem_restriction","disposition":"considered_rejected","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Unenforced promises permit authoritative outputs on violating inputs; prefer syntactic enforcement.","counterfactual_removal":"No loss because fragment admission supplies the boundary."},{"slug":"proof_by_counterexample","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Refute current universal claims with any verified in-scope failure.","counterfactual_removal":"The pilot loses a cheap overclaim test."},{"slug":"proof_checking","disposition":"selected_supporting","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Independently check the exact theorem and exposed assumptions.","counterfactual_removal":"Boundary claims depend on author authority."},{"slug":"reduction_direction_checklist","disposition":"selected_supporting","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Gate source-to-target direction, totality, and preservation.","counterfactual_removal":"A reversed reduction could falsely certify impossibility."},{"slug":"semi_decision_with_explicit_unknown","disposition":"selected_load_bearing","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Bound one-sided searches and expose UNKNOWN.","counterfactual_removal":"Timeout may again be collapsed into a Boolean verdict."},{"slug":"theorem_prover_guided_search","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Optional implementation aid; unavailable proof search must not define the boundary.","counterfactual_removal":"Manual checked evidence remains sufficient."},{"slug":"turing_reduction_analysis","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Relative oracle degrees do not answer the immediate shipped-guarantee question.","counterfactual_removal":"No material change to classification or routing."}],"causal_chain":["Specify the policy class, encoding, quantifiers, environment, and computational capabilities.","Seek a total constructive analyzer and a valid impossibility reduction in parallel.","Classify enforceable fragments without converting failed search into impossibility.","Admit exact analysis only where correctness and termination obligations hold.","Route remaining policies to sound approximation, bounded recognition, or accountable escalation.","Expose guarantee labels and UNKNOWN so downstream planning cannot interpret uncertainty as safety.","Recheck when language or operating assumptions change."],"baseline":"Continue using the current analyzer as a universal Boolean service, interpreting completion as authority and timeouts through ad hoc operational rules.","nearest_rival":"Treat the task solely as state-space optimization: add compute, pruning, simulation, and benchmarks without first testing whether the unrestricted total-exact specification is attainable.","authority_safety":{"affected_parties":["policy authors","operators","suppliers and carriers","customers","compliance teams"],"decision_authority":"The platform product owner may authorize only with approval from operations risk and an independent methods reviewer; local operators retain shipment-hold authority.","authorized_first_step":"On a non-production policy corpus, formalize one rule-language version and exhaustively test a bounded fragment while attempting constructive and reduction evidence; compare labeled outputs with the baseline.","excluded_actions":["No autonomous release or cancellation of live shipments","No timeout-to-safe or timeout-to-unsafe coercion","No claim beyond the checked fragment or bound","No reliance on an unmodeled human or service as an oracle"],"halt_rollback":"Halt if the abstraction misses a known concrete behavior, fragment admission is bypassable, labels are lost downstream, or a checked argument fails. Revert to advisory-only output and the existing human approval path."}},"negative_tests":{"strongest_counterevidence":"The deployed language and environment may already be finite, effectively enumerable, and served by a known total correct analyzer; then the problem is complexity or documentation, not computability.","analogy_break":"Logistics policies describe an external stochastic world, not programs in isolation. A halting analogy fails unless event semantics and external actors can be represented and the source-to-target encoding preserves the exact fulfillment property.","failure_condition":"The proposal fails if fragment membership cannot be enforced, the abstraction is unsound, UNKNOWN is consumed as a Boolean, or usable policies overwhelmingly fall outside the admitted region.","problem_falsifier":"A complete formalization shows every admitted policy, queue, event alphabet, horizon, and external response is finitely bounded and a total correct decision procedure already covers the declared class; observed failures are only resource scaling.","intervention_falsifier":"Within the bounded pilot, the mapped router and fragment produce no reduction in mislabeled outcomes or proof obligations versus baseline, or independent review finds that their guarantees do not correspond to real fulfillment safety.","risks":["Over-restricting the language excludes operationally necessary policies.","False alarms from coarse abstraction create alert fatigue.","A formally checked model may omit real carrier, supplier, or human behavior.","Complexity may make a decidable fragment operationally unusable.","Boundary labels may be stripped by downstream systems.","An invalid reduction may prematurely stop useful engineering."]},"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 logistics diagnosis and presence of an unrestricted expressive policy language are hypotheses; the candidate deliberately conditions any undecidability conclusion on formalization and a checked preservation proof."}