{"schema_version":1,"assessment_id":"eoa_inverse_innovation_exp03_opportunity320_20260801","source_experiment_id":"eoa_inverse_innovation_exp03_full320_20260801","cell_id":"computability_boundary_mapping__robotics_automation","archetype_slug":"computability_boundary_mapping","domain_slug":"robotics_automation","title":"Model-relative collision-verification boundary for robot controllers","opportunity_summary":"Formalize the controller and environment class, distinguish decidable fragments from unresolved unrestricted cases, mechanically enforce fragment admission, and preserve UNKNOWN and scope labels so timeouts or bounded searches cannot become unsupported collision-safety clearances. The opportunity is conditional on confirming that the diagnosed production requirement exists and on establishing a robotics-specific decider, reduction, and sound abstraction.","adopter_authorizer":"The designated robotics safety owner can authorize formal-boundary work and an offline synthetic pilot after independent proof review; the existing safety authority retains deployment clearance.","scores":{"meaningful_impact":{"score":4,"rationale":"Preventing false SAFE labels for collision-capable controllers could materially protect operators and bystanders and avoid wasted verification work, but the packet does not establish how often the diagnosed requirement or mislabeling occurs."},"stakeholder_pull":{"score":3,"rationale":"Safety owners, verification engineers, controller developers, and operators have clear interests in trustworthy labels, but no adopter interviews, demand evidence, or confirmed production instance is supplied."},"incremental_advantage":{"score":4,"rationale":"Compared with timeout-based clearance or thresholded simulation, enforced admission, exact checking where justified, and explicit UNKNOWN labels directly improve guarantee discipline; advantage over established robotics assurance methods is unmeasured."},"distinctiveness_plausibility":{"score":3,"rationale":"The model-relative boundary mapping and guarantee-preserving routing form a coherent proposal, but prior art is explicitly unsearched and overlap with verification, reachability, abstraction, and runtime-assurance practice is unknown."},"technical_implementability":{"score":3,"rationale":"A finite-state synthetic pilot with 20 bounded scenarios is implementable in principle, while the unrestricted reduction, production-class mapping, abstraction relation, and state-space performance remain unresolved."},"adoption_authority_feasibility":{"score":4,"rationale":"The packet identifies a designated safety owner for the offline pilot, preserves existing deployment authority, specifies excluded actions, and defines halt and rollback rules; actual organizational willingness is unknown."},"evidence_readiness":{"score":3,"rationale":"The candidate supplies explicit problem and intervention falsifiers plus a bounded offline comparison, but lacks the decisive formal reduction, constructive decider, abstraction proof, production inventory, and independent review."},"safety_net_benefit":{"score":5,"rationale":"Preserving UNKNOWN, prohibiting timeout-to-SAFE conversion, retaining scope labels, requiring independent proof review, and reverting questionable cases to manual safety review create strong safeguards without robot actuation."},"scalability":{"score":3,"rationale":"Mechanical fragment admission and routing could be reused across controllers, but restrictive fragments, model maintenance, proof obligations, bypass incentives, and state-space explosion may substantially limit expansion."}},"score_confidence":"MODERATE","costs":{"first_evidence":{"band_2026_usd":"50K_TO_250K","scope":"Inventory one target controller class, formalize a finite-state fragment, build mechanical admission checks, evaluate 20 synthetic bounded scenarios against exact enumeration and abstraction or UNKNOWN outputs, audit labels, and obtain independent proof review.","confidence":"MODERATE","assumptions":["The work remains offline and non-actuating.","Existing modeling and verification software can be adapted rather than built from scratch.","The 20 scenarios and finite fragment do not require proprietary data acquisition or new robot hardware.","The estimate includes formal-methods labor, robotics review, evaluation, and coordination."]},"initial_deployment_startup":{"band_2026_usd":"250K_TO_1M","scope":"Translate validated boundary logic into one production-adjacent verification workflow, integrate admission and guarantee-label routing, document the assurance case, validate the abstraction against representative models, and train reviewers without granting deployment clearance.","confidence":"LOW","assumptions":["One controller language and one robot or environment family are in scope.","Existing safety interlocks and approval processes remain unchanged.","No unrestricted-class guarantee is claimed without an accepted proof.","Tool qualification and integration requirements are moderate rather than certification-program scale."]},"operational_launch":{"band_2026_usd":"1M_TO_5M","scope":"Launch a governed production verification service across an initial robotics program, including tool hardening, model governance, safety-case integration, independent validation, access controls, monitoring, training, and change-management procedures.","confidence":"LOW","assumptions":["Launch spans multiple controller versions but not an enterprise-wide heterogeneous fleet.","Formal models and trace interfaces require substantial engineering.","Existing safety authority supplies the final clearance process.","Physical certification, major hardware redesign, and broad regulatory approval are outside this band."]},"annual_recurring":{"band_2026_usd":"250K_TO_1M","scope":"Maintain semantics, fragment definitions, abstractions, proof artifacts, label provenance, regression suites, reviewer capacity, and reclassification after controller, environment, or external-capability changes.","confidence":"LOW","assumptions":["A small specialist team supports one initial robotics program.","Model and controller changes occur regularly but are not continuous across a large fleet.","Recurring work includes independent audits and regression evaluation.","Major new language support or hardware redesign would be separately funded."]}},"research_burden":"HIGH","earliest_credible_horizon":"3_TO_12_MONTHS","pipeline_gates":{"recognizable_externally_supportable_problem":{"status":"UNCERTAIN","reason":"The packet clearly defines timeout-based overclaiming and overbroad impossibility claims, but explicitly treats their occurrence in production as a hypothesis and supplies no prevalence or adopter evidence."},"identifiable_adopter_or_authorizer":{"status":"YES","reason":"The designated robotics safety owner is identified as the offline-pilot authorizer after independent proof review, while existing safety authority retains deployment clearance."},"distinct_testable_incremental_claim":{"status":"YES","reason":"The proposal claims that enforced fragment admission, matched checking, and preserved UNKNOWN and scope labels prevent unsupported safety clearances; exact enumeration, admission errors, and abstraction false-SAFE outputs provide direct tests."},"bounded_next_evidence_step":{"status":"YES","reason":"The authorized step is limited to one finite-state fragment and 20 bounded, synthetic, non-actuating scenarios, with exact exhaustive results as the comparison and explicit falsifiers."},"no_unresolved_safety_or_authority_stop":{"status":"YES","reason":"The first step prohibits actuation and deployment clearance, preserves safety authority, excludes timeout-to-SAFE conversion, and specifies halt and rollback conditions for admission, labeling, and proof failures."},"implementation_cost_scope_and_range":{"status":"UNCERTAIN","reason":"The packet bounds the offline pilot but does not specify production system complexity, certification obligations, existing tooling, staffing, fleet diversity, or integration scope sufficiently to support a confident launch-cost range."}},"blocking_evidence":["Whether production requirements actually demand a total correct verifier over arbitrary controllers, unbounded executions, and admissible traces.","A mechanically checked inventory showing whether deployed controller and environment inputs are already an enforceable finite, effectively enumerable class.","An instantiated answer-preserving reduction for the unrestricted class or a constructive total decider for the restricted class, with independent review.","A demonstrated simulation or over-approximation relation showing that the proposed abstraction cannot label a feasible modeled collision SAFE.","Evidence that fragment membership and guarantee labels remain enforced through production routing and organizational handoffs.","Scoped prior-art evidence establishing overlap or incremental advantage relative to existing robotics verification and assurance methods.","Operational evidence on state-space growth and the proportion of representative controllers admitted to a useful fragment."],"next_evidence_step":"On synthetic non-actuating models, formalize one finite-state controller fragment and 20 bounded scenarios; mechanically test fragment admission, compare exact exhaustive collision results with the proposed abstraction and UNKNOWN routing, audit every scope label, and falsify the intervention if any known collision is labeled SAFE, any out-of-fragment case receives an exact guarantee, or independent review rejects the formal artifact.","research_questions":["What controller language, numerical semantics, state bounds, trace horizons, environment nondeterminism, and external capabilities are actually admitted in production?","Does the production requirement truly quantify over unrestricted programs and unbounded traces, or is it a finite reachability problem whose primary barrier is complexity?","Can a checked reduction preserve collision reachability in both directions for the declared unrestricted robot and environment semantics?","Which finite or otherwise decidable fragments can be mechanically recognized, and what share of representative controllers would they admit?","What verified relation makes the abstraction sound with respect to concrete modeled behaviors, and which physical faults remain outside its scope?","How quickly does exact checking become operationally unusable as controller, plant, and environment state grow?","Can guarantee scope and UNKNOWN labels survive integrations, reports, safety cases, and later model changes without being stripped or misinterpreted?","What prior methods already provide controller restrictions, reachability analysis, abstraction-based verification, runtime assurance, or scoped guarantee labeling?","Which safety owner would sponsor the work, and what evidence would the existing deployment authority require beyond the offline pilot?"],"recommendation":"PARTNERED_RESEARCH","uncertainty_constraints":["Problem prevalence, stakeholder demand, realized impact, and market size are not established in the sealed packet.","World novelty and comparative advantage are unmeasured because prior art is unsearched.","The computability diagnosis applies only to a precisely declared unrestricted formal class, not automatically to bounded physical robots or missions.","Safety conclusions remain relative to encoded robot, environment, sensor, and collision semantics and exclude omitted physical or human-interaction failure modes.","Cost bands are resource-equivalent planning ranges, not vendor quotes, and are especially sensitive to certification, tool qualification, fleet diversity, and existing infrastructure.","No pilot result authorizes robot actuation, deployment clearance, or generalization beyond the encoded fragment and bound."],"closed_book_prior_art_boundary":"No external search was performed. The packet explicitly reports prior art as unsearched; therefore this assessment makes no claim about novelty, prevalence, market size, realized impact, or the existence and performance of comparable robotics-verification systems."}