From 63c99d94a584e04099a1c31d1f8de899b3ddd2ad Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:04:27 +0000
Subject: [PATCH 01/17] docs(proofs): record safe Agda and cross-kernel
 reconciliation contract

---
 docs/PROOF-RECONCILIATION.adoc | 40 ++++++++++++++++++++++++++++++++++
 1 file changed, 40 insertions(+)
 create mode 100644 docs/PROOF-RECONCILIATION.adoc

diff --git a/docs/PROOF-RECONCILIATION.adoc b/docs/PROOF-RECONCILIATION.adoc
new file mode 100644
index 0000000..96a6e53
--- /dev/null
+++ b/docs/PROOF-RECONCILIATION.adoc
@@ -0,0 +1,40 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Proof Reconciliation Receipts
+:toc:
+
+Proof Burrower discovers candidate proof locations and can ask ECHIDNA to
+run a prover; neither a search hit nor a proposed tactic establishes that
+a theory theorem has been checked.
+
+Estate policy: https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[Proof and Verification Policy].
+
+== Interim theory reconciliation
+
+The canonical primary checker invocation is:
+
+[source,bash]
+----
+agda --safe --without-K --cubical-compatible path/to/Theorem.agda
+----
+
+Record each original proof and Agda conversion or re-proof, its stable
+theorem identity, source and target digests, checker version and exact
+command, assumptions, kernel result, and CI execution evidence.
+
+Rocq/Coq and Lean are distinct recheck legs. A transported witness is not
+independent evidence until the target kernel accepts it and the source and
+target statements (and assumptions) are compared. A fresh re-proof is a
+valid fallback, with the statement comparison recorded. Preserve all
+prior evidence on unsuccessful conversion; a translation failure never
+refutes a theorem.
+
+Proof status remains the estate's canonical closed vocabulary:
+`proven`, `proven-with-postulates`, `tested-only`, `argued`,
+`open`. The route and execution state of an individual leg are
+separate metadata, not new global status tokens.
+
+A checker that was not invoked is `open` (unavailable), not `proven`.
+Current Burrower attempts use Isabelle; they do not claim to run the
+Agda/Rocq/Lean reconciliation pipeline. ECHIDNA will eventually
+coordinate the full process; this record is an interim evidence format,
+not a second proof engine.

From b14ccc99eb41852ada98b1d01d247831a1ff2c7d Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:05:27 +0000
Subject: [PATCH 02/17] feat(proofs): validate reconciliation evidence without
 promoting unverified results

---
 crates/burrower-core/src/reconciliation.rs | 311 +++++++++++++++++++++
 1 file changed, 311 insertions(+)
 create mode 100644 crates/burrower-core/src/reconciliation.rs

diff --git a/crates/burrower-core/src/reconciliation.rs b/crates/burrower-core/src/reconciliation.rs
new file mode 100644
index 0000000..77ee8c8
--- /dev/null
+++ b/crates/burrower-core/src/reconciliation.rs
@@ -0,0 +1,311 @@
+// SPDX-License-Identifier: MPL-2.0
+//! Typed *evidence claims* for the interim Agda -> Rocq/Coq and Lean
+//! reconciliation process. Validating this document does NOT run a checker,
+//! verify a signature or authenticate a CI receipt. Do not treat it as a
+//! kernel-level proof; only the cited checker runs can establish that.
+use crate::ledger::{goal_hash, new_id, now_iso, Ledger, LedgerRecord, RecordResult};
+use anyhow::Result;
+use serde::{Deserialize, Serialize};
+
+pub const RECONCILIATION_SCHEMA: &str = "proof.reconciliation/1";
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "snake_case")]
+pub enum Checker {
+    Agda,
+    Rocq,
+    Lean,
+}
+
+/// These describe a single leg; they do not replace the estate's closed
+/// proof-ledger status vocabulary (proven/argued/open/etc.).
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "snake_case")]
+pub enum LegOutcome {
+    Open,
+    Unavailable,
+    Failed,
+    Checked,
+    CheckedWithAxioms,
+}
+
+impl LegOutcome {
+    fn checked(self) -> bool {
+        matches!(self, Self::Checked | Self::CheckedWithAxioms)
+    }
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "snake_case")]
+pub enum Route {
+    OriginalAgda,
+    Converted,
+    Reproved,
+    Transported,
+}
+
+#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)]
+#[serde(rename_all = "snake_case")]
+pub enum Correspondence {
+    /// Source/target propositions and assumptions were compared.
+    Verified,
+    /// No comparison established; a transported accepted term is insufficient.
+    Unchecked,
+    /// Only appropriate for the Agda source leg.
+    NotApplicable,
+}
+
+/// A claim about a real checker run, rather than a proof-checking operation.
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+pub struct CheckLeg {
+    pub checker: Checker,
+    pub route: Route,
+    pub outcome: LegOutcome,
+    pub artifact_path: Option<String>,
+    /// SHA-256 digest of the checked source or witness.
+    pub artifact_sha256: Option<String>,
+    pub checker_version: Option<String>,
+    pub invocation: Option<String>,
+    /// Immutable CI run URL, local signed execution receipt, or equivalent.
+    pub run_ref: Option<String>,
+    pub correspondence: Correspondence,
+    #[serde(default)]
+    pub axioms: Vec<String>,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+pub struct OriginalProof {
+    pub language: String,
+    pub path: String,
+    pub sha256: String,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
+pub struct ProofReconciliation {
+    pub schema: String,
+    pub theorem_id: String,
+    pub original: OriginalProof,
+    pub agda: CheckLeg,
+    pub rocq: CheckLeg,
+    pub lean: CheckLeg,
+}
+
+fn filled(s: &Option<String>) -> bool {
+    s.as_deref().is_some_and(|v| !v.trim().is_empty())
+}
+
+fn sha256(s: &str) -> bool {
+    s.len() == 64 && s.bytes().all(|b| b.is_ascii_hexdigit())
+}
+
+impl ProofReconciliation {
+    /// Reject contradictory or under-specified evidence metadata.
+    ///
+    /// A successful validation is NOT a checked proof; callers must still
+    /// authenticate the run references and check the referenced artefacts.
+    pub fn validate(&self) -> std::result::Result<(), String> {
+        if self.schema != RECONCILIATION_SCHEMA {
+            return Err("unsupported reconciliation schema".into());
+        }
+        if self.theorem_id.trim().is_empty()
+            || self.original.language.trim().is_empty()
+            || self.original.path.trim().is_empty()
+            || !sha256(&self.original.sha256)
+        {
+            return Err("theorem identity or original proof provenance missing".into());
+        }
+        for (expected, leg) in [
+            (Checker::Agda, &self.agda),
+            (Checker::Rocq, &self.rocq),
+            (Checker::Lean, &self.lean),
+        ] {
+            if leg.checker != expected {
+                return Err(format!("leg checker mismatch: expected {expected:?}"));
+            }
+            let source_leg = expected == Checker::Agda;
+            let valid_route = if source_leg {
+                matches!(leg.route, Route::OriginalAgda | Route::Converted | Route::Reproved)
+            } else {
+                matches!(leg.route, Route::Transported | Route::Reproved)
+            };
+            if !valid_route {
+                return Err(format!("invalid {expected:?} reconciliation route"));
+            }
+            if leg.outcome.checked() {
+                if !filled(&leg.artifact_path)
+                    || !leg.artifact_sha256.as_deref().is_some_and(sha256)
+                    || !filled(&leg.checker_version)
+                    || !filled(&leg.invocation)
+                    || !filled(&leg.run_ref)
+                {
+                    return Err(format!("checked {expected:?} leg lacks run evidence"));
+                }
+                if !source_leg && leg.correspondence != Correspondence::Verified {
+                    return Err(format!(
+                        "checked {expected:?} target lacks statement/assumptions comparison"
+                    ));
+                }
+                if source_leg && leg.correspondence != Correspondence::NotApplicable {
+                    return Err("Agda source leg must not claim a cross-prover comparison".into());
+                }
+                if leg.outcome == LegOutcome::Checked && !leg.axioms.is_empty() {
+                    return Err(format!("unchecked axioms in {expected:?} no-axiom claim"));
+                }
+                if leg.outcome == LegOutcome::CheckedWithAxioms && leg.axioms.is_empty() {
+                    return Err(format!("{expected:?} axiomatic claim names no axioms"));
+                }
+                if source_leg {
+                    // The canonical policy requires this exact command-line option set.
+                    // A shell line is metadata only: it must be backed by run_ref.
+                    let words: Vec<&str> = leg
+                        .invocation
+                        .as_deref()
+                        .unwrap_or_default()
+                        .split_whitespace()
+                        .collect();
+                    if words.len() < 5
+                        || !words[0].rsplit('/').next().is_some_and(|cmd| cmd == "agda")
+                        || words[1..4] != ["--safe", "--without-K", "--cubical-compatible"]
+                    {
+                        return Err("Agda check missing canonical safe flags".into());
+                    }
+                }
+            } else if leg.correspondence == Correspondence::Verified && !source_leg {
+                return Err(format!("unchecked {expected:?} leg claims verified correspondence"));
+            }
+        }
+        Ok(())
+    }
+}
+
+/// Append the *claim* to Burrower's existing interim JSONL ledger. The
+/// status remains "proposed": an imported receipt is not proof of execution.
+/// No second persistent database or new state store is introduced.
+pub fn record_reconciliation(
+    ledger: &Ledger,
+    theorem_statement: &str,
+    receipt: &ProofReconciliation,
+) -> Result<()> {
+    receipt.validate().map_err(anyhow::Error::msg)?;
+    ledger.append(&LedgerRecord {
+        id: new_id(),
+        timestamp: now_iso(),
+        goal_hash: goal_hash(theorem_statement),
+        goal_id: Some(crate::ids::goal_content_id(theorem_statement)),
+        goal_excerpt: theorem_statement.chars().take(200).collect(),
+        specialist: "ProofReconciliation".to_string(),
+        approach: None,
+        result: Some(RecordResult {
+            status: "proposed".to_string(),
+            explanation: "Reconciliation evidence submitted; checker runs not authenticated by Burrower".into(),
+            artifacts: Vec::new(),
+        }),
+        learning: None,
+        extra: serde_json::json!({"proof_reconciliation": receipt}),
+    })
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use tempfile::tempdir;
+
+    const DIGEST: &str =
+        "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef";
+
+    fn checked(checker: Checker, route: Route, invocation: &str) -> CheckLeg {
+        CheckLeg {
+            checker,
+            route,
+            outcome: LegOutcome::Checked,
+            artifact_path: Some("verification/theorem".into()),
+            artifact_sha256: Some(DIGEST.into()),
+            checker_version: Some("pinned-1.0".into()),
+            invocation: Some(invocation.into()),
+            run_ref: Some("https://github.com/hyperpolymath/proof-burrower/actions/runs/1".into()),
+            correspondence: if checker == Checker::Agda {
+                Correspondence::NotApplicable
+            } else {
+                Correspondence::Verified
+            },
+            axioms: Vec::new(),
+        }
+    }
+
+    fn valid() -> ProofReconciliation {
+        ProofReconciliation {
+            schema: RECONCILIATION_SCHEMA.into(),
+            theorem_id: "theory/example/theorem1".into(),
+            original: OriginalProof {
+                language: "Idris2".into(),
+                path: "verification/theorem.idr".into(),
+                sha256: DIGEST.into(),
+            },
+            agda: checked(
+                Checker::Agda,
+                Route::Reproved,
+                "agda --safe --without-K --cubical-compatible verification/Theorem.agda",
+            ),
+            rocq: checked(Checker::Rocq, Route::Reproved, "rocq c theorem.v"),
+            lean: checked(Checker::Lean, Route::Reproved, "lake env lean Theorem.lean"),
+        }
+    }
+
+    #[test]
+    fn honest_record_roundtrip() {
+        let record = valid();
+        assert_eq!(record.validate(), Ok(()));
+        let roundtrip: ProofReconciliation =
+            serde_json::from_str(&serde_json::to_string(&record).unwrap()).unwrap();
+        assert_eq!(roundtrip, record);
+    }
+
+    #[test]
+    fn cannot_promote_uncompared_transport() {
+        let mut r = valid();
+        r.lean.route = Route::Transported;
+        r.lean.correspondence = Correspondence::Unchecked;
+        assert!(r.validate().is_err());
+    }
+
+    #[test]
+    fn cannot_hide_unsafe_agda_invocation() {
+        let mut r = valid();
+        r.agda.invocation = Some("agda --safe --without-K theorem.agda".into());
+        assert!(r.validate().is_err());
+    }
+
+    #[test]
+    fn cannot_promote_unattributed_result_or_axioms() {
+        let mut r = valid();
+        r.rocq.run_ref = None;
+        assert!(r.validate().is_err());
+        r = valid();
+        r.lean.axioms.push("classical_choice".into());
+        assert!(r.validate().is_err());
+        r.lean.outcome = LegOutcome::CheckedWithAxioms;
+        assert_eq!(r.validate(), Ok(()));
+    }
+
+    #[test]
+    fn unavailable_checker_is_not_a_success() {
+        let mut r = valid();
+        r.rocq.outcome = LegOutcome::Unavailable;
+        r.rocq.correspondence = Correspondence::Unchecked;
+        assert_eq!(r.validate(), Ok(()));
+    }
+
+    #[test]
+    fn persistence_never_claims_proven_without_external_check() {
+        let tmp = tempdir().unwrap();
+        let ledger = Ledger::open(tmp.path().join("ledger.jsonl")).unwrap();
+        record_reconciliation(&ledger, "Theorem1", &valid()).unwrap();
+        let rows = ledger.read_all().unwrap();
+        assert_eq!(rows.len(), 1);
+        assert_eq!(rows[0].result.as_ref().unwrap().status, "proposed");
+        assert_eq!(
+            rows[0].extra["proof_reconciliation"]["schema"],
+            RECONCILIATION_SCHEMA
+        );
+    }
+}

From bb8e80a1a78c5bd679805f05f18d584389a2dab8 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:05:29 +0000
Subject: [PATCH 03/17] feat(proofs): export typed reconciliation ledger API

---
 crates/burrower-core/src/lib.rs | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/crates/burrower-core/src/lib.rs b/crates/burrower-core/src/lib.rs
index 4d1db1b..29e6dc8 100644
--- a/crates/burrower-core/src/lib.rs
+++ b/crates/burrower-core/src/lib.rs
@@ -34,6 +34,7 @@ pub mod ids;
 pub mod ledger;
 pub mod oracle;
 pub mod ranking;
+pub mod reconciliation;
 pub mod serve;
 pub mod specialist;
 
@@ -49,6 +50,7 @@ pub use ledger::{
     RecordResult,
 };
 pub use ranking::{rank, Home};
+pub use reconciliation::{record_reconciliation, CheckLeg, Checker, Correspondence, LegOutcome, OriginalProof, ProofReconciliation, Route, RECONCILIATION_SCHEMA};
 pub use specialist::{
     Algebraist, Combinatorialist, ConsensusHome, OrderTheorist, Reading, Specialist, Swarm,
     Synthesis,

From 493290ceffcc799f251671dc48cf800ea6a8a495 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:06:47 +0000
Subject: [PATCH 04/17] test(proofs): establish fail-closed canonical Agda
 invocation

---
 scripts/agda-safe-check.sh | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 scripts/agda-safe-check.sh

diff --git a/scripts/agda-safe-check.sh b/scripts/agda-safe-check.sh
new file mode 100644
index 0000000..3600947
--- /dev/null
+++ b/scripts/agda-safe-check.sh
@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# First-party Agda theory checks must use the exact safety option set.
+set -euo pipefail
+if (( $# == 0 )); then
+  echo "usage: $0 FILE.agda [FILE.agda ...]" >&2
+  exit 2
+fi
+agda_bin="${AGDA_BIN:-agda}"
+if ! command -v "$agda_bin" >/dev/null 2>&1; then
+  echo "Agda checker unavailable: $agda_bin" >&2
+  exit 127
+fi
+"$agda_bin" --version >&2
+for source in "$@"; do
+  if [[ "$source" == -* || "$source" != *.agda || ! -f "$source" ]]; then
+    echo "Not a readable Agda source (options forbidden): $source" >&2
+    exit 2
+  fi
+  "$agda_bin" --safe --without-K --cubical-compatible "$source"
+done

From 34f856a2d4797f7d108a9e0db03b964fb77afa98 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:06:50 +0000
Subject: [PATCH 05/17] test(proofs): establish fail-closed canonical Agda
 invocation

---
 tests/agda-safe-check.sh | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 tests/agda-safe-check.sh

diff --git a/tests/agda-safe-check.sh b/tests/agda-safe-check.sh
new file mode 100644
index 0000000..275128d
--- /dev/null
+++ b/tests/agda-safe-check.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+set -euo pipefail
+root="$(cd "$(dirname "$0")/.." && pwd)"
+tmp="$(mktemp -d)"
+trap 'rm -rf "$tmp"' EXIT
+printf 'module Test where\n' > "$tmp/Test.agda"
+cat > "$tmp/fake-agda" <<'SH'
+#!/usr/bin/env bash
+set -euo pipefail
+if [[ "${1:-}" == --version ]]; then
+  echo "Agda version 2.8.0"
+else
+  printf '%s\n' "$@" > "$AGDA_CAPTURE"
+fi
+SH
+chmod +x "$tmp/fake-agda"
+AGDA_BIN="$tmp/fake-agda" AGDA_CAPTURE="$tmp/capture" \
+  bash "$root/scripts/agda-safe-check.sh" "$tmp/Test.agda"
+mapfile -t args < "$tmp/capture"
+[[ "${#args[@]}" -eq 4 && "${args[0]}" == --safe &&
+   "${args[1]}" == --without-K && "${args[2]}" == --cubical-compatible &&
+   "${args[3]}" == "$tmp/Test.agda" ]]
+if AGDA_BIN="$tmp/fake-agda" AGDA_CAPTURE="$tmp/capture" \
+  bash "$root/scripts/agda-safe-check.sh" --with-K; then
+  echo "unsafe option incorrectly accepted" >&2; exit 1
+fi
+if AGDA_BIN="$tmp/not-installed" \
+  bash "$root/scripts/agda-safe-check.sh" "$tmp/Test.agda"; then
+  echo "missing checker incorrectly accepted" >&2; exit 1
+fi
+echo 'Agda flags positive and negative controls passed'

From 0a1dbcf5235786287ffc3ff4b06c8f2cdb0c75ba Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:08:43 +0000
Subject: [PATCH 06/17] feat(proofs): expose reconciliation evidence ingestion
 via Burrower CLI

---
 crates/burrower-cli/src/main.rs | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

diff --git a/crates/burrower-cli/src/main.rs b/crates/burrower-cli/src/main.rs
index e17f8e1..26e77eb 100644
--- a/crates/burrower-cli/src/main.rs
+++ b/crates/burrower-cli/src/main.rs
@@ -11,7 +11,7 @@
 //!   given a goal, return ranked candidate "homes".
 
 use anyhow::Result;
-use burrower_core::{parse_goal, rank, Corpus, Ledger, ProverConfig, Swarm};
+use burrower_core::{parse_goal, rank, record_reconciliation, Corpus, Ledger, ProofReconciliation, ProverConfig, Swarm};
 use clap::{Parser, Subcommand};
 use std::path::PathBuf;
 
@@ -122,6 +122,18 @@ enum Cmd {
         #[arg(long, default_value = "julia")]
         oracle_julia: PathBuf,
     },
+    /// Record a reconciliation receipt as UNVERIFIED evidence, not a proof.
+    Reconcile {
+        /// JSON file with the proof.reconciliation/1 receipt.
+        #[arg(long)]
+        receipt: PathBuf,
+        /// Original theorem statement for ledger identity.
+        #[arg(long)]
+        goal: String,
+        /// Existing interim Burrow Ledger (JSONL).
+        #[arg(long)]
+        ledger: PathBuf,
+    },
     /// Burrow Ledger inspection.
     Ledger {
         #[command(subcommand)]
@@ -401,6 +413,14 @@ fn main() -> Result<()> {
                 oracle_julia,
             )
         }
+        Cmd::Reconcile { receipt, goal, ledger } => {
+            let body = std::fs::read_to_string(&receipt)?;
+            let evidence: ProofReconciliation = serde_json::from_str(&body)?;
+            let ledger = Ledger::open(&ledger)?;
+            record_reconciliation(&ledger, &goal, &evidence)?;
+            eprintln!("reconciliation evidence recorded as proposed, NOT verified");
+            return Ok(());
+        }
         Cmd::Ledger { sub } => return handle_ledger(sub),
         Cmd::Serve { socket } => return burrower_core::serve::run(socket),
         Cmd::Index { root, output } => {

From cd620e4cbdb36205b36f56fe3e480a481c2a5fe8 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:08:58 +0000
Subject: [PATCH 07/17] docs(proofs): document reconciliation CLI and
 executable Agda check

---
 docs/PROOF-RECONCILIATION.adoc | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/docs/PROOF-RECONCILIATION.adoc b/docs/PROOF-RECONCILIATION.adoc
index 96a6e53..6fcd260 100644
--- a/docs/PROOF-RECONCILIATION.adoc
+++ b/docs/PROOF-RECONCILIATION.adoc
@@ -38,3 +38,36 @@ Current Burrower attempts use Isabelle; they do not claim to run the
 Agda/Rocq/Lean reconciliation pipeline. ECHIDNA will eventually
 coordinate the full process; this record is an interim evidence format,
 not a second proof engine.
+
+== Recording a reconciliation claim
+
+The first consumer is a typed evidence claim, not an automatic checker.
+Its schema identifier is `proof.reconciliation/1`. To ingest an existing
+JSON receipt (with source/target SHA-256 digests, checker versions, run
+references, and the Agda, Rocq and Lean legs), run:
+
+[source,bash]
+----
+cargo run --locked -p burrower -- reconcile \
+  --receipt path/to/receipt.json \
+  --goal 'the original theorem statement' \
+  --ledger path/to/burrow-ledger.jsonl
+----
+
+The CLI validates the metadata shape and consistency and appends a record
+with status `proposed`. The caller remains responsible for authenticating
+checker executions and comparing statements and assumptions. Do not elevate
+this receipt to `proven` merely because the CLI accepted it.
+
+To check an Agda source with the mandated flags:
+
+[source,bash]
+----
+bash scripts/agda-safe-check.sh verification/proofs/agda/Properties.agda
+bash tests/agda-safe-check.sh
+----
+
+The second command tests the *wrapper* with an artificial checker and
+negative controls; it does not prove Properties.agda. The first command
+requires a real Agda binary and suitable installed libraries and fails
+closed if either is missing or incompatible.

From 87ae9a9033176f61ffde6ee3dc9be94764fdfef3 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:51:13 +0000
Subject: [PATCH 08/17] style(proofs): rustfmt reconciliation code for CI

---
 crates/burrower-cli/src/main.rs | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/crates/burrower-cli/src/main.rs b/crates/burrower-cli/src/main.rs
index 26e77eb..55b3f43 100644
--- a/crates/burrower-cli/src/main.rs
+++ b/crates/burrower-cli/src/main.rs
@@ -11,7 +11,10 @@
 //!   given a goal, return ranked candidate "homes".
 
 use anyhow::Result;
-use burrower_core::{parse_goal, rank, record_reconciliation, Corpus, Ledger, ProofReconciliation, ProverConfig, Swarm};
+use burrower_core::{
+    parse_goal, rank, record_reconciliation, Corpus, Ledger, ProofReconciliation, ProverConfig,
+    Swarm,
+};
 use clap::{Parser, Subcommand};
 use std::path::PathBuf;
 
@@ -413,7 +416,11 @@ fn main() -> Result<()> {
                 oracle_julia,
             )
         }
-        Cmd::Reconcile { receipt, goal, ledger } => {
+        Cmd::Reconcile {
+            receipt,
+            goal,
+            ledger,
+        } => {
             let body = std::fs::read_to_string(&receipt)?;
             let evidence: ProofReconciliation = serde_json::from_str(&body)?;
             let ledger = Ledger::open(&ledger)?;

From 7b4b05fc577c5e4d949d7de9c78c2a7b59e47601 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:51:16 +0000
Subject: [PATCH 09/17] style(proofs): rustfmt reconciliation code for CI

---
 crates/burrower-core/src/lib.rs | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/crates/burrower-core/src/lib.rs b/crates/burrower-core/src/lib.rs
index 29e6dc8..c51b877 100644
--- a/crates/burrower-core/src/lib.rs
+++ b/crates/burrower-core/src/lib.rs
@@ -50,7 +50,10 @@ pub use ledger::{
     RecordResult,
 };
 pub use ranking::{rank, Home};
-pub use reconciliation::{record_reconciliation, CheckLeg, Checker, Correspondence, LegOutcome, OriginalProof, ProofReconciliation, Route, RECONCILIATION_SCHEMA};
+pub use reconciliation::{
+    record_reconciliation, CheckLeg, Checker, Correspondence, LegOutcome, OriginalProof,
+    ProofReconciliation, Route, RECONCILIATION_SCHEMA,
+};
 pub use specialist::{
     Algebraist, Combinatorialist, ConsensusHome, OrderTheorist, Reading, Specialist, Swarm,
     Synthesis,

From 20b84fdb3469bf84a83ad5eec27d25c6967b98de Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:51:19 +0000
Subject: [PATCH 10/17] style(proofs): rustfmt reconciliation code for CI

---
 crates/burrower-core/src/reconciliation.rs | 16 +++++++++++-----
 1 file changed, 11 insertions(+), 5 deletions(-)

diff --git a/crates/burrower-core/src/reconciliation.rs b/crates/burrower-core/src/reconciliation.rs
index 77ee8c8..e4df007 100644
--- a/crates/burrower-core/src/reconciliation.rs
+++ b/crates/burrower-core/src/reconciliation.rs
@@ -124,7 +124,10 @@ impl ProofReconciliation {
             }
             let source_leg = expected == Checker::Agda;
             let valid_route = if source_leg {
-                matches!(leg.route, Route::OriginalAgda | Route::Converted | Route::Reproved)
+                matches!(
+                    leg.route,
+                    Route::OriginalAgda | Route::Converted | Route::Reproved
+                )
             } else {
                 matches!(leg.route, Route::Transported | Route::Reproved)
             };
@@ -171,7 +174,9 @@ impl ProofReconciliation {
                     }
                 }
             } else if leg.correspondence == Correspondence::Verified && !source_leg {
-                return Err(format!("unchecked {expected:?} leg claims verified correspondence"));
+                return Err(format!(
+                    "unchecked {expected:?} leg claims verified correspondence"
+                ));
             }
         }
         Ok(())
@@ -197,7 +202,9 @@ pub fn record_reconciliation(
         approach: None,
         result: Some(RecordResult {
             status: "proposed".to_string(),
-            explanation: "Reconciliation evidence submitted; checker runs not authenticated by Burrower".into(),
+            explanation:
+                "Reconciliation evidence submitted; checker runs not authenticated by Burrower"
+                    .into(),
             artifacts: Vec::new(),
         }),
         learning: None,
@@ -210,8 +217,7 @@ mod tests {
     use super::*;
     use tempfile::tempdir;
 
-    const DIGEST: &str =
-        "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef";
+    const DIGEST: &str = "0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef";
 
     fn checked(checker: Checker, route: Route, invocation: &str) -> CheckLeg {
         CheckLeg {

From b203cc0acc41d8ecb60be23261890ff265140f0c Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:56:45 +0000
Subject: [PATCH 11/17] fix(proofs): resolve Agda nested modules and pinned
 library path

---
 scripts/agda-safe-check.sh | 26 ++++++++++++++++++++++----
 1 file changed, 22 insertions(+), 4 deletions(-)

diff --git a/scripts/agda-safe-check.sh b/scripts/agda-safe-check.sh
index 3600947..eac4b04 100644
--- a/scripts/agda-safe-check.sh
+++ b/scripts/agda-safe-check.sh
@@ -1,21 +1,39 @@
 #!/usr/bin/env bash
 # SPDX-License-Identifier: MPL-2.0
-# First-party Agda theory checks must use the exact safety option set.
+# First-party Agda theory checks: keep the safety flags and module roots.
 set -euo pipefail
 if (( $# == 0 )); then
   echo "usage: $0 FILE.agda [FILE.agda ...]" >&2
   exit 2
 fi
 agda_bin="${AGDA_BIN:-agda}"
-if ! command -v "$agda_bin" >/dev/null 2>&1; then
+checker="$(command -v -- "$agda_bin" || true)"
+if [[ -z "$checker" ]]; then
   echo "Agda checker unavailable: $agda_bin" >&2
   exit 127
 fi
-"$agda_bin" --version >&2
+# Preserve an executable path when checking modules from their own roots.
+if [[ "$checker" != /* ]]; then
+  checker="$(realpath -e -- "$checker")"
+fi
+"$checker" --version >&2
+include_args=()
+if [[ -n "${AGDA_LIBRARY_INCLUDE:-}" ]]; then
+  if [[ ! -d "$AGDA_LIBRARY_INCLUDE" ]]; then
+    echo "Agda library source directory unavailable: $AGDA_LIBRARY_INCLUDE" >&2
+    exit 2
+  fi
+  include_args=(-i "$(realpath -e -- "$AGDA_LIBRARY_INCLUDE")")
+fi
 for source in "$@"; do
   if [[ "$source" == -* || "$source" != *.agda || ! -f "$source" ]]; then
     echo "Not a readable Agda source (options forbidden): $source" >&2
     exit 2
   fi
-  "$agda_bin" --safe --without-K --cubical-compatible "$source"
+  module="$(realpath -e -- "$source")"
+  # Module Properties in path/to/Properties.agda must be checked from
+  # path/to, rather than forcing a false module/path mismatch at repo root.
+  ( cd -- "$(dirname -- "$module")" &&
+    "$checker" --safe --without-K --cubical-compatible \
+      "${include_args[@]}" "$(basename -- "$module")" )
 done

From 0d96e944b6ff001c8a32d6df30e74cbbc970ef84 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:56:48 +0000
Subject: [PATCH 12/17] fix(proofs): resolve Agda nested modules and pinned
 library path

---
 tests/agda-safe-check.sh | 33 ++++++++++++++++++++++-----------
 1 file changed, 22 insertions(+), 11 deletions(-)

diff --git a/tests/agda-safe-check.sh b/tests/agda-safe-check.sh
index 275128d..be27a64 100644
--- a/tests/agda-safe-check.sh
+++ b/tests/agda-safe-check.sh
@@ -4,29 +4,40 @@ set -euo pipefail
 root="$(cd "$(dirname "$0")/.." && pwd)"
 tmp="$(mktemp -d)"
 trap 'rm -rf "$tmp"' EXIT
-printf 'module Test where\n' > "$tmp/Test.agda"
+mkdir -p "$tmp/nested" "$tmp/stdlib"
+printf 'module Test where\n' > "$tmp/nested/Test.agda"
 cat > "$tmp/fake-agda" <<'SH'
 #!/usr/bin/env bash
 set -euo pipefail
 if [[ "${1:-}" == --version ]]; then
-  echo "Agda version 2.8.0"
+  printf 'Agda version 2.8.0\n'
 else
   printf '%s\n' "$@" > "$AGDA_CAPTURE"
+  pwd > "$AGDA_CWD_CAPTURE"
 fi
 SH
 chmod +x "$tmp/fake-agda"
 AGDA_BIN="$tmp/fake-agda" AGDA_CAPTURE="$tmp/capture" \
-  bash "$root/scripts/agda-safe-check.sh" "$tmp/Test.agda"
+ AGDA_CWD_CAPTURE="$tmp/cwd" bash "$root/scripts/agda-safe-check.sh" "$tmp/nested/Test.agda"
 mapfile -t args < "$tmp/capture"
-[[ "${#args[@]}" -eq 4 && "${args[0]}" == --safe &&
-   "${args[1]}" == --without-K && "${args[2]}" == --cubical-compatible &&
-   "${args[3]}" == "$tmp/Test.agda" ]]
+[[ "${#args[@]}" -eq 4 && "${args[0]}" == --safe ]]
+[[ "${args[1]}" == --without-K && "${args[2]}" == --cubical-compatible ]]
+[[ "${args[3]}" == Test.agda ]]
+[[ "$(cat "$tmp/cwd")" == "$tmp/nested" ]]
+AGDA_BIN="$tmp/fake-agda" AGDA_CAPTURE="$tmp/capture" AGDA_CWD_CAPTURE="$tmp/cwd" \
+ AGDA_LIBRARY_INCLUDE="$tmp/stdlib" bash "$root/scripts/agda-safe-check.sh" "$tmp/nested/Test.agda"
+mapfile -t args < "$tmp/capture"
+[[ "${#args[@]}" -eq 6 && "${args[3]}" == -i ]]
+[[ "${args[4]}" == "$tmp/stdlib" && "${args[5]}" == Test.agda ]]
 if AGDA_BIN="$tmp/fake-agda" AGDA_CAPTURE="$tmp/capture" \
   bash "$root/scripts/agda-safe-check.sh" --with-K; then
-  echo "unsafe option incorrectly accepted" >&2; exit 1
+  echo "unsafe option was accepted" >&2; exit 1
+fi
+if AGDA_BIN="$tmp/not-installed" bash "$root/scripts/agda-safe-check.sh" "$tmp/nested/Test.agda"; then
+  echo "missing checker was accepted" >&2; exit 1
 fi
-if AGDA_BIN="$tmp/not-installed" \
-  bash "$root/scripts/agda-safe-check.sh" "$tmp/Test.agda"; then
-  echo "missing checker incorrectly accepted" >&2; exit 1
+if AGDA_BIN="$tmp/fake-agda" AGDA_LIBRARY_INCLUDE="$tmp/missing" \
+  bash "$root/scripts/agda-safe-check.sh" "$tmp/nested/Test.agda"; then
+  echo "missing include directory was accepted" >&2; exit 1
 fi
-echo 'Agda flags positive and negative controls passed'
+echo 'Agda safe invocation, nested module, include path, and negative controls passed'

From 96699a957b04fa1d8a24b218af0f192b011d9852 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 09:25:22 +0000
Subject: [PATCH 13/17] Update crates/burrower-core/src/reconciliation.rs

Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
---
 crates/burrower-core/src/reconciliation.rs | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/crates/burrower-core/src/reconciliation.rs b/crates/burrower-core/src/reconciliation.rs
index e4df007..053ca8d 100644
--- a/crates/burrower-core/src/reconciliation.rs
+++ b/crates/burrower-core/src/reconciliation.rs
@@ -154,7 +154,9 @@ impl ProofReconciliation {
                 if leg.outcome == LegOutcome::Checked && !leg.axioms.is_empty() {
                     return Err(format!("unchecked axioms in {expected:?} no-axiom claim"));
                 }
-                if leg.outcome == LegOutcome::CheckedWithAxioms && leg.axioms.is_empty() {
+                if leg.outcome == LegOutcome::CheckedWithAxioms
+                    && (leg.axioms.is_empty() || leg.axioms.iter().any(|a| a.trim().is_empty()))
+                {
                     return Err(format!("{expected:?} axiomatic claim names no axioms"));
                 }
                 if source_leg {

From 6fb19fd5a0db31ff1a3f64fa468d84031fbb6d7c Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 09:25:46 +0000
Subject: [PATCH 14/17] Update docs/PROOF-RECONCILIATION.adoc

Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
---
 docs/PROOF-RECONCILIATION.adoc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/PROOF-RECONCILIATION.adoc b/docs/PROOF-RECONCILIATION.adoc
index 6fcd260..dcb416d 100644
--- a/docs/PROOF-RECONCILIATION.adoc
+++ b/docs/PROOF-RECONCILIATION.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-License-Identifier: MPL-2.0
 = Proof Reconciliation Receipts
 :toc:
 

From 0ae5a754aab487217162e483c95a5a4a98e51305 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 09:26:49 +0000
Subject: [PATCH 15/17] Update tests/agda-safe-check.sh

Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
---
 tests/agda-safe-check.sh | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tests/agda-safe-check.sh b/tests/agda-safe-check.sh
index be27a64..98ecce0 100644
--- a/tests/agda-safe-check.sh
+++ b/tests/agda-safe-check.sh
@@ -1,5 +1,7 @@
 #!/usr/bin/env bash
 # SPDX-License-Identifier: MPL-2.0
+# Tests scripts/agda-safe-check.sh with a fake Agda executable.
+# Checks the canonical safe Agda options, rejection of --with-K, and failure when the checker is missing.
 set -euo pipefail
 root="$(cd "$(dirname "$0")/.." && pwd)"
 tmp="$(mktemp -d)"

From 68795acbe0e539f8b839f0cd19456984122a994b Mon Sep 17 00:00:00 2001
From: "coderabbitai[bot]"
 <136622811+coderabbitai[bot]@users.noreply.github.com>
Date: Sun, 1 Nov 2026 09:28:05 +0000
Subject: [PATCH 16/17] docs(reconciliation): document CLI dispatch, validation
 rules, and ledger recording errors

<!-- coderabbit-ai-generated:v1 -->
---
 crates/burrower-cli/src/main.rs            |  3 +++
 crates/burrower-core/src/reconciliation.rs | 15 +++++++++++++++
 2 files changed, 18 insertions(+)

diff --git a/crates/burrower-cli/src/main.rs b/crates/burrower-cli/src/main.rs
index 55b3f43..5f609af 100644
--- a/crates/burrower-cli/src/main.rs
+++ b/crates/burrower-cli/src/main.rs
@@ -386,6 +386,9 @@ fn handle_attempt(
     Ok(())
 }
 
+/// Dispatch the requested command. Reconciliation reads a JSON receipt and
+/// records it as proposed evidence, propagating read, parse, validation and
+/// ledger errors.
 fn main() -> Result<()> {
     let cli = Cli::parse();
     match cli.cmd {
diff --git a/crates/burrower-core/src/reconciliation.rs b/crates/burrower-core/src/reconciliation.rs
index 053ca8d..d4fe21b 100644
--- a/crates/burrower-core/src/reconciliation.rs
+++ b/crates/burrower-core/src/reconciliation.rs
@@ -30,6 +30,7 @@ pub enum LegOutcome {
 }
 
 impl LegOutcome {
+    /// Whether the leg claims a check, with or without axioms.
     fn checked(self) -> bool {
         matches!(self, Self::Checked | Self::CheckedWithAxioms)
     }
@@ -90,10 +91,12 @@ pub struct ProofReconciliation {
     pub lean: CheckLeg,
 }
 
+/// Whether a value is present and contains non-whitespace characters.
 fn filled(s: &Option<String>) -> bool {
     s.as_deref().is_some_and(|v| !v.trim().is_empty())
 }
 
+/// Whether a string has the shape of a SHA-256 digest in hexadecimal.
 fn sha256(s: &str) -> bool {
     s.len() == 64 && s.bytes().all(|b| b.is_ascii_hexdigit())
 }
@@ -103,6 +106,12 @@ impl ProofReconciliation {
     ///
     /// A successful validation is NOT a checked proof; callers must still
     /// authenticate the run references and check the referenced artefacts.
+    /// Unchecked or unavailable legs can pass validation without run evidence.
+    ///
+    /// # Errors
+    ///
+    /// Returns a description of the first invalid schema, provenance, leg
+    /// route, run evidence, correspondence, axiom claim or Agda invocation.
     pub fn validate(&self) -> std::result::Result<(), String> {
         if self.schema != RECONCILIATION_SCHEMA {
             return Err("unsupported reconciliation schema".into());
@@ -188,6 +197,12 @@ impl ProofReconciliation {
 /// Append the *claim* to Burrower's existing interim JSONL ledger. The
 /// status remains "proposed": an imported receipt is not proof of execution.
 /// No second persistent database or new state store is introduced.
+/// `theorem_statement` supplies the ledger's goal identity and excerpt.
+///
+/// # Errors
+///
+/// Returns a validation error before appending if the receipt is invalid,
+/// or propagates an error from serialising or appending the ledger record.
 pub fn record_reconciliation(
     ledger: &Ledger,
     theorem_statement: &str,

From f12f53275f0fa1aef073be975def84e954fc63b0 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Mon, 2 Nov 2026 07:09:47 +0000
Subject: [PATCH 17/17] Update crates/burrower-core/src/reconciliation.rs

Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
---
 crates/burrower-core/src/reconciliation.rs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/crates/burrower-core/src/reconciliation.rs b/crates/burrower-core/src/reconciliation.rs
index d4fe21b..ad5d8d9 100644
--- a/crates/burrower-core/src/reconciliation.rs
+++ b/crates/burrower-core/src/reconciliation.rs
@@ -180,6 +180,7 @@ impl ProofReconciliation {
                     if words.len() < 5
                         || !words[0].rsplit('/').next().is_some_and(|cmd| cmd == "agda")
                         || words[1..4] != ["--safe", "--without-K", "--cubical-compatible"]
+                        || words[4..].iter().any(|w| w.starts_with('-'))
                     {
                         return Err("Agda check missing canonical safe flags".into());
                     }