Normal form for a seed-using useful child

The old-state shift may contain the seed with coefficient zero or one. In the latter case the identity (g + a) * (c + 1) = (g + a) * c + g + a absorbs that coefficient. Thus a useful seed-using child always supplies an actual target-ambient product F = (g + a) * c outside the rational-low state. This is the precise input to the quartic idempotence argument.

def UnrestrictedBooleanMul.N4.SeedUsingTargetWitness (g : ANF 8) : Prop

A seed-using product that gives a target outside the affine-plus-rational-target space.

Equations

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

theorem UnrestrictedBooleanMul.N4.NormalizedEight.seedUsingTargetWitness {C : Circuit 8 8} (h : NormalizedEight C) {target representative shift : ANF 8} (htarget : target ∈ targetAmbient 8 (mulTarget 4)) (htargetOld : target ∉ circuitFlag C 4) (hshift : shift ∈ circuitFlag C 4) (htargetEq : target = shift + representative) (hrepresentative : IsSeedUsingProduct (C.gate 3) representative) : SeedUsingTargetWitness (C.gate 3)

Convert the circuit-level useful-child data to the target product used by the manuscript's seed-using quartic argument.

theorem UnrestrictedBooleanMul.N4.seedUsing_idempotence {g a c F : ANF 8} (hF : F = (g + a) * c) : (g + a) * F = F ∧ F * c = F

The two Boolean idempotence equations attached to a seed-using target product.