docs: establish Robodog research programme and BFT comparator

README.adoc

@@ -96,6 +96,8 @@ The repository is organised around a simulation-first safety boundary:
 
 See link:TOPOLOGY.md[TOPOLOGY.md] for the architecture map and completion dashboard.
 
+The research programme is documented in link:docs/programme-plan.adoc[docs/programme-plan.adoc]. Mathematical extensions and their proof ladder are tracked in link:docs/mathematical-agenda.adoc[docs/mathematical-agenda.adoc]. External reports are received through link:docs/incoming-reports.adoc[docs/incoming-reports.adoc]. The educational BFT/type comparator is described in link:docs/bft-type-comparator.adoc[docs/bft-type-comparator.adoc].
+
 == Technology Stack
 
 [cols="1,2,2"]

docs/bft-type-comparator.adoc

@@ -0,0 +1,32 @@
+= BFT and Type-Augmented Design Comparator
+:toc:
+
+== Purpose
+
+`www/index.html` is an educational visualisation prompted by a comparison between Byzantine Fault Tolerance (BFT) and ideas associated with epistemic types, proof transport, echo types, choreographies, and tropical grading.
+
+It is deliberately a *comparator*, not a claim of equivalence. BFT and typed evidence answer different questions:
+
+* BFT: can non-faulty replicas agree despite a specified class of faults, network model, and quorum assumptions?
+* Typed evidence: which states can a component accept, and what machine-checkable evidence accompanies them?
+
+A signature authenticates origin; it does not authenticate truth. A proof term proves only the proposition actually formalised, under the soundness assumptions of its checker, axioms, specifications, and data sources. Typed boundaries therefore complement BFT; they do not remove quorum intersection, liveness, membership, recovery, or a threat model.
+
+== What is grounded here
+
+The repository contains Idris2 ABI declarations, Rust ECM code and tests, and SPARK safety modules. The immediately actionable synthesis is evidence-aware safety boundaries: distinguish measured, inferred, stale, degraded, and rejected inputs, and make unsafe actuator commands unrepresentable or rejected.
+
+The names `epistemic-types`, `echo-types`, `choreographic`, `tropical`, `residual evidence`, `Januskey`, and `Absolute Zero` should be treated as proposed research modules until their repositories expose formal definitions, semantics, soundness claims, and executable tests. The visualisation labels their useful hypotheses without presenting them as established results.
+
+== Suggested progression
+
+. State faults explicitly: crash, omission, equivocation, stale data, malicious sensor, compromised runtime, and unsafe FFI.
+. Define one invariant, for example: `unsafe actuator command => no valid evidence path`.
+. Build a minimal 3f+1 trace and a typed admission trace, including counterexamples.
+. Prove/check the boundary with Idris2, Rust, and SPARK where appropriate.
+. Measure latency, memory, proof-check cost, false rejection, and recovery behaviour.
+. Add named extensions only when each has an operational semantics and a testable contract.
+
+== Limitations
+
+Echo-like witnesses can preserve structured provenance of loss but cannot recover information never received. A choreography can constrain protocol shape but cannot make a compromised runtime honest. Quantitative path costs can make budgets explicit but do not themselves establish safety. These distinctions are the central teaching point.

docs/incoming-reports.adoc

@@ -0,0 +1,58 @@
+= Incoming Research Reports
+:toc:
+
+This is the receiving surface for results from related repositories. Copy the compact hand-off from each project here, then verify every referenced theorem, test, file, and assumption locally before using it in Robodog design.
+
+== Intake rules
+
+. Preserve the submitting repository, revision, date, and exact status.
+. Separate formal proof, executable test, documentation, and speculation.
+. Do not upgrade a result when importing it.
+. Record counterexamples and retractions beside positive results.
+. Link the result to a Robodog issue or experiment.
+. A result is not an implementation requirement until its safety and scope review is complete.
+
+== Required report
+
+[source,yaml]
+----
+repository: hyperpolymath/example
+revision: "commit or tag"
+status: PROVEN | PARTIALLY PROVEN | NOT PROVEN | NOT APPLICABLE
+claim: "one precise claim"
+formal_objects:
+  - "definitions or types"
+proof_or_test_evidence:
+  - file: "path"
+    theorem_or_test: "name"
+    command: "command, if applicable"
+assumptions:
+  - "checker soundness"
+  - "fault/timing/physical model"
+limits:
+  - "what is not established"
+robodog_relevance: direct | indirect | speculative | none
+robodog_integration_proposal:
+  - "concrete type, invariant, test, or experiment"
+robodog_hand_off: "short summary"
+verification:
+  checked_by: "name or handle"
+  checked_on: "YYYY-MM-DD"
+  result: pending | accepted | rejected | needs clarification
+  robodog_issue: "link or identifier"
+----
+
+== Current intake queue
+
+No external research result has yet been accepted into the Robodog safety case. The visual comparator in link:bft-type-comparator.adoc[bft-type-comparator.adoc] is explanatory material, not evidence of a BFT or type-theoretic theorem.
+
+== Standing distinctions
+
+* BFT agreement is not physical truth.
+* Authentication is not correctness.
+* A proof term proves only its declared proposition under its assumptions.
+* An information residue does not recover information never received.
+* A choreography constrains protocol shape; it does not make a runtime honest.
+* A resource bound is not a safety proof.
+* Inverse metadata is not unconditional reversibility.
+* Rejection with no actuator effect is not necessarily total observational nullity.

docs/mathematical-agenda.adoc

@@ -0,0 +1,40 @@
+= Mathematical Agenda
+
+== Highest-value proof ladder
+
+=== 1. Evidence refinement
+
+Define `e₁ ⊑ e₂` when `e₂` is at least as informative as `e₁`. Prove that valid refinement cannot introduce unsupported certainty. This is the common spine for epistemic, residual, and safety-state work.
+
+=== 2. Compatible worlds
+
+Represent an observation by the set of system worlds compatible with it. Prove monotonicity under genuine evidence refinement and exhibit a two-world counterexample where telemetry does not justify a unique action.
+
+=== 3. Agreement versus truth
+
+Keep separate predicates for `AgreesOn(replicas, digest)` and `TrueInWorld(world, claim)`. Document the additional sensor, environment, and model assumptions required to connect them.
+
+=== 4. Typed safety gate
+
+Make actuator admission depend on explicit evidence predicates, not a single trust flag. Test every transition with stale, degraded, conflicting, forged, and missing evidence.
+
+=== 5. Quantitative bounds
+
+Add latency, rounds, trust crossings, evidence-check cost, and recovery cost as separate grades. Prove composition and budget failure without treating a grade as a safety theorem.
+
+=== 6. Null-effect and trace properties
+
+For rejected or quarantined inputs, prove no protected actuator-state change, then enumerate allowed audit, timing, queue, cache, and metrics traces. This is a realistic route into noninterference.
+
+== Why this order
+
+The first four steps clarify semantics and safety before introducing more machinery. They are small enough to produce counterexamples quickly and strong enough to expose whether later Echo, tropical, choreography, residual-evidence, or epistemic claims genuinely apply.
+
+== Minimum artefacts per step
+
+* one definition;
+* one positive theorem or explicit counterexample;
+* one executable test;
+* one named assumption;
+* one statement of what remains unproved;
+* one Robodog integration note.

docs/programme-plan.adoc

@@ -0,0 +1,69 @@
+= Robodog Defensive Systems Lab: Programme Plan
+:toc:
+
+== Mission
+
+Build a simulation-first, defensible safety case for resilient autonomous coordination. The project should make unsafe state transitions difficult to express, easy to reject, and auditable after the fact. It is not an operational ECM, surveillance, weapons, or field-deployment programme.
+
+== Programme questions
+
+. Can a component distinguish observation, inference, agreement, and physical truth?
+. Can degraded or conflicting telemetry cross a safety boundary without being silently upgraded?
+. Can safe-state decisions be checked across Rust, Idris2, SPARK, and FFI boundaries?
+. Can every claimed guarantee state its model, assumptions, evidence, and limits?
+. Can resource, latency, provenance, and recovery budgets fail loudly and locally?
+
+== Workstreams
+
+[cols="1,2,2,2",options="header"]
+|===
+| Workstream | Near-term deliverable | Mathematical question | Primary evidence
+
+| Safety state | Explicit evidence-state algebra and gate | Is admission monotone in valid evidence? | Rust tests + SPARK proof obligations
+| Proof boundary | Claim meanings, receipts, and transport records | What proposition is actually proved? | Idris2 types + checked examples
+| Residual evidence | Compatible-world model for ambiguous telemetry | Does added evidence reduce alternatives? | finite model + Agda hand-off
+| Information residue | Degradation/truncation witness | What loss is known, and what is unrecoverable? | Echo-style finite examples
+| Agreement | Small 3f+1 trace model | Do replicas agree under the declared fault model? | executable fault traces
+| Resource grades | Latency/round/boundary budget | Are worst-case bounds compositional? | benchmark + formal grade
+| Recovery | Evidence-backed rollback and audit states | What is required for reversal? | property tests and crash cases
+| Noninterference | Rejected/quarantined path | What state and trace effects remain? | SPARK/Absolute-Zero style model
+|===
+
+== Phase gates
+
+=== Gate 0: vocabulary and threat model
+
+Define crash, omission, equivocation, stale input, malicious input, compromised runtime, unsafe FFI, and physical-model error. No security claim may proceed without naming its fault model.
+
+=== Gate 1: executable baseline
+
+Implement explicit states: `Measured`, `Inferred`, `Verified`, `Stale`, `Degraded`, `Conflicting`, `Rejected`, and `UnknownProvenance`. Add positive, negative, and fault-injection tests.
+
+=== Gate 2: one cross-language invariant
+
+Select and state one invariant:
+
+[source]
+----
+unsafe actuator command => no valid evidence path exists
+----
+
+Map the invariant across Rust, Idris2, SPARK, and the FFI. Record which layer proves which part.
+
+=== Gate 3: mathematical extensions
+
+Only after Gate 2, add residual-world ordering, Echo residues, tropical grades, choreography, reversibility, or non-disclosure. Each extension needs definitions, a theorem or counterexample, an executable test, and a Robodog adapter note.
+
+=== Gate 4: integrated safety case
+
+Produce a traceable argument from input to decision to safe-state outcome, including degraded communication, contradictory evidence, timeout, crash, and recovery.
+
+== Definition of done for a research claim
+
+A claim is `PROVEN` only when a formal checker or complete stated argument establishes it under named assumptions. `PARTIALLY PROVEN` means some lemmas or cases are established. `NOT PROVEN` is a valid result when a counterexample or missing assumption is identified. “Implemented”, “tested”, and “plausible” are not synonyms for proven.
+
+Every imported result must be recorded in link:incoming-reports.adoc[incoming-reports.adoc].
+
+== Safety and publication boundary
+
+All experiments remain synthetic, defensive, and non-operational. No real RF captures, field deployment guidance, target tracking, intrusion, jamming, or offensive autonomy should be added. See link:../DEFENSIVE-USE.adoc[DEFENSIVE-USE.adoc] and link:../EXPORT-CONTROL.adoc[EXPORT-CONTROL.adoc].