Frame invariant (round six, `physical_inv`)

Proved

IntMul.Kappa.R6.Bit.physical_inv

by xuanji · Oct 19, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

Frame invariant. Physical content = frame permutation (by the tracked label) of the logical content.

The following holds (Lean statement, in the scope of module Solutions.R6BitLab):

theorem IntMul.Kappa.R6.Bit.physical_inv :
    ∀ (prog : List (Instr Wr R m)), (∀ e ∈ progEdges prog, EdgeOK N e) →
      ∀ (st lg : Wr → List R) (F : Wr → Matrix (Fin (m + m)) (Fin (m + m)) (ZMod N)),
        (∀ w, (lg w).length = vol sh) → (∀ w, st w = frameArr Λ (F w) (lg w)) →
        LabGates N prog F →
        ∀ w, netRunH (vol sh) (fun e => runArr Λ 0 (e.steps N)) prog st w =
          frameArr Λ (prog.foldl (labStepH N) F w)
            (netRunH (vol sh) (fun _ ys => ys) prog lg w)

Context. Round six, bit side: IdealOK from frame labels and a scalar routing identity

A sufficient condition for QHNet.IdealOK N in the style of OpenAI's network theorem (AModel.network_realizes), but with multiplicative (non-commuting) frames:

every edge e has lower triangular rational Bruhat factors with unit diagonals mod N (EdgesOK); its frame matrix is X_e = E₁ · σ_e · E₂ mod N (edgeMat);
labels (frames) are tracked along the program: initially 1 on every wire, an edge on w multiplies the label of w on the left by X_e; every gate touches wires with equal labels, and the final label of every role ρ w is swapMat (LabOK);
the scalar circuit (gates only; temporaries start at 0) routes role w to role ρ w (ScalarOK).

Then C.IdealOK N (idealOK_of_labels). The physical content of each wire is the array permutation Φ(F) = pull (amap F⁻¹) of its logical content (frameArr), Φ is multiplicative (frameArr_mul), commutes with pointwise gates (frameArr_gate), and the ideal edge is Φ(X_e) (runArr_steps_eq, from AModel.linear_via_bruhat_array).

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).

Preamble

-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.

import Definitions.Def_IntMul_Kappa_R6_Defs4

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Bit
open AModel AModelFac Matrix
variable {R : Type*} [CommRing R] {m : ℕ}
variable {Wr : Type*} [Fintype Wr] [DecidableEq Wr] {sh : Shape} {N : ℕ} [NeZero N]
  (Λ : Layout sh (m + m) N)

Formal statement

theorem IntMul.Kappa.R6.Bit.physical_inv :
    ∀ (prog : List (Instr Wr R m)), (∀ e ∈ progEdges prog, EdgeOK N e) →
      ∀ (st lg : Wr → List R) (F : Wr → Matrix (Fin (m + m)) (Fin (m + m)) (ZMod N)),
        (∀ w, (lg w).length = vol sh) → (∀ w, st w = frameArr Λ (F w) (lg w)) →
        LabGates N prog F →
        ∀ w, netRunH (vol sh) (fun e => runArr Λ 0 (e.steps N)) prog st w =
          frameArr Λ (prog.foldl (labStepH N) F w)
            (netRunH (vol sh) (fun _ ys => ys) prog lg w) := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `IntMul.Kappa.R6.Bit.physical_inv`, Solutions/R6BitLab.lean (lines 198–247) of the round-six development.

View graph