tokitai-operator 0.1.0

//! Theorem-binding registry.
//!
//! `TheoremBindingRegistry` pairs each property (e.g.
//! `padic_valuation_skip`, `finite_sheaf_gluing`) with a Lean
//! theorem identifier, a runtime oracle, and a known-coverage
//! status. The registry is the bridge between the Rust-side
//! property tests and the Lean-side formal proofs.
//!
//! `tokitai_default()` returns the registry that ships with the
//! crate; the optional Lean check (`scripts/optional_lean_check.sh`)
//! exercises the actual `lean` compiler on each theorem.
//!
use std::collections::BTreeMap;
use std::fs;
use std::path::Path;

use crate::domain::PadicOutputCertificate;
use crate::object::sheaf::SheafCompatibilityReport;
use crate::planner::{ExecutionPlan, PlanStepKind, ProofKind};
use crate::{Error, Result};

pub const PADIC_VALUATION_SKIP_THEOREM_ID: &str = "tokitai_padic_valuation_skip_sound_mod_pk";
pub const PADIC_VALUATION_DOT_PRODUCT_THEOREM_ID: &str =
    "tokitai_padic_valuation_skip_dot_product_sound_mod_pk";
pub const PADIC_VALUATION_MATRIX_OUTPUT_THEOREM_ID: &str =
    "tokitai_padic_valuation_skip_matrix_output_sound_mod_pk";
pub const PADIC_VALUATION_SKIP_LEAN_FILE: &str = "docs/theorems/padic_valuation_skip.lean";
pub const FINITE_SHEAF_GLUING_THEOREM_ID: &str = "tokitai_finite_sheaf_gluing_sound";
pub const FINITE_SHEAF_OBSTRUCTION_THEOREM_ID: &str =
    "tokitai_finite_sheaf_incompatible_overlap_blocks_gluing";
pub const FINITE_SHEAF_GLUING_LEAN_FILE: &str = "docs/theorems/finite_sheaf_gluing.lean";
pub const PADIC_VALUATION_SKIP_TRANSCRIPT_FILE: &str =
    "docs/theorems/padic_valuation_skip.transcript.txt";
pub const FINITE_SHEAF_GLUING_TRANSCRIPT_FILE: &str =
    "docs/theorems/finite_sheaf_gluing.transcript.txt";

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct PadicValuationSkipTheoremBinding {
    pub theorem_id: String,
    pub lean_file: String,
    pub runtime_proof_id: String,
    pub runtime_proof_kind: String,
    pub replay_rule: String,
    pub prime: u64,
    pub precision: u32,
    pub valuation_cutoff: u32,
    pub modulus: u128,
    pub assumption_mapping: Vec<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct PadicValuationStratifiedMatmulTheoremBinding {
    pub theorem_id: String,
    pub matrix_output_theorem_id: String,
    pub lean_file: String,
    pub runtime_proof_id: String,
    pub runtime_proof_kind: String,
    pub replay_rule: String,
    pub prime: u64,
    pub precision: u32,
    pub valuation_cutoff: u32,
    pub output_certificate_count: usize,
    pub evaluated_product_count: usize,
    pub skipped_product_count: usize,
    pub minimum_skipped_valuation: Option<u32>,
    pub minimum_precision_safety_margin: Option<u32>,
    pub assumption_mapping: Vec<String>,
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct FiniteSheafGluingTheoremBinding {
    pub theorem_id: String,
    pub obstruction_theorem_id: String,
    pub lean_file: String,
    pub runtime_proof_id: String,
    pub runtime_proof_kind: String,
    pub replay_rule: String,
    pub target: String,
    pub cover_opens: Vec<String>,
    pub checked_overlaps: usize,
    pub restriction_witness_count: usize,
    pub obstruction_count: usize,
    pub compatible: bool,
    pub assumption_mapping: Vec<String>,
}

pub trait RuntimeTheoremBinding {
    fn theorem_id(&self) -> &str;
    fn lean_file(&self) -> &str;
    fn runtime_proof_id(&self) -> &str;
    fn runtime_proof_kind(&self) -> &str;
    fn replay_rule(&self) -> &str;
    fn assumption_mapping(&self) -> &[String];
}

impl RuntimeTheoremBinding for PadicValuationSkipTheoremBinding {
    fn theorem_id(&self) -> &str {
        &self.theorem_id
    }

    fn lean_file(&self) -> &str {
        &self.lean_file
    }

    fn runtime_proof_id(&self) -> &str {
        &self.runtime_proof_id
    }

    fn runtime_proof_kind(&self) -> &str {
        &self.runtime_proof_kind
    }

    fn replay_rule(&self) -> &str {
        &self.replay_rule
    }

    fn assumption_mapping(&self) -> &[String] {
        &self.assumption_mapping
    }
}

impl RuntimeTheoremBinding for PadicValuationStratifiedMatmulTheoremBinding {
    fn theorem_id(&self) -> &str {
        &self.theorem_id
    }

    fn lean_file(&self) -> &str {
        &self.lean_file
    }

    fn runtime_proof_id(&self) -> &str {
        &self.runtime_proof_id
    }

    fn runtime_proof_kind(&self) -> &str {
        &self.runtime_proof_kind
    }

    fn replay_rule(&self) -> &str {
        &self.replay_rule
    }

    fn assumption_mapping(&self) -> &[String] {
        &self.assumption_mapping
    }
}

impl RuntimeTheoremBinding for FiniteSheafGluingTheoremBinding {
    fn theorem_id(&self) -> &str {
        &self.theorem_id
    }

    fn lean_file(&self) -> &str {
        &self.lean_file
    }

    fn runtime_proof_id(&self) -> &str {
        &self.runtime_proof_id
    }

    fn runtime_proof_kind(&self) -> &str {
        &self.runtime_proof_kind
    }

    fn replay_rule(&self) -> &str {
        &self.replay_rule
    }

    fn assumption_mapping(&self) -> &[String] {
        &self.assumption_mapping
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub enum CheckerTranscriptStatus {
    CheckedLocally,
    CheckerReady,
    StructuralOnly,
    MissingLean,
    Failed,
    Unknown(String),
}

impl CheckerTranscriptStatus {
    pub fn from_value(value: &str) -> Self {
        match value {
            "checked_locally" => Self::CheckedLocally,
            "checker-ready" => Self::CheckerReady,
            "structural_validation_only" | "structural validation only" => Self::StructuralOnly,
            "missing" => Self::MissingLean,
            "failed" => Self::Failed,
            other => Self::Unknown(other.to_string()),
        }
    }

    pub fn as_str(&self) -> &str {
        match self {
            Self::CheckedLocally => "checked_locally",
            Self::CheckerReady => "checker-ready",
            Self::StructuralOnly => "structural_validation_only",
            Self::MissingLean => "missing",
            Self::Failed => "failed",
            Self::Unknown(value) => value,
        }
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct CheckerTranscript {
    pub path: String,
    pub artifact: String,
    pub theorem_file: String,
    pub theorem_id: String,
    pub theorem_ids: Vec<String>,
    pub obstruction_theorem_id: Option<String>,
    pub checker: String,
    pub checker_version: Option<String>,
    pub checker_command: String,
    pub captured_status: CheckerTranscriptStatus,
    pub default_validation: String,
    pub local_default_with_lean: Option<String>,
    pub local_default_without_lean: Option<String>,
    pub scope: String,
    pub non_claim: String,
}

impl CheckerTranscript {
    pub fn from_file(path: impl AsRef<Path>) -> Result<Self> {
        let path = path.as_ref();
        let content = fs::read_to_string(path).map_err(|err| {
            Error::verification(format!(
                "failed to read checker transcript {}: {err}",
                path.display()
            ))
        })?;
        Self::from_str(&path.display().to_string(), &content)
    }

    pub fn from_str(path: &str, content: &str) -> Result<Self> {
        let mut fields = BTreeMap::new();
        for line in content.lines() {
            let Some((key, value)) = line.split_once(':') else {
                continue;
            };
            fields.insert(key.trim().to_string(), value.trim().to_string());
        }
        let required = |key: &str| -> Result<String> {
            fields.get(key).cloned().ok_or_else(|| {
                Error::verification(format!("checker transcript {path} missing field {key}"))
            })
        };
        Ok(Self {
            path: path.to_string(),
            artifact: required("artifact")?,
            theorem_file: required("theorem_file")?,
            theorem_id: required("theorem_id")?,
            theorem_ids: fields
                .get("theorem_ids")
                .map(|value| {
                    value
                        .split(',')
                        .map(str::trim)
                        .filter(|value| !value.is_empty())
                        .map(ToOwned::to_owned)
                        .collect::<Vec<_>>()
                })
                .unwrap_or_default(),
            obstruction_theorem_id: fields.get("obstruction_theorem_id").cloned(),
            checker: required("checker")?,
            checker_version: fields.get("checker_version").cloned(),
            checker_command: required("checker_command")?,
            captured_status: CheckerTranscriptStatus::from_value(&required("captured_status")?),
            default_validation: required("default_validation")?,
            local_default_with_lean: fields.get("local_default_with_lean").cloned(),
            local_default_without_lean: fields.get("local_default_without_lean").cloned(),
            scope: required("scope")?,
            non_claim: required("non_claim")?,
        })
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TheoremRuntimeRequirement {
    pub runtime_source: String,
    pub required_evidence: Vec<String>,
}

impl TheoremRuntimeRequirement {
    pub fn new(
        runtime_source: impl Into<String>,
        required_evidence: impl IntoIterator<Item = impl Into<String>>,
    ) -> Self {
        Self {
            runtime_source: runtime_source.into(),
            required_evidence: required_evidence
                .into_iter()
                .map(Into::into)
                .collect::<Vec<_>>(),
        }
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TheoremBindingDescriptor {
    pub theorem_id: String,
    pub lean_file: String,
    pub transcript_file: String,
    pub checker_command: String,
    pub assumption_mapping: Vec<String>,
    pub runtime_requirements: Vec<TheoremRuntimeRequirement>,
    pub conclusion_scope: String,
    pub non_claims: Vec<String>,
    pub transcript: CheckerTranscript,
}

impl TheoremBindingDescriptor {
    pub fn validate_transcript(&self) -> Result<()> {
        if self.transcript.theorem_file != self.lean_file {
            return Err(Error::verification(format!(
                "theorem {} transcript file mismatch: descriptor={} transcript={}",
                self.theorem_id, self.lean_file, self.transcript.theorem_file
            )));
        }
        let transcript_mentions_theorem = self.transcript.theorem_id == self.theorem_id
            || self
                .transcript
                .theorem_ids
                .iter()
                .any(|theorem| theorem == &self.theorem_id)
            || self
                .transcript
                .obstruction_theorem_id
                .as_deref()
                .is_some_and(|theorem| theorem == self.theorem_id);
        if !transcript_mentions_theorem {
            return Err(Error::verification(format!(
                "theorem {} missing from transcript {}",
                self.theorem_id, self.transcript.path
            )));
        }
        if self.transcript.checker_command != self.checker_command {
            return Err(Error::verification(format!(
                "theorem {} checker command mismatch: descriptor={} transcript={}",
                self.theorem_id, self.checker_command, self.transcript.checker_command
            )));
        }
        if matches!(
            self.transcript.captured_status,
            CheckerTranscriptStatus::Failed
        ) {
            return Err(Error::verification(format!(
                "theorem {} transcript records failed checker status",
                self.theorem_id
            )));
        }
        Ok(())
    }

    pub fn validate_runtime_evidence(&self, runtime_evidence: &[String]) -> Result<()> {
        for requirement in &self.runtime_requirements {
            for required in &requirement.required_evidence {
                if !runtime_evidence
                    .iter()
                    .any(|evidence| evidence == required || evidence.contains(required))
                {
                    return Err(Error::verification(format!(
                        "theorem {} missing runtime evidence {} from {}",
                        self.theorem_id, required, requirement.runtime_source
                    )));
                }
            }
        }
        Ok(())
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
pub struct TheoremBindingRegistry {
    descriptors: Vec<TheoremBindingDescriptor>,
}

impl TheoremBindingRegistry {
    pub fn from_descriptors(descriptors: Vec<TheoremBindingDescriptor>) -> Result<Self> {
        let registry = Self { descriptors };
        registry.validate()?;
        Ok(registry)
    }

    pub fn tokitai_default() -> Result<Self> {
        let padic_transcript = CheckerTranscript::from_file(PADIC_VALUATION_SKIP_TRANSCRIPT_FILE)?;
        let sheaf_transcript = CheckerTranscript::from_file(FINITE_SHEAF_GLUING_TRANSCRIPT_FILE)?;
        Self::from_descriptors(vec![
            padic_valuation_skip_theorem_descriptor(padic_transcript.clone()),
            padic_valuation_dot_product_theorem_descriptor(padic_transcript.clone()),
            padic_valuation_matrix_output_theorem_descriptor(padic_transcript),
            finite_sheaf_gluing_theorem_descriptor(sheaf_transcript.clone()),
            finite_sheaf_obstruction_theorem_descriptor(sheaf_transcript),
        ])
    }

    pub fn lookup(&self, theorem_id: &str) -> Result<&TheoremBindingDescriptor> {
        self.descriptors
            .iter()
            .find(|descriptor| descriptor.theorem_id == theorem_id)
            .ok_or_else(|| Error::verification(format!("unknown theorem binding {theorem_id}")))
    }

    pub fn descriptors(&self) -> &[TheoremBindingDescriptor] {
        &self.descriptors
    }

    pub fn validate(&self) -> Result<()> {
        if self.descriptors.is_empty() {
            return Err(Error::verification(
                "theorem binding registry must contain at least one descriptor",
            ));
        }
        for descriptor in &self.descriptors {
            descriptor.validate_transcript()?;
        }
        Ok(())
    }
}

pub fn padic_valuation_skip_theorem_binding(
    plan: &ExecutionPlan,
) -> Result<PadicValuationSkipTheoremBinding> {
    let resource = plan.resources.padic.as_ref().ok_or_else(|| {
        Error::verification("p-adic valuation-skip theorem binding requires p-adic plan resource")
    })?;
    let proof = plan
        .proof_objects
        .iter()
        .find(|proof| proof.kind == ProofKind::ValuationCutoff)
        .ok_or_else(|| {
            Error::verification(
                "p-adic valuation-skip theorem binding requires valuation_cutoff proof object",
            )
        })?;
    if !plan.steps.iter().any(|step| {
        matches!(
            step.kind,
            PlanStepKind::PadicValuationSkip { .. } | PlanStepKind::PadicMatmulValuationSkip { .. }
        )
    }) {
        return Err(Error::verification(
            "p-adic valuation-skip theorem binding requires a valuation-skip plan step",
        ));
    }
    let modulus = checked_modulus(resource.prime, resource.precision)?;
    Ok(PadicValuationSkipTheoremBinding {
        theorem_id: PADIC_VALUATION_SKIP_THEOREM_ID.to_string(),
        lean_file: PADIC_VALUATION_SKIP_LEAN_FILE.to_string(),
        runtime_proof_id: proof.id.clone(),
        runtime_proof_kind: "valuation_cutoff".to_string(),
        replay_rule: "valuation_cutoff_replay".to_string(),
        prime: resource.prime,
        precision: resource.precision,
        valuation_cutoff: resource.valuation_cutoff,
        modulus,
        assumption_mapping: vec![
            "Lean modulus p^k maps to PadicPlanningResource(prime, precision)".to_string(),
            "Lean skippedTermVanishesModulo assumption maps to valuation_cutoff proof evidence"
                .to_string(),
            "Lean dense/evaluated same-modulo conclusion maps to precision-bounded equality"
                .to_string(),
            "Rust runtime checks concrete terms before using the valuation-skip rewrite"
                .to_string(),
        ],
    })
}

pub fn padic_valuation_skip_theorem_binding_report(
    binding: &PadicValuationSkipTheoremBinding,
) -> String {
    format!(
        "theorem_id={}\nlean_file={}\nruntime_proof_id={}\nruntime_proof_kind={}\nreplay_rule={}\nprime={}\nprecision={}\nvaluation_cutoff={}\nmodulus={}\nassumption_mapping={}\n",
        binding.theorem_id,
        binding.lean_file,
        binding.runtime_proof_id,
        binding.runtime_proof_kind,
        binding.replay_rule,
        binding.prime,
        binding.precision,
        binding.valuation_cutoff,
        binding.modulus,
        binding.assumption_mapping.join(";")
    )
}

pub fn padic_valuation_stratified_matmul_theorem_binding(
    plan: &ExecutionPlan,
    output_certificates: &[PadicOutputCertificate],
) -> Result<PadicValuationStratifiedMatmulTheoremBinding> {
    let (prime, precision) = plan
        .steps
        .iter()
        .find_map(|step| {
            if let PlanStepKind::PadicMatmulValuationSkip {
                prime, precision, ..
            } = step.kind
            {
                Some((prime, precision))
            } else {
                None
            }
        })
        .ok_or_else(|| {
            Error::verification(
                "valuation-stratified matmul theorem binding requires padic_matmul_valuation_skip plan step",
            )
        })?;
    let proof = plan
        .proof_objects
        .iter()
        .find(|proof| {
            proof.kind == ProofKind::ValuationCutoff
                && proof.id.starts_with("proof:padic_matmul_valuation_skip:")
        })
        .ok_or_else(|| {
            Error::verification(
                "valuation-stratified matmul theorem binding requires matmul valuation_cutoff proof object",
            )
        })?;
    if output_certificates.is_empty() {
        return Err(Error::verification(
            "valuation-stratified matmul theorem binding requires output certificates",
        ));
    }

    let mut evaluated_product_count = 0usize;
    let mut skipped_product_count = 0usize;
    let mut minimum_skipped_valuation: Option<u32> = None;
    let mut minimum_precision_safety_margin: Option<u32> = None;
    for certificate in output_certificates {
        if certificate.precision_cutoff != precision {
            return Err(Error::verification(format!(
                "matmul output certificate ({},{}) precision cutoff {} does not match plan precision {}",
                certificate.row, certificate.col, certificate.precision_cutoff, precision
            )));
        }
        if certificate.skipped_product_count > 0 {
            let Some(min_skipped) = certificate.min_skipped_valuation else {
                return Err(Error::verification(format!(
                    "matmul output certificate ({},{}) skips products without minimum skipped valuation",
                    certificate.row, certificate.col
                )));
            };
            if min_skipped < precision {
                return Err(Error::verification(format!(
                    "matmul output certificate ({},{}) has unsafe skipped valuation {} below precision {}",
                    certificate.row, certificate.col, min_skipped, precision
                )));
            }
            let Some(margin) = certificate.precision_safety_margin else {
                return Err(Error::verification(format!(
                    "matmul output certificate ({},{}) skips products without precision safety margin",
                    certificate.row, certificate.col
                )));
            };
            minimum_skipped_valuation = Some(
                minimum_skipped_valuation
                    .map(|current| current.min(min_skipped))
                    .unwrap_or(min_skipped),
            );
            minimum_precision_safety_margin = Some(
                minimum_precision_safety_margin
                    .map(|current| current.min(margin))
                    .unwrap_or(margin),
            );
        }
        evaluated_product_count += certificate.evaluated_product_count;
        skipped_product_count += certificate.skipped_product_count;
    }

    Ok(PadicValuationStratifiedMatmulTheoremBinding {
        theorem_id: PADIC_VALUATION_DOT_PRODUCT_THEOREM_ID.to_string(),
        matrix_output_theorem_id: PADIC_VALUATION_MATRIX_OUTPUT_THEOREM_ID.to_string(),
        lean_file: PADIC_VALUATION_SKIP_LEAN_FILE.to_string(),
        runtime_proof_id: proof.id.clone(),
        runtime_proof_kind: "valuation_cutoff".to_string(),
        replay_rule: "valuation_stratified_matmul_certificate_replay".to_string(),
        prime,
        precision,
        valuation_cutoff: precision,
        output_certificate_count: output_certificates.len(),
        evaluated_product_count,
        skipped_product_count,
        minimum_skipped_valuation,
        minimum_precision_safety_margin,
        assumption_mapping: vec![
            "Lean evaluatedDot maps to the sum of products with valuation lower bound below the active precision cutoff".to_string(),
            "Lean skippedDot maps to products counted by PadicOutputCertificate::skipped_product_count".to_string(),
            "Lean hskipDot maps to PadicOutputCertificate::min_skipped_valuation >= precision_cutoff".to_string(),
            "Lean matrix output theorem is applied independently to each output certificate row/col".to_string(),
            "Rust dense CPU oracle equality maps to the sameModulo conclusion for each matrix output".to_string(),
        ],
    })
}

pub fn padic_valuation_stratified_matmul_theorem_binding_report(
    binding: &PadicValuationStratifiedMatmulTheoremBinding,
) -> String {
    format!(
        "theorem_id={}\nmatrix_output_theorem_id={}\nlean_file={}\nruntime_proof_id={}\nruntime_proof_kind={}\nreplay_rule={}\nprime={}\nprecision={}\nvaluation_cutoff={}\noutput_certificate_count={}\nevaluated_product_count={}\nskipped_product_count={}\nminimum_skipped_valuation={:?}\nminimum_precision_safety_margin={:?}\nassumption_mapping={}\n",
        binding.theorem_id,
        binding.matrix_output_theorem_id,
        binding.lean_file,
        binding.runtime_proof_id,
        binding.runtime_proof_kind,
        binding.replay_rule,
        binding.prime,
        binding.precision,
        binding.valuation_cutoff,
        binding.output_certificate_count,
        binding.evaluated_product_count,
        binding.skipped_product_count,
        binding.minimum_skipped_valuation,
        binding.minimum_precision_safety_margin,
        binding.assumption_mapping.join(";")
    )
}

pub fn finite_sheaf_gluing_theorem_binding<T>(
    plan: &ExecutionPlan,
    compatibility: &SheafCompatibilityReport<T>,
) -> Result<FiniteSheafGluingTheoremBinding> {
    let (target, cover_opens) = plan
        .steps
        .iter()
        .find_map(|step| {
            if let PlanStepKind::CoverGlueCheck { target, opens } = &step.kind {
                Some((target.clone(), opens.clone()))
            } else {
                None
            }
        })
        .ok_or_else(|| {
            Error::verification(
                "finite-sheaf gluing theorem binding requires cover_glue_check plan step",
            )
        })?;
    let proof = plan
        .proof_objects
        .iter()
        .find(|proof| {
            proof.kind == ProofKind::RewriteSoundness
                && proof.id == "proof:rewrite:cover_local_to_global_glue"
        })
        .ok_or_else(|| {
            Error::verification(
                "finite-sheaf gluing theorem binding requires cover_local_to_global_glue rewrite proof",
            )
        })?;
    Ok(FiniteSheafGluingTheoremBinding {
        theorem_id: if compatibility.compatible {
            FINITE_SHEAF_GLUING_THEOREM_ID.to_string()
        } else {
            FINITE_SHEAF_OBSTRUCTION_THEOREM_ID.to_string()
        },
        obstruction_theorem_id: FINITE_SHEAF_OBSTRUCTION_THEOREM_ID.to_string(),
        lean_file: FINITE_SHEAF_GLUING_LEAN_FILE.to_string(),
        runtime_proof_id: proof.id.clone(),
        runtime_proof_kind: "rewrite_soundness".to_string(),
        replay_rule: "rewrite_soundness_replay".to_string(),
        target,
        cover_opens,
        checked_overlaps: compatibility.checked_overlaps,
        restriction_witness_count: compatibility.restriction_witnesses.len(),
        obstruction_count: compatibility.obstructions.len(),
        compatible: compatibility.compatible,
        assumption_mapping: vec![
            "Lean validCover maps to FiniteSite::validate_cover success".to_string(),
            "Lean restrictionComposition maps to FiniteSite::check_restriction_composition witnesses"
                .to_string(),
            "Lean compatibleOverlaps maps to SheafCompatibilityReport.compatible".to_string(),
            "Lean globalRestrictsToLocals maps to restriction witnesses in SheafCompatibilityReport"
                .to_string(),
            "Lean obstruction theorem maps to SheafObstruction entries when compatibility fails"
                .to_string(),
        ],
    })
}

pub fn finite_sheaf_gluing_theorem_binding_report(
    binding: &FiniteSheafGluingTheoremBinding,
) -> String {
    format!(
        "theorem_id={}\nobstruction_theorem_id={}\nlean_file={}\nruntime_proof_id={}\nruntime_proof_kind={}\nreplay_rule={}\ntarget={}\ncover_opens={}\nchecked_overlaps={}\nrestriction_witness_count={}\nobstruction_count={}\ncompatible={}\nassumption_mapping={}\n",
        binding.theorem_id,
        binding.obstruction_theorem_id,
        binding.lean_file,
        binding.runtime_proof_id,
        binding.runtime_proof_kind,
        binding.replay_rule,
        binding.target,
        binding.cover_opens.join("|"),
        binding.checked_overlaps,
        binding.restriction_witness_count,
        binding.obstruction_count,
        binding.compatible,
        binding.assumption_mapping.join(";")
    )
}

fn checked_modulus(prime: u64, precision: u32) -> Result<u128> {
    let mut modulus = 1u128;
    for _ in 0..precision {
        modulus = modulus.checked_mul(u128::from(prime)).ok_or_else(|| {
            Error::verification("p-adic valuation-skip theorem binding modulus overflow")
        })?;
    }
    Ok(modulus)
}

fn padic_valuation_skip_theorem_descriptor(
    transcript: CheckerTranscript,
) -> TheoremBindingDescriptor {
    TheoremBindingDescriptor {
        theorem_id: PADIC_VALUATION_SKIP_THEOREM_ID.to_string(),
        lean_file: PADIC_VALUATION_SKIP_LEAN_FILE.to_string(),
        transcript_file: PADIC_VALUATION_SKIP_TRANSCRIPT_FILE.to_string(),
        checker_command: "lean docs/theorems/padic_valuation_skip.lean".to_string(),
        assumption_mapping: vec![
            "Lean p maps to PadicPlanningResource.prime".to_string(),
            "Lean k maps to PadicPlanningResource.precision".to_string(),
            "Lean skippedTermVanishesModulo maps to valuation_cutoff proof evidence".to_string(),
            "Lean sameModulo conclusion maps to precision-bounded equality".to_string(),
        ],
        runtime_requirements: vec![TheoremRuntimeRequirement::new(
            "PadicValuationSkipTheoremBinding",
            [
                "PadicPlanningResource",
                "valuation_cutoff proof object",
                "valuation-skip plan step",
            ],
        )],
        conclusion_scope: "skipped terms vanish modulo p^k for the minimized valuation-skip model"
            .to_string(),
        non_claims: vec![
            "not a formalization of p-adic fields".to_string(),
            "not a proof of Tokitai's Rust runtime".to_string(),
            "not a theorem for all p-adic algebra".to_string(),
        ],
        transcript,
    }
}

fn padic_valuation_dot_product_theorem_descriptor(
    transcript: CheckerTranscript,
) -> TheoremBindingDescriptor {
    TheoremBindingDescriptor {
        theorem_id: PADIC_VALUATION_DOT_PRODUCT_THEOREM_ID.to_string(),
        lean_file: PADIC_VALUATION_SKIP_LEAN_FILE.to_string(),
        transcript_file: PADIC_VALUATION_SKIP_TRANSCRIPT_FILE.to_string(),
        checker_command: "lean docs/theorems/padic_valuation_skip.lean".to_string(),
        assumption_mapping: vec![
            "Lean evaluatedDot maps to products evaluated by the certified sparse CPU oracle"
                .to_string(),
            "Lean skippedDot maps to products summarized by output skip certificates".to_string(),
            "Lean hskipDot maps to min_skipped_valuation >= precision_cutoff".to_string(),
            "Lean sameModulo conclusion maps to dense CPU oracle equality for each dot output"
                .to_string(),
        ],
        runtime_requirements: vec![TheoremRuntimeRequirement::new(
            "PadicValuationStratifiedMatmulTheoremBinding",
            [
                "padic_matmul_valuation_skip plan step",
                "matmul valuation_cutoff proof object",
                "output certificates",
                "min_skipped_valuation >= precision_cutoff",
            ],
        )],
        conclusion_scope:
            "valuation-stratified dot-product skipped terms vanish modulo p^k in the minimized model"
                .to_string(),
        non_claims: vec![
            "not a proof of arbitrary p-adic dot products".to_string(),
            "not a proof of Tokitai's Rust runtime".to_string(),
            "not a proof of GPU machine code".to_string(),
        ],
        transcript,
    }
}

fn padic_valuation_matrix_output_theorem_descriptor(
    transcript: CheckerTranscript,
) -> TheoremBindingDescriptor {
    TheoremBindingDescriptor {
        theorem_id: PADIC_VALUATION_MATRIX_OUTPUT_THEOREM_ID.to_string(),
        lean_file: PADIC_VALUATION_SKIP_LEAN_FILE.to_string(),
        transcript_file: PADIC_VALUATION_SKIP_TRANSCRIPT_FILE.to_string(),
        checker_command: "lean docs/theorems/padic_valuation_skip.lean".to_string(),
        assumption_mapping: vec![
            "Lean evaluatedOutput maps to each certified sparse matrix output".to_string(),
            "Lean skippedOutput maps to the products skipped for one output certificate"
                .to_string(),
            "Lean hskipOutput maps to per-output minimum skipped valuation evidence".to_string(),
            "Lean sameModulo conclusion maps to dense CPU oracle equality for that output"
                .to_string(),
        ],
        runtime_requirements: vec![TheoremRuntimeRequirement::new(
            "PadicValuationStratifiedMatmulTheoremBinding",
            [
                "output certificates",
                "matrix output theorem",
                "dense CPU oracle equality",
            ],
        )],
        conclusion_scope:
            "each valuation-stratified matrix output preserves the fixed-precision residue modulo p^k"
                .to_string(),
        non_claims: vec![
            "not a proof of a complete p-adic GEMM implementation".to_string(),
            "not a proof of Tokitai's Rust runtime".to_string(),
            "not a proof of GPU machine code".to_string(),
        ],
        transcript,
    }
}

fn finite_sheaf_gluing_theorem_descriptor(
    transcript: CheckerTranscript,
) -> TheoremBindingDescriptor {
    TheoremBindingDescriptor {
        theorem_id: FINITE_SHEAF_GLUING_THEOREM_ID.to_string(),
        lean_file: FINITE_SHEAF_GLUING_LEAN_FILE.to_string(),
        transcript_file: FINITE_SHEAF_GLUING_TRANSCRIPT_FILE.to_string(),
        checker_command: "lean docs/theorems/finite_sheaf_gluing.lean".to_string(),
        assumption_mapping: vec![
            "Lean validCover maps to FiniteSite::validate_cover success".to_string(),
            "Lean compatibleOverlaps maps to SheafCompatibilityReport.compatible".to_string(),
            "Lean globalRestrictsToLocals maps to restriction witnesses".to_string(),
        ],
        runtime_requirements: vec![TheoremRuntimeRequirement::new(
            "FiniteSheafGluingTheoremBinding",
            [
                "cover_glue_check plan step",
                "cover_local_to_global_glue rewrite proof",
                "SheafCompatibilityReport.compatible",
                "restriction witnesses",
            ],
        )],
        conclusion_scope: "finite-site compatible local sections glue in the minimized model"
            .to_string(),
        non_claims: vec![
            "not a formalization of general sheaf theory".to_string(),
            "not a cohomology theorem".to_string(),
            "not a proof of Tokitai's Rust runtime".to_string(),
        ],
        transcript,
    }
}

fn finite_sheaf_obstruction_theorem_descriptor(
    transcript: CheckerTranscript,
) -> TheoremBindingDescriptor {
    TheoremBindingDescriptor {
        theorem_id: FINITE_SHEAF_OBSTRUCTION_THEOREM_ID.to_string(),
        lean_file: FINITE_SHEAF_GLUING_LEAN_FILE.to_string(),
        transcript_file: FINITE_SHEAF_GLUING_TRANSCRIPT_FILE.to_string(),
        checker_command: "lean docs/theorems/finite_sheaf_gluing.lean".to_string(),
        assumption_mapping: vec![
            "Lean incompatible overlap premise maps to SheafObstruction entries".to_string(),
            "Lean blocked gluing conclusion maps to incompatible SheafCompatibilityReport"
                .to_string(),
        ],
        runtime_requirements: vec![TheoremRuntimeRequirement::new(
            "FiniteSheafGluingTheoremBinding",
            [
                "cover_glue_check plan step",
                "cover_local_to_global_glue rewrite proof",
                "SheafObstruction",
                "compatible=false",
            ],
        )],
        conclusion_scope: "finite-site obstruction boundary blocks gluing in the minimized model"
            .to_string(),
        non_claims: vec![
            "not a complete obstruction theory".to_string(),
            "not sheaf cohomology".to_string(),
            "not a proof of Tokitai's Rust runtime".to_string(),
        ],
        transcript,
    }
}