Counting permanently constant gate outputs

The pairing proof charges a restriction to newly constant outputs. Constancy is preserved on smaller flats, so these charges cannot be reused by later gates.

noncomputable def Algebraic.Aggregate.Geometry.constantCount {n g : ℕ} (p : Program signature n g) (S : AffineFlat n) : ℕ

Number of actual gate outputs already constant on a flat.

Equations

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

theorem Algebraic.Aggregate.Geometry.constantCount_le {n g : ℕ} (p : Program signature n g) (S : AffineFlat n) : constantCount p S ≤ g

Each actual gate can contribute at most one permanently constant output.

theorem Algebraic.Aggregate.Geometry.constantCount_mono {n g : ℕ} {S T : AffineFlat n} (p : Program signature n g) (sub : T.carrier ⊆ S.carrier) : constantCount p S ≤ constantCount p T

Further restrictions cannot decrease the constant-output count.

theorem Algebraic.Aggregate.Geometry.constantCount_lt {n g : ℕ} {S T : AffineFlat n} (p : Program signature n g) (sub : T.carrier ⊆ S.carrier) (gate : Fin g) (before : ¬ConstantOn S (p.gateFunction interpretation gate)) (after : ConstantOn T (p.gateFunction interpretation gate)) : constantCount p S < constantCount p T

Freezing one previously live gate strictly increases the count.

theorem Algebraic.Aggregate.Geometry.constantCount_gate {n g : ℕ} (p : Program signature n g) (line : Line signature n g) (S : AffineFlat n) : constantCount (p.gate line) S = constantCount p S + if ConstantOn S (lineFunction p line) then 1 else 0

Appending a line contributes exactly its own constant-output indicator.