Transporting the De Morgan parity lower bound

The literal De Morgan lower bound extends to every realized macro basis, both for chosen implementation costs and for intrinsic minimum AND/OR costs.

theorem Algebraic.parity_lowerBound_of_deMorgan_realization {n : ℕ} {ρ : Signature} {interpretation : Interpretation ρ Bool} (realization : Realization ρ DeMorgan.signature interpretation DeMorgan.interpretation) (circuit : Circuit ρ n 1) (computes : circuit.ComputesWith interpretation (GateElimination.Xor.parityTarget n)) : 3 * (n - 1) ≤ circuit.cost (realization.pullCost DeMorgan.binaryCost)

Every circuit over a basis realized by De Morgan circuits pays at least 3 * (n - 1) for parity, when each source gate is charged by the binary-gate cost of its implementation.

theorem Algebraic.parity_lowerBound_of_deMorgan_minimumCost {n : ℕ} {ρ : Signature} {interpretation : Interpretation ρ Bool} (realization : Realization ρ DeMorgan.signature interpretation DeMorgan.interpretation) (circuit : Circuit ρ n 1) (computes : circuit.ComputesWith interpretation (GateElimination.Xor.parityTarget n)) : 3 * (n - 1) ≤ circuit.cost (realization.minimumCost DeMorgan.binaryCost)

The intrinsic form of the transported parity bound. Each source operation is charged by its minimum possible De Morgan AND/OR implementation cost, not by an arbitrary initially selected gadget.

theorem Algebraic.parity_size_lowerBound_of_deMorgan_minimumCost {K n : ℕ} {ρ : Signature} {interpretation : Interpretation ρ Bool} (realization : Realization ρ DeMorgan.signature interpretation DeMorgan.interpretation) (positive : 0 < K) (bounded : ∀ (op : ρ.Op), realization.minimumCost DeMorgan.binaryCost op ≤ K) (circuit : Circuit ρ n 1) (computes : circuit.ComputesWith interpretation (GateElimination.Xor.parityTarget n)) : 3 * (n - 1) ⌈/⌉ K ≤ circuit.size

If every macro operation has intrinsic De Morgan AND/OR cost at most K, then the ordinary source gate count satisfies the ceiling-divided parity lower bound.

theorem Algebraic.parity_size_lowerBound_of_deMorgan_realization {K n : ℕ} {ρ : Signature} {interpretation : Interpretation ρ Bool} (realization : Realization ρ DeMorgan.signature interpretation DeMorgan.interpretation) (positive : 0 < K) (bounded : ∀ (op : ρ.Op), (realization.operation op).size ≤ K) (circuit : Circuit ρ n 1) (computes : circuit.ComputesWith interpretation (GateElimination.Xor.parityTarget n)) : 3 * (n - 1) ⌈/⌉ K ≤ circuit.size

Conventional unit-cost corollary: if every source operation has a chosen De Morgan implementation of at most K gates, then parity requires at least the ceiling of 3 * (n - 1) / K source gates.