Skip to content

v0.2.38 two-frame routing arithmetic

Choose a tag to compare

View all tags
@whyihaveyou whyihaveyou released this 08 Oct 17:28
· 9 commits to scope-130-parameter-certificate since this release
v0.2.38-two-frame-routing-arithmetic
5b29b27

This release adds TwoFrameRoutingArithmetic.lean, a Lean-checked H24 arithmetic certificate for the dense two-frame target-routing candidate.

For the conditional accounting model, it proves:

  • switch-only charge 1202, margin 2,425,171,790, normalized margin 1212585895/118747255799808 > 10^-6;
  • block-roundtrip charge 55,292, margin 2,425,117,700, normalized margin 606279425/59373627899904 > 10^-6.

The label-level cover remains the pair u=e_0, w=1+e_0 at even width. These are route-candidate width margins, not an unconditional exponent theorem. A complex gate, direct source formation, global frame schedule, and all-length DFT recurrence remain open.

Validation:

cd lean
lake build OAI.Computability.FourierCircuit.TwoFrameRoutingArithmetic
Assets 2
Loading