{"schema_version":1,"experiment_id":"eoa_inverse_innovation_exp03_full320_20260801","cell_id":"computability_boundary_mapping__archaeology_paleontology","trajectory_id":"R","attempt_index":0,"archetype_slug":"computability_boundary_mapping","domain_slug":"archaeology_paleontology","decision":"CANDIDATE","problem_id":"unbounded_site_formation_reachability_claim","causal_lever_id":"enforceable_model_fragment_and_labeled_fallback","proposal":{"problem":"A proposed archaeology or paleontology modeling service promises to decide, for every formally specified site-formation or taphonomic process model, whether some possible process history can produce an observed assemblage. If the accepted modeling language permits unbounded state, iteration, and conditional transitions, repeated timeouts cannot establish whether the problem is merely expensive or lacks a total exact decider for the declared class. Forced yes/no outputs can consequently turn unresolved reachability into false historical conclusions.","actors_substrate":["archaeologists and paleontologists authoring process models","software and methods teams implementing reachability analysis","curators and project leads relying on reported model consistency","formal transition models of deposition, disturbance, preservation, and observation","observed assemblage and stratigraphic constraints"],"observable_state":"The service accepts an open-ended process language, advertises a terminating exact answer for all accepted models, and reports timeout or failed search as inconsistency; its documentation lacks an enforceable fragment boundary and an UNKNOWN state.","consequence":"Valid models may be rejected after resource exhaustion, or an impossible universal-decider project may consume effort without resolving its specification.","affected_objective":"Produce auditable consistency claims about whether a formal site-formation or taphonomic model can generate specified observations without overstating what the analysis establishes.","structural_mapping":[{"archetype_element":"unrestricted universal analyzer","domain_realization":"A universal reachability analyzer for arbitrary encoded depositional or taphonomic transition models.","claim_kind":"HYPOTHESIS"},{"archetype_element":"implicit problem class and representation","domain_realization":"The accepted model grammar, bounds, observation encoding, and meaning of 'can produce' are not versioned as one contract.","claim_kind":"INFERENCE"},{"archetype_element":"possible undecidability boundary","domain_realization":"An unbounded model language may encode a known-undecidable transition system; this requires an explicit computable reduction and is not established by archaeological complexity alone.","claim_kind":"HYPOTHESIS"},{"archetype_element":"decidable restricted region","domain_realization":"Finite-state or explicitly depth-bounded process models admit terminating exhaustive reachability checks, subject to a complete encoding.","claim_kind":"INFERENCE"},{"archetype_element":"honest weaker fallback","domain_realization":"Out-of-fragment models receive witness-bearing YES or explicit UNKNOWN, never a timeout-derived NO.","claim_kind":"INFERENCE"}],"component_map":[{"component":"Problem-Class Specification","status":"adapted","domain_realization":"Grammar and semantics of accepted site-formation models plus the reachability property."},{"component":"Instance Representation Contract","status":"adapted","domain_realization":"Versioned encoding for states, transitions, observations, bounds, and equivalence."},{"component":"Computation Model Contract","status":"direct","domain_realization":"Machine, allowed memory, external solvers, and certificate checker."},{"component":"Solvability Guarantee Profile","status":"direct","domain_realization":"Exact total decision, one-sided recognition, bounded decision, and UNKNOWN distinguished."},{"component":"Quantifier and Scope Map","status":"direct","domain_realization":"Separates every accepted model from one named model and bounded subclasses."},{"component":"Computability Status Lattice","status":"direct","domain_realization":"Classifies fragments as decidable, recognizable, relative, or unresolved."},{"component":"Constructive Procedure Witness","status":"adapted","domain_realization":"Reachability algorithm with correctness and termination argument for each safe fragment."},{"component":"Reduction Preservation Contract","status":"adapted","domain_realization":"Computable source-to-model translation preserving reachability."},{"component":"Computability Impossibility Certificate","status":"adapted","domain_realization":"Checked reduction from a known-undecidable source if the unrestricted language supports it."},{"component":"Assumption Register","status":"direct","domain_realization":"Expressiveness, encoding, finiteness, and observation-semantics assumptions."},{"component":"Decidable Subclass Map","status":"adapted","domain_realization":"Enforceable finite-state, bounded-depth, and otherwise proven fragments."},{"component":"One-Sided Recognition Contract","status":"direct","domain_realization":"A found execution trace certifies YES; lack of a trace does not certify NO."},{"component":"Unknown and Nontermination Policy","status":"direct","domain_realization":"UNKNOWN, timeout, out-of-fragment, and false are separate states."},{"component":"Fallback Solution Contract","status":"adapted","domain_realization":"Exact within certified fragments; bounded or one-sided outside them."},{"component":"Computability Guarantee Record","status":"direct","domain_realization":"Version-linked claim, proof, checker, and output semantics."},{"component":"Recheck Trigger","status":"adapted","domain_realization":"Any grammar, bound, solver, or external-capability change triggers reclassification."},{"component":"Termination Condition","status":"direct","domain_realization":"Finite state count or declared trace/resource bound."},{"component":"Scope Boundary","status":"direct","domain_realization":"Mechanically checked fragment membership before analysis."},{"component":"Decision Record","status":"direct","domain_realization":"Auditable choice of shipped modes and guarantees."},{"component":"Uncertainty Residue","status":"adapted","domain_realization":"Unproved reduction obligations and unresolved out-of-fragment instances."},{"component":"Independent Proof Review","status":"direct","domain_realization":"Reviewer checks formalization, reduction, and fragment algorithm."},{"component":"Complexity Follow-On Gate","status":"direct","domain_realization":"Decidable fragments proceed to state-space and runtime assessment."}],"mechanism_dispositions":[{"slug":"abstract_interpretation_or_model_checking","disposition":"selected_supporting","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Decide reachability on a finite conservative abstraction; label abstraction-induced uncertainty.","counterfactual_removal":"The fallback would lose a sound finite abstraction route but retain bounded enumeration."},{"slug":"bounded_domain_exhaustive_search","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Enumerate all states or traces inside a declared finite bound.","counterfactual_removal":"No complete terminating verdict would remain for the bounded pilot."},{"slug":"computability_boundary_decision_record","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Version the boundary, shipped guarantee, assumptions, and triggers.","counterfactual_removal":"The mathematical boundary could remain, but guarantee drift would be harder to detect."},{"slug":"computational_complexity_analysis","disposition":"selected_supporting","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Assess state explosion only after decidability is established.","counterfactual_removal":"Correctness survives, but practical viability is ungated."},{"slug":"constructive_algorithm_and_correctness_proof","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Supply totality and correctness arguments for the restricted analyzer.","counterfactual_removal":"The claimed decidable fragment would lack its positive witness."},{"slug":"diagonalization_impossibility_proof","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"A direct self-referential proof is unnecessary if a valid reduction is available.","counterfactual_removal":"No change."},{"slug":"enumeration_and_dovetailing","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Finite trace enumeration plus an explicit resource bound is sufficient for the first test.","counterfactual_removal":"No change to the bounded test."},{"slug":"fallback_mode_router","disposition":"selected_load_bearing","contribution_type":"OPERATIONAL","adaptation_or_rejection":"Route enforceably among exact-fragment, bounded, and UNKNOWN modes with guarantee labels.","counterfactual_removal":"Outputs could inherit guarantees from the wrong analysis mode."},{"slug":"halting_problem_reduction","disposition":"selected_load_bearing","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Attempt a computable, reachability-preserving encoding into the unrestricted model language.","counterfactual_removal":"There would be no valid test of the conjectured undecidability boundary."},{"slug":"language_fragment_restriction","disposition":"selected_load_bearing","contribution_type":"CORE_CAUSAL","adaptation_or_rejection":"Enforce a finite-state or bounded grammar at ingestion.","counterfactual_removal":"The system could not guarantee that exact-mode inputs lie in the decidable region."},{"slug":"many_one_reduction_proof","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Formalize totality, computability, and answer preservation of the proposed reduction.","counterfactual_removal":"The halting reduction would lack a disciplined preservation contract."},{"slug":"promise_problem_restriction","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"A mere caller promise is weaker than mechanically enforced fragment membership.","counterfactual_removal":"No change."},{"slug":"proof_by_counterexample","disposition":"selected_supporting","contribution_type":"TEST_DESIGN","adaptation_or_rejection":"Use one in-scope timeout-to-NO failure to refute an existing universal implementation claim, not to prove undecidability.","counterfactual_removal":"Boundary proofs remain possible, but overclaim detection becomes less direct."},{"slug":"proof_checking","disposition":"selected_supporting","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Independently check the reduction and restricted-fragment proof against the stated semantics.","counterfactual_removal":"A formalization or proof gap could authorize a false guarantee."},{"slug":"reduction_direction_checklist","disposition":"selected_supporting","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Gate any impossibility claim on source-to-target direction and declared assumptions.","counterfactual_removal":"A reversed reduction could be mistaken for an impossibility result."},{"slug":"semi_decision_with_explicit_unknown","disposition":"selected_load_bearing","contribution_type":"SAFETY_GUARDRAIL","adaptation_or_rejection":"Return witness-bearing YES or budget-triggered UNKNOWN outside exact mode.","counterfactual_removal":"Resource exhaustion would again invite a deceptive NO."},{"slug":"theorem_prover_guided_search","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Optional automation is unnecessary for the bounded hand-checkable first test.","counterfactual_removal":"No change to causal validity."},{"slug":"turing_reduction_analysis","disposition":"considered_rejected","contribution_type":"NONE","adaptation_or_rejection":"Relative computability degrees do not answer the required total-decider boundary.","counterfactual_removal":"No change."}],"causal_chain":["Specify the model language, encoding, quantifiers, and exact reachability guarantee.","Test whether unrestricted syntax supports a valid undecidability reduction while constructing total algorithms for enforced fragments.","Route only certified-fragment inputs to exact analysis; route others to bounded or one-sided analysis.","Preserve YES, NO, UNKNOWN, timeout, and out-of-scope labels.","Prevent failed search from becoming a historical inconsistency claim."],"baseline":"Continue universal search under an implicit language boundary and convert timeout or exhausted budget into NO or generic failure.","nearest_rival":"Treat the accepted language as already finite and perform only complexity optimization; this is appropriate if read-only inspection proves every accepted instance effectively bounded.","authority_safety":{"affected_parties":["model authors","field and collections researchers relying on results","institutions preserving or publishing interpretations"],"decision_authority":"The project methods lead and domain custodian jointly authorize output semantics; an independent formal reviewer approves any class-wide guarantee.","authorized_first_step":"On synthetic models only, freeze a small grammar, encode a finite-state fragment and one candidate unbounded extension, prove and exhaustively cross-check the finite analyzer, and attempt one explicit source-to-target reduction. No archaeological interpretation is changed by the pilot.","excluded_actions":["Treating timeout as NO","Claiming the physical past itself is undecidable","Applying a formal verdict to real collections before semantic validation","Discarding records or revising provenance from pilot outputs","Publishing an impossibility claim before independent proof review"],"halt_rollback":"Halt if fragment membership is ambiguous, exhaustive results disagree with the constructive procedure, the reduction lacks total answer preservation, or domain reviewers reject semantic fidelity. Withdraw the class-wide label and retain all affected outputs as UNKNOWN."}},"negative_tests":{"strongest_counterevidence":"If the deployed grammar is demonstrably finite-state or bounded and has a known total reachability algorithm, the problem is complexity and engineering rather than computability; the proposed impossibility branch is then inapplicable.","analogy_break":"Depositional history and fossilization are physical processes, not programs. Computability results attach only to the chosen formal representation and requested guarantee; they cannot establish uniqueness, truth, or recoverability of the actual past from incomplete evidence.","failure_condition":"The mapping fails if the model language cannot express the source reduction, safe-fragment membership is not enforceable, or the abstraction can omit real modeled behaviors while still reporting a definitive NO.","problem_falsifier":"Audit every accepted production input and grammar feature; the diagnosed problem is falsified if all inputs are effectively bounded, output states already distinguish UNKNOWN from NO, and no universal unrestricted guarantee is claimed.","intervention_falsifier":"On a bounded synthetic corpus with an independently enumerated oracle, the intervention is falsified if the exact route misclassifies any instance, fails to terminate, routes an out-of-fragment instance as exact, or labels budget exhaustion as NO.","risks":["A formally correct model may be semantically unfaithful to archaeological practice.","Restricting expressiveness may exclude the process behavior researchers need.","UNKNOWN may be ignored or operationally coerced into NO downstream.","Finite exact analysis may still be computationally infeasible.","An official decision record may entrench an incorrect boundary."]},"null_rationale":null,"classification":{"candidate_kind":"TESTABLE_CONJECTURE","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 the testable hypothesis that the unrestricted domain model language can encode an undecidable reachability source. The packet supplies no evidence that a deployed archaeological system currently has this expressiveness or makes the diagnosed universal claim."}