cs.LO — Logic in Computer Science
A Machine-Checked Kernel for Federated Automated Adjudication: Credibility Lattice Completion, Certificate Lifecycle Invariants, Certified Numerical Anchors, and a Parameterized Rice Template
We present a formally specified and machine-checked kernel for a federated automated adjudication system, in which independent computational lines judge mathematical and operational claims and deposit their verdicts, evidence, and certificates in a shared ledger. The kernel comprises five components. (i) A three-rung, three-track credibility lattice obtained as a completion of a legacy five-element poset: the completion is justified by an exhaustive enumeration over all 11^{3}=1331 ordered triples and is fully re-formalized in Lean 4, where the equational lattice laws, the order axioms, and the extremality properties of join and meet are all proved by the decide procedure over the finite carrier. (ii) A five-state certificate lifecycle machine with nine legal transitions and machine-checked invariants, likewise re-formalized in Lean 4; the formalization caught a specification flaw in one invariant (the originally stated grant-gating condition is false), and we report the corrected, machine-proved form. (iii) Certified numerical anchors: uniqueness of the gauged fixed point of circulant entropic-optimal-transport (Sinkhorn) systems, established by a Krawczyk interval operator with outward rounding across a six-instance family (k in {6,10 }, varepsilon in {1,1/2,1/5 }, later extended to ten instances), together with a second anchor family of five auction-algorithm assignment instances certified by interval dual brackets. We state plainly that the certification of these numerical anchors is carried by the Python interval-arithmetic layer; the attempted port to the Lean 4 interval library leancert is blocked by structural capability boundaries of that library (absence of the logarithm from its supported expression grammar and infeasibility of its determinant computation at the required dimensions), and the Lean files are formal statements, not machine-verified certificates. (iv) A parameterized Lean 4 template for Rice-type undecidability, consisting of a bridge theorem, an extensionality lemma, an instantiation generator, and discharged instances of increasing difficulty. (v) A minimal trusted computing base result: the soundness of an interval certificate checker (accept implies correctness), itself machine-proved in Lean 4. All Lean artifacts were verified on cloud infrastructure (Axiom Axle, environment lean-4.28.0) under the strict verify_proof channel, with axiom audits restricted to propext, Classical.choice, and Quot.sound, and no sorryAx. Empirical fuzzing over three certificate families observed zero false accepts; we report rule-of-three 95% upper bounds on the false-accept rate and explicitly do not claim a guarantee.