The edge code computes the implemented edge `realEdge` (round six, `edgeR_runs`)

The edge code computes the implemented edge realEdge.

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

theorem IntMul.Kappa.R6.IL.edgeR_runs {N : ℕ} [NeZero N] (j0 : Fin Pp) (A B Cs : Shape) (P L : ℕ)
    (hpos : ∀ a ∈ P :: L :: hdShape A B Cs m N, 1 ≤ a) (e : Bit.Edge m) (Bb : ℕ)
    (hT : ∀ T ∈ tplE e.E₁ ++ tplE e.E₂, TOK T N Bb)
    (hcop : ∀ i j, Nat.Coprime (e.E₁ i j).den N ∧ Nat.Coprime (e.E₂ i j).den N)
    (hV : zsz ((vol (P :: L :: hdShape A B Cs m N) : ℕ) : ℤ) ≤ Bb)
    (hQ2 : zsz ((2 * N : ℕ) : ℤ) ≤ Bb)
    (child : ℕ × ℕ × ℕ → List (ZMod 2) → List (ZMod 2)) (cC : ℕ × ℕ × ℕ → ℕ)
    (t : IState HS) {LN LQ LX LB LC : List Item} (hNQ : t.G sNQ = .int (-(N : ℤ)) :: LN)
    (hQQ : t.G sQQ = .int (N : ℤ) :: LQ)
    (hX : t.G rXs = .int ((vol (P :: L :: A) : ℕ) : ℤ) :: LX)
    (hB : t.G rVB = .int ((vol B : ℕ) : ℤ) :: LB)
    (hC : t.G rVC = .int ((vol Cs : ℕ) : ℤ) :: LC)
    (hrun : ∀ ρ ∈ e.runs, ∀ (R : List Item) (ys : List (ZMod 2)),
      ys.length = vol (P :: L :: hdShape A B Cs m N) →
      IRuns I iprog (callR j0 m ρ) (t.upd 0 (ints (enc2 ys) ++ R))
        (t.upd 0 (ints (enc2 (child ρ ys)) ++ R)) (cC ρ) ∧
      (child ρ ys).length = vol (P :: L :: hdShape A B Cs m N))
    (R : List Item) (ys : List (ZMod 2)) (hys : ys.length = vol (P :: L :: hdShape A B Cs m N)) :
    IRuns I iprog (edgeR j0 m e) (t.upd 0 (ints (enc2 ys) ++ R))
      (t.upd 0 (ints (enc2 (Bit.realEdge ((hdLayout A B Cs m N).cons2 P L) child e ys)) ++ R))
      (cEdgeR m e (vol (P :: L :: hdShape A B Cs m N)) Bb cC) ∧
    (Bit.realEdge ((hdLayout A B Cs m N).cons2 P L) child e ys).length =
      vol (P :: L :: hdShape A B Cs m N)

Context. Round six, item language: the code of one edge (shift templates and one child call per run)

• the general descriptor DescG t e P L a b c (dJ = -1, dT = e, dP, dL, dA, dB, dC);
• npow and the natural-expression push lists (pushOK_NE);
• callR m ρ: push the child descriptor of the run ρ = (i, j, r) (width r f, shapes A ++ [N]^i, [N]^(m-i-r) ++ B ++ [N]^j, [N]^(m-j-r) ++ Cs), call procedure 0, pop; callR_runs;
• tplE E: the rational shift templates of the lower triangular E (tplE_eval: they denote shiftSteps (redM N E));
• edgeR m e: shifts of E₂, the child calls, shifts of E₁; edgeR_runs: it computes realEdge (R6BitLevel).

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*).