Sparsity of the local steps (round six, `den_row_card_le`)

Sparsity of the local steps. Every local step has at most |R| nonzero entries per row (gates), and the other local steps at most one (monomial matrices).

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

theorem P8Lift.RStep.den_row_card_le (T : Op κ) (st : RStep R m) (hst : st.isChild = false)
    (p : R × Addr m κ) : (rowSupp (st.den T) p).card ≤ Fintype.card R

Context. A restricted Proposition 8 interface (only the paper's cheap local operations)

Butterfly.Prop8Iface allows an arbitrary matrix as a non-recursive step, which makes it vacuous. Here the non-recursive steps are restricted to the operations of §3.5/§5.1, each of which touches every state entry a bounded number of times:

• gate G — a pointwise scalar gate across roles at equal addresses (G on the roles, identity on the addresses);
• rowAdd w i j — a binary row addition x(j,c) += x(i,c) (all columns c) on the address bits of role w, i.e. an address permutation;
• phase w k₀ k₁ a — the diagonal phase i^{k₀ + k₁|κ| + Σ_{(r,c)} a_r x(r,c)} on role w (covers Z_u with a = 2u, S on selected bits, scalars i^{27|κ|});
• perm σ — a permutation of the roles;
• child w h fwd — a recursive call on slot h of role w (forward or the (17) inverse).

The step list is independent of the column type κ (the same program for every κ).

• Prop8IfaceR.toIface: the forgetful map to Butterfly.Prop8Iface (so recOp_eq, recCost_le, prop14_output apply).
• den_row_card_le: every local step's matrix has at most |R| nonzero entries per row (≤ 1 except for gates), so one local step costs ≤ W · V entry operations.
• recCostR_le: the §5.3 bound for the recursion whose local work is the actual work ≤ nloc · W · V of the local steps (nloc = number of local steps, independent 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*).