Merged edge (round six, `edgeStepsH_den`)
ProvedIntMul.Kappa.R6.Cx.edgeStepsH_denMerged edge (same denotation as P8Lift.edgeSteps_den).
The following holds (Lean statement, in the scope of module Solutions.R6CxMerge):
theorem IntMul.Kappa.R6.Cx.edgeStepsH_den (w : R) {V U : Submodule (ZMod 2) (Vc h)} (hE : EdgeP V U) :
denListH (chEx (κ := κ)) (edgeStepsH w V U) = wireOp w (PhiK (qL V - qL U))
Context. NC3: the PR #15 whole-residual merge
For a linearly independent family v₁, …, v_ρ in 𝔽₂^m (e.g. an orthonormal residual basis of
a Proposition 8 edge) and signs ε_k = ±1, the edge operator
∏_k (aI + bX_{v_k})^{ε_k} (on every column: colT (∏ Tk ε_k v_k)) is conjugate, by a word of
binary row additions P (an element of GL_m(𝔽₂) sending v_k ↦ e_{h_k}), to
(-i)^{|N||κ|} Z_N C^{⊗(S × κ)} Z_N with S = {h_k} (|S| = ρ) and N = {h_k : ε_k = -1}:
one forward child call of width ρ.
conj_rowAdds: conjugation of a kernel product by row additions (15).kernels_single: kernels on distinct unit vectorse_{h_k}= the slot family (they live on distinct slots and commute).exists_rowAdds: every independent family is sent to distinct unit vectors by a word of row additions (basis extension +gl_f2_row_additions).merge_identity(operator form) andmerge_chunk(step form: row additions, one childchild w S neg, row additions reversed).mergedChunk,mergedChunk_den,mergedChunk_widths: the chosen chunk for a kernel listL(inP8Lift.frameStepsform) with independent vectors;mergedChunk_den_frameSteps: same denotation as the single-slot chunksframeSteps w L, but child widths[|L|]instead of|L|ones. Orthonormal versionlin_indep_of_orthonormal.edgeStepsH: the merged frame change of a Proposition 8 edge (EdgeP): denotationwireOp w (PhiK (qL V - qL U))asP8Lift.edgeSteps, one child of
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_R6_Defs2
set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000
open IntMul IntMul.Kappa IntMul.Kappa.R6 IntMul.Kappa.R6.Cx
open Matrix Finset Complex Butterfly P8Lift
variable {m : ℕ} {κ : Type} [Fintype κ] [DecidableEq κ]
open NetComplexP8 NetComplexLabels
variable {h : ℕ} {R : Type} [Fintype R] [DecidableEq R]
theorem IntMul.Kappa.R6.Cx.edgeStepsH_den (w : R) {V U : Submodule (ZMod 2) (Vc h)} (hE : EdgeP V U) :
denListH (chEx (κ := κ)) (edgeStepsH w V U) = wireOp w (PhiK (qL V - qL U)) := by sorry