Compression by the rank of modular contributions

For aggregate gates over one prime modulus, the two possible contributions of each circuit signal are columns of a matrix. Its column space is an actual joint register, with exactly p ^ rank states. Arbitrary readouts, repeated slots, and dependencies between special gates are included in this construction.

@[reducible, inline]

abbrev Algebraic.Aggregate.Compressed.Modular.State (p : ℕ) : Unit → Type

The additive modular register, written multiplicatively for the aggregate API.

Equations

• Algebraic.Aggregate.Compressed.Modular.State p x✝ = Multiplicative (ZMod p)

def Algebraic.Aggregate.Compressed.Modular.gate {p n : ℕ} (weights : Fin n → ZMod p) (target : ZMod p) : Op (State p)

A weighted modular equality gate; all weights one give the usual MOD gate.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Aggregate.Compressed.Modular.registerEquiv {p : ℕ} (op : Op (State p)) (h : op.isSpecial = true) : op.Register ≃* Multiplicative (ZMod p)

Every special gate in the modular signature has the same modular register.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Aggregate.Compressed.Modular.registersEquiv {p n g : ℕ} (c : Program (signature (State p)) n g) : Registers c ≃* Multiplicative (SpecialGate c → ZMod p)

All dependent special registers identify with a vector of residues.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Aggregate.Compressed.Modular.contributionMatrix {p n g : ℕ} (c : Program (signature (State p)) n g) : Matrix (SpecialGate c) (Wire n g × Bool) (ZMod p)

The two possible contribution columns for each signal, counting repeated slots.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Aggregate.Compressed.Modular.contributionSpace {p n g : ℕ} (c : Program (signature (State p)) n g) : Submodule (ZMod p) (SpecialGate c → ZMod p)

The concrete space spanned by the joint modular contributions.

Equations

• Algebraic.Aggregate.Compressed.Modular.contributionSpace c = Submodule.span (ZMod p) (Set.range (Algebraic.Aggregate.Compressed.Modular.contributionMatrix c).col)

noncomputable def Algebraic.Aggregate.Compressed.Modular.contributionRank {p n g : ℕ} (c : Program (signature (State p)) n g) : ℕ

Joint modular information is measured by the rank of the contribution matrix.

Equations

• Algebraic.Aggregate.Compressed.Modular.contributionRank c = (Algebraic.Aggregate.Compressed.Modular.contributionMatrix c).rank

@[reducible, inline]

abbrev Algebraic.Aggregate.Compressed.Modular.CompressedState {p n g : ℕ} (c : Program (signature (State p)) n g) : Type

A vector in the contribution space is one compressed aggregate state.

Equations

• Algebraic.Aggregate.Compressed.Modular.CompressedState c = Multiplicative ↥(Algebraic.Aggregate.Compressed.Modular.contributionSpace c)

@[instance_reducible]

noncomputable instance Algebraic.Aggregate.Compressed.Modular.instFintypeSubtypeForallSpecialGateUnitStateZModMemSubmoduleContributionSpaceOfNeZeroNat {p n g : ℕ} (c : Program (signature (State p)) n g) [NeZero p] : Fintype ↥(contributionSpace c)

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Aggregate.Compressed.Modular.decode {p n g : ℕ} (c : Program (signature (State p)) n g) : CompressedState c →* Registers c

The column-space inclusion decodes the joint special registers.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Aggregate.Compressed.Modular.factorization {p n g : ℕ} (c : Program (signature (State p)) n g) : Factorization c (CompressedState c)

Every modular circuit factors through its contribution space, without a rank premise.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Aggregate.Compressed.Modular.contributionRank_eq_finrank {p n g : ℕ} (c : Program (signature (State p)) n g) : contributionRank c = Module.finrank (ZMod p) ↥(contributionSpace c)

The rank counts the independent modular coordinates in the concrete compressed state.

theorem Algebraic.Aggregate.Compressed.Modular.card_compressedState {p n g : ℕ} (c : Program (signature (State p)) n g) [Fact (Nat.Prime p)] : Fintype.card (CompressedState c) = p ^ contributionRank c

Over a prime modulus, the joint state space has exactly one residue per rank coordinate.

theorem Algebraic.Aggregate.Compressed.Modular.contributionRank_le_specialCount {p n g : ℕ} (c : Program (signature (State p)) n g) [Fact (Nat.Prime p)] : contributionRank c ≤ specialCount c

Matrix rank never exceeds the number of modular gates.

theorem Algebraic.Aggregate.Compressed.Modular.budget_compressedState {p n g : ℕ} (c : Program (signature (State p)) n g) [Fact (Nat.Prime p)] : budget (CompressedState c) = 2 * Nat.clog 2 (p ^ contributionRank c)

The compiler charges the rank-based joint state twice, for guessing and checking.

theorem Algebraic.Aggregate.Compressed.Modular.contributionRank_le_of_factor {p n g : ℕ} (c : Program (signature (State p)) n g) [Fact (Nat.Prime p)] {r : ℕ} (left : Matrix (SpecialGate c) (Fin r) (ZMod p)) (right : Matrix (Fin r) (Wire n g × Bool) (ZMod p)) (h : contributionMatrix c = left * right) : contributionRank c ≤ r

A matrix factorization through r coordinates certifies a rank bound.

theorem Algebraic.Aggregate.Compressed.Modular.budget_compressedState_le {p n g : ℕ} (c : Program (signature (State p)) n g) [Fact (Nat.Prime p)] : budget (CompressedState c) ≤ 2 * contributionRank c * Nat.clog 2 p

For a fixed modulus, the compressed budget is bounded linearly by matrix rank.