The Nasr–Carlini Möbius Bridge is not specific to the AES S-box. It holds for every S-box of the form S = L2 ∘ Frobj ∘ inv ∘ L1, with L1, L2 GF(2)-affine bijections and the Frobenius exponent j as the only degree of freedom. ARIA instantiates four members of that class at once (S1, S2, S1−1, S2−1 at exponents 0, 3, 0, 5). This deposit is the Lean 4 formalization and exhaustive GF(28) Python verifier for that class identity. No attack complexities for ARIA are claimed. ---------------------------This version (v1.0.4, 2026-10-07). GitHub Release v1.0.4 zip. Lean spine unchanged from v1.0.3 (Theorem 3.1 / Corollary 3.2 / §5). Adds an independent-kernel accept of the Bridge export: con-leche --verified CHECK_EXIT=0 (283412 declarations, 2026-09-17), checker pin leanprover/con-leche c431b1ca, lean4export 3.1.0 / Lean 4.32.2; see results/con-leche-verified.md. Also ships CC-BY-4.0 LICENSE and lake build + Python verifier CI. Optional gate; NDJSON not in the zip. Prefer software concept DOI 10.5281/zenodo.21705939 for always-latest zip. Companion paper: 10.5281/zenodo.21705468 (concept) / 10.5281/zenodo.21765164 (v1.0.5 PDF).---------------------------- TL;DRs for different audiences For the SME. Class theorem companion: the Nasr–Carlini Möbius Bridge holds for every invert-and-affine S-box S = L2 ∘ Frobj ∘ inv ∘ L1, with j the only degree of freedom. This zip is the Lean 4.32.2 spine of Theorem 3.1 / Corollary 3.2 / §5 plus a five-check exhaustive GF(28) oracle. ARIA S1, S2, S1−1, S2−1 at j = 0, 3, 0, 5 with published A, B, a=0x63, b=0xE2: 0/64770 mismatches per Table 1 row. Axioms: propext / Classical.choice / Quot.sound; no sorry. Independent kernel: con-leche --verified accepted the Bridge export (CHECK_EXIT=0). No attack complexities are claimed. For the interested layman. A fingerprint trick written for AES also works for ARIA's four related S-boxes. This archive is the proof-and-check code: Lean proves the algebra, a small Python script brute-checks every byte of GF(256), and a second Lean kernel re-checked the exported proofs. Cite the paper for the claim; this DOI for the replay. For the skeptic. The Python oracle is exhaustive (0/64770 per published ARIA row, seed 5785). The Lean files build with a three-axiom kernel set and no sorry. An independent verified-mode kernel (con-leche) accepted the exported Bridge environment. Paper PDF and this zip are separate Zenodo concepts. If you do not trust the claim, run python verify_bridge_class.py and lake build; the kernel check is optional and documented in results/con-leche-verified.md. For the decision maker. A reusable, citable formal artifact for a published class identity — not an attack paper. Cite the paper concept DOI for the theorem; this software concept DOI for the verifier and Lean. Two concepts, one GitHub repo, CC BY 4.0. For the funder. Small, replayable Lean + Python deposit aligned to a versioned preprint. Laptop runtime is seconds. Next cost is optional further Lean (concrete ARIA matrices), not a new campaign. Deliverables are binary: lake build clean, verifier exit 0, independent-kernel accept, DOIs pinned.
ARIA · block cipher · Mobius Bridge · GF(2^8) · Frobenius · Lean 4 · S-box · formal verification · mathlib · invert-and-affine · class bridge · fingerprint invariance · meet-in-the-middle · cryptanalysis · axiom audit · con-leche · independent kernel