Proof of `The Explicit Subcubic Family Expands`
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The powered seed has spectral bound one fifth. Zig-zag iteration gives bound two fifths, and path replacement gives the stated edge expansion.