6.6.1. The five curves🔗

Each plot is log-scale wall-time per reduction against the family dimension:

• fpLLL: the raw floating-point reducer, unverified; the speed baseline.

• Lean native: Hex.lllNative, the exact all-integer d/ν reducer. Correct by construction, but its exact arithmetic pays for wide operands and high swap counts.

• Lean certified: an fpLLL candidate checked by the verified Lean checker Hex.certCheck. It inherits floating-point speed and adds only a cheap integer check, so it stays close to the fpLLL curve while remaining fully verified.

• verified Isabelle native: the Isabelle extraction's own reducer; the independent verified point of comparison.

• verified Isabelle certified: the same fpLLL candidate checked by the Isabelle checker instead of the Lean one; the apples-to-apples yardstick for the Lean certified path.

6.6.2. The six input families🔗

Each family is a faithful port of an fplll generator, and stresses a different part of the algorithm:

• random-bounded: near-orthogonal random bases; the easy baseline, few swaps.

• harsh-cubic: entries of bit-length about 3.3·n; exact-integer operand-width growth (shown above).

• ajtai: fplll gen_trg worst-case triangular bases; the swap / iteration count Θ(d² log B) (shown in the introduction).

• q-ary: LWE/SIS bases [[I, H], [0, qI]]; the cryptographic Z-shape.

• ntru: bases [[I, Rot h], [0, qI]]; a planted dense sublattice plus a q-block.

• knapsack: the rectangular d × (d+1) integer-relation form; the only family with more columns than rows, using the m > n construction.

Across every family the exact reducers are correct but climb steeply on the hard bases, while Lean certified stays within about 1.2 to 2.5 times raw fpLLL: verified output at close to floating-point cost.

6.6.3. Selecting the certified versus native path🔗

This is a runtime choice, not a Lean import. HexLLL always builds its FFI shim, and the same Hex.lll call picks its path by whether an external provider symbol is resolvable in the process:

• set the environment variable HEX_FPLLL_FFI_LIB to a built fpLLL-ffi shared library and lll takes the certified path: the shim dlopens it, providerAvailable returns true, and the candidate is certified by Hex.certCheck;

• leave it unset (or if certification ever fails) and lll runs the exact Hex.lllNative directly.

Either way the returned basis is (δ, 11/20)-reduced.

6.6.4. The size-reduction bound and its constants🔗

The public Hex.lll certifies its output (δ, 11/20)-reduced: every Gram-Schmidt coefficient satisfies |μ| ≤ 11/20. Two numbers in its signature follow from η = 11/20. The precondition is 121/400 < δ, because 121/400 = (11/20)² = η² and the bound is well-defined only when η² < δ. The short-vector constant is 1/(δ − 121/400). So the 121/400 stands exactly where the classical bound would put 1/4 = (1/2)².

Why 11/20 rather than the classical 1/2? Solely the external provider. The exact Hex.lllNative already lands at |μ| ≤ 1/2, but a black-box reducer cannot be forced to exactly 1/2 (fpLLL's default size-reduction target sits slightly above it), so the certified path accepts its candidate at the looser 11/20. When you want the tighter guarantee, call Hex.lllNative directly: its short-vector theorem lllNative_short_vector carries the precondition 1/4 < δ and the strictly better constant 1/(δ − 1/4).

6.6.5. The other families🔗

The remaining comparator plots, for reference: