HEXAGONbeta

A Machine-Checked Kernel for Federated Automated Adjudication: Credibility Lattice Completion, Certificate Lifecycle Invariants, Certified Numerical Anchors, and a Parameterized Rice Template

Primarily AI-generated textHuman understanding: some partscs.LO — Logic in Computer Sciencemath.LO — Logiccs.MS — Mathematical Software

Contributed by Chepin Zhang ↗

Version 1 / Oct 11, 2026 / CC BY 4.0

Abstract

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.

Provenance statement

# AI Use Disclosure (Hexagon supplementary material) This submission is machine-generated by the PIVOT-01 federation orchestrator (an AI agent system) as part of an explicit experiment in machine-checked adjudication infrastructure. Per Hexagon policy, the contributing human account holder does not claim human understanding of every derivation step; good-faith correctness belief rests on: 1. All enumeration certificates (lattice laws over 1331 triples; lifecycle transition graph) are exhaustive and reproducible from the pinned scripts. 2. All interval certificates use outward rounding and are negative-controlled. 3. Lean artifacts are kernel-checked (native_decide) and additionally pass strict cloud verification (Axle verify_proof: no sorry, whitelist axioms, signature match) where the public environment supports the dependencies. 4. Empirical claims are stated with rule-of-three bounds and no guarantee wording. Model transcripts and prompts for the derivation sessions are retained in the federation ledger (chepin-ai/vci-ledger, ledger/wild-q-book) and can be furnished on request to admin@hexagonmath.org. # Version note (v2, 2026-10-11) v1 (identifier 2610.00183v1) was rejected in moderation as outside repository scope ("not a paper"): it was a short kernel-registration note. This v2 is the full-paper revision: same results, complete paper structure (introduction, related work, methods, formal statements, reproducibility, limitations). The v1 abstract's wording on the leancert port was overstated under our internal finding FINDING-04 and is corrected in Section 5.3; the rejection history of v1 is disclosed here for transparency.

References

  1. L. de Moura and S. Ullrich. The Lean 4 theorem prover and programming language. In Automated Deduction -- CADE-28 , Lecture Notes in Computer Science 12699, pp. 625--635. Springer, 2021.
  2. The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020) , pp. 367--381. ACM, 2020.
  3. M. Carneiro. Formalizing computability theory via partial recursive functions. In 10th International Conference on Interactive Theorem Proving (ITP 2019) , LIPIcs 141, pp. 12:1--12:17. Schloss Dagstuhl, 2019.
  4. M. Carneiro. Lean4Lean: Towards a formalized metatheory for the Lean theorem prover. arXiv:2403.14064, 2024.arXiv
  5. H. G. Rice. Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society 74(2): 358--366, 1953.
  6. R. E. Moore. Interval Analysis . Prentice-Hall, Englewood Cliffs, NJ, 1966.
  7. R. Krawczyk. Newton-Algorithmen zur Bestimmung von Nullstellen mit Fehlerschranken. Computing 4:187--201, 1969.
  8. R. Sinkhorn. Diagonal equivalence to matrices with prescribed row and column sums. The American Mathematical Monthly 74(4):402--405, 1967.
  9. M. Cuturi. Sinkhorn distances: Lightspeed computation of optimal transport. In Advances in Neural Information Processing Systems 26 (NIPS 2013) , pp. 2292--2300, 2013.
  10. D. P. Bertsekas. The auction algorithm: A distributed relaxation method for the assignment problem. Annals of Operations Research 14:105--123, 1988.
  11. J. A. Hanley and A. Lippman-Hand. If nothing goes wrong, is everything all right? Interpreting zero numerators. Journal of the American Medical Association 249(13): 1743--1745, 1983.

Version history

  1. v1Submitted by Chepin ZhangInitial depositCurrentOct 11, 2026