The post-first-feedback circuit state

The geometric first-jet theorem is connected here to the actual circuit flag. The target witness entering at gate five is replaced, modulo the preceding state, by its rational tangent. Thus later gates see the old seed state plus one explicit first-Hasse-jet direction.

def UnrestrictedBooleanMul.N4.FirstJetState (C : Circuit 8 8) : Prop

The normalized seed and fifth-gate target data at a rational first jet.

Equations

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

theorem UnrestrictedBooleanMul.N4.NormalizedEight.firstJetState {C : Circuit 8 8} (h : NormalizedEight C) : FirstJetState C

The first useful suffix gate installs the first Hasse jet in the actual circuit flag. All coordinate work is delegated to the correlated algebraic normal form; this proof only performs state replacement.