v1.0.3 — full class bridge formalization Lean spine for the published note (paper v1.0.5): Theorem 3.1: class_bridge / class_bridge' / class_bridge_with_key Corollary 3.2: J_class_invariant (via J_affine_invariant) §5 bad indices: L1_inv_zero, IsBadIndex, bad_index_set Pairwise β-cancel: class_bridge_pair_diff Verifier: verify_bridge_class.py auto-writes results/verify_bridge_class_meta.json Axiom audit: propext / Classical.choice / Quot.sound only; no sorry Paper: https://doi.org/10.5281/zenodo.21705468 (concept) / https://doi.org/10.5281/zenodo.21765164 (v1.0.5 PDF) No attack complexities for ARIA are claimed.
ARIA · block cipher · Mobius Bridge · GF(2^8) · Frobenius · Lean 4 · S-box