The injection identity (round six, `inject_identity`)
ProvedIntMul.Kappa.R6.Bit.inject_identityThe injection identity. In characteristic two (z + z = 0), the retained totals of the
points of T plus the excluded sums (c, T \ {c}) inject exactly x_T into target T.
The following holds (Lean statement, in the scope of module Solutions.R6BitNBWord):
theorem IntMul.Kappa.R6.Bit.inject_identity (h2 : ∀ z : M, z + z = 0) (trips : Finset (Finset (Fin h)))
(htr : ∀ S ∈ trips, S.card = 3) {T : Finset (Fin h)} (hT : T ∈ trips) (x : Finset (Fin h) → M) :
(∑ c ∈ T, ∑ S ∈ trips.filter (fun S => c ∈ S), x S) +
(∑ c ∈ T, ∑ S ∈ trips.filter (fun S => c ∈ S ∧ ∀ t ∈ T, t ≠ c → t ∉ S), x S) = x T
Context. Round six, bit side: data-free scalar facts of the invocation word
The scalar part of one invocation (L, J, L⁻¹, V, L, J, L⁻¹, V, dirty scratch, characteristic
two) and the coefficient identity behind it, stated for any modules (in particular for the module
of formal frame values of R6BitNBFormal, where the two-stage motif needs them):
word_dirty: with an invertible producerAon the scratch, an injectionB(scratch → targets) and a source copyC(inputs → scratch), the word restores arbitrary scratch and addsB (A (C x))to the targets;coeff_mod_two: for triplesS, T,|S ∩ T| + [|S ∩ T| = 1] ≡ [S = T] (mod 2);inject_identity: if targetTreceives the retained point totalsstar c(c ∈ T) and the excluded sumsstar c \ (star t₁ ∪ star t₂)(T = {c, t₁, t₂}), the total injected intoTisx_T(in characteristic two). This is the identityM = Iof the scalar exchange.
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction.
import Definitions.Def_IntMul_Kappa_K_Defs33
import Definitions.Def_IntMul_Kappa_R6_Defs1
import Mathlib
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open IntMul IntMul.Kappa IntMul.Kappa.R6
variable {h : ℕ}
variable {M : Type*} [AddCommGroup M]
theorem IntMul.Kappa.R6.Bit.inject_identity (h2 : ∀ z : M, z + z = 0) (trips : Finset (Finset (Fin h)))
(htr : ∀ S ∈ trips, S.card = 3) {T : Finset (Fin h)} (hT : T ∈ trips) (x : Finset (Fin h) → M) :
(∑ c ∈ T, ∑ S ∈ trips.filter (fun S => c ∈ S), x S) +
(∑ c ∈ T, ∑ S ∈ trips.filter (fun S => c ∈ S ∧ ∀ t ∈ T, t ≠ c → t ∉ S), x S) = x T := by sorry