Semantic bridge from active slices to the algebraic exclusions #
The hypotheses below are equalities of six-variable slice functions. Möbius
polarization recovers their cubic, quadratic, and linear ANF coefficients.
Those three coefficient equations are exactly the inputs consumed by
no_typeA_active_slice_pair and no_typeB_active_slice_pair.
theorem
UnrestrictedBooleanMul.N4.no_typeA_slice_model_pair
{x y x' y' : F₂}
(hdistinct : x ≠ x' ∨ y ≠ y')
(leftConst rightConst correctionConst targetConst eps : F₂)
(leftLinear rightLinear correctionLinear targetLinear : LinearForm)
(correctionCoeff : Fin 3 → F₂)
(hslice :
∀ (z : Fin 6 → F₂),
eval
(sliceTypeAFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear
correctionCoeff x y)
(sliceAssignment x y z) = eval (sliceTangentModel targetConst targetLinear eps x y) (sliceAssignment x y z))
(hslice' :
∀ (z : Fin 6 → F₂),
eval
(sliceTypeAFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear
correctionCoeff x' y')
(sliceAssignment x' y' z) = eval (sliceTangentModel targetConst targetLinear eps x' y') (sliceAssignment x' y' z))
:
Two distinct active Type-A slice models cannot both equal slices of the same zero-place target tangent.
theorem
UnrestrictedBooleanMul.N4.no_typeB_slice_model_pair
{x y x' y' : F₂}
(hdistinct : x ≠ x' ∨ y ≠ y')
(leftConst rightConst correctionConst targetConst eps : F₂)
(leftLinear rightLinear correctionLinear targetLinear : LinearForm)
(correctionCoeff : Fin 3 → F₂)
(hslice :
∀ (z : Fin 6 → F₂),
eval
(sliceTypeBFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear
correctionCoeff x y)
(sliceAssignment x y z) = eval (sliceTangentModel targetConst targetLinear eps x y) (sliceAssignment x y z))
(hslice' :
∀ (z : Fin 6 → F₂),
eval
(sliceTypeBFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear
correctionCoeff x' y')
(sliceAssignment x' y' z) = eval (sliceTangentModel targetConst targetLinear eps x' y') (sliceAssignment x' y' z))
:
Two distinct active Type-B slice models cannot both equal slices of the same zero-place target tangent.
theorem
UnrestrictedBooleanMul.N4.no_typeInfinity_slice_model_pair
{x y x' y' : F₂}
(hdistinct : x ≠ x' ∨ y ≠ y')
(leftConst rightConst correctionConst targetConst eps : F₂)
(leftLinear rightLinear correctionLinear targetLinear : LinearForm)
(correctionCoeff : Fin 3 → F₂)
(hslice :
∀ (z : Fin 6 → F₂),
eval
(sliceTypeInfinityFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear
correctionCoeff x y)
(sliceAssignment x y z) = eval (sliceTangentModel targetConst targetLinear eps x y) (sliceAssignment x y z))
(hslice' :
∀ (z : Fin 6 → F₂),
eval
(sliceTypeInfinityFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear
correctionCoeff x' y')
(sliceAssignment x' y' z) = eval (sliceTangentModel targetConst targetLinear eps x' y') (sliceAssignment x' y' z))
:
theorem
UnrestrictedBooleanMul.N4.exists_representedLowFactor_of_mem
{p : ANF 8}
(hp : p ∈ rationalLowSpace)
:
∃ (a : F₂) (ell : LinearForm) (alpha : Fin 3 → F₂), p = representedLowFactor a ell alpha
theorem
UnrestrictedBooleanMul.N4.eval_sliceTypeAFullModel_eq_normalized
(leftConst : F₂)
(leftLinear : LinearForm)
(rightConst : F₂)
(rightLinear : LinearForm)
(correctionConst : F₂)
(correctionLinear : LinearForm)
(correctionCoeff : Fin 3 → F₂)
(x y : F₂)
(z : Fin 6 → F₂)
:
eval
(sliceTypeAFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x
y)
(sliceAssignment x y z) = eval
(representedLowFactor leftConst leftLinear (rationalSingleton 0) * representedLowFactor rightConst rightLinear (rationalSingleton 1) + representedLowFactor correctionConst correctionLinear correctionCoeff)
(sliceAssignment x y z)
theorem
UnrestrictedBooleanMul.N4.eval_sliceTypeBFullModel_eq_normalized
(leftConst : F₂)
(leftLinear : LinearForm)
(rightConst : F₂)
(rightLinear : LinearForm)
(correctionConst : F₂)
(correctionLinear : LinearForm)
(correctionCoeff : Fin 3 → F₂)
(x y : F₂)
(z : Fin 6 → F₂)
:
eval
(sliceTypeBFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x
y)
(sliceAssignment x y z) = eval
(representedLowFactor leftConst leftLinear (rationalSingleton 0) * representedLowFactor rightConst rightLinear (rationalSingleton 1 + rationalSingleton 2) + representedLowFactor correctionConst correctionLinear correctionCoeff)
(sliceAssignment x y z)
theorem
UnrestrictedBooleanMul.N4.eval_sliceTypeInfinityFullModel_eq_normalized
(leftConst : F₂)
(leftLinear : LinearForm)
(rightConst : F₂)
(rightLinear : LinearForm)
(correctionConst : F₂)
(correctionLinear : LinearForm)
(correctionCoeff : Fin 3 → F₂)
(x y : F₂)
(z : Fin 6 → F₂)
:
eval
(sliceTypeInfinityFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear
correctionCoeff x y)
(sliceAssignment x y z) = eval
(representedLowFactor leftConst leftLinear (rationalSingleton 0) * representedLowFactor rightConst rightLinear (rationalSingleton 2) + representedLowFactor correctionConst correctionLinear correctionCoeff)
(sliceAssignment x y z)
theorem
UnrestrictedBooleanMul.N4.typeA_slice_eq_of_active
{factor target : ANF 8}
{delta rho sigma : F₂}
(leftConst : F₂)
(leftLinear : LinearForm)
(rightConst : F₂)
(rightLinear : LinearForm)
(correctionConst : F₂)
(correctionLinear : LinearForm)
(correctionCoeff : Fin 3 → F₂)
(targetConst eps : F₂)
(targetLinear : LinearForm)
{x y : F₂}
(hsource :
target = (representedLowFactor leftConst leftLinear (rationalSingleton 0) * representedLowFactor rightConst rightLinear (rationalSingleton 1) + representedLowFactor correctionConst correctionLinear correctionCoeff) * factor)
(htarget : target = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps))
(hfactor : factor = affineANF delta (rho • sliceX + sigma • sliceY) + rationalANF (rationalSingleton 0))
(hactive : feedbackCorner delta rho sigma x y = 1)
(z : Fin 6 → F₂)
:
eval
(sliceTypeAFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x
y)
(sliceAssignment x y z) = eval (sliceTangentModel targetConst targetLinear eps x y) (sliceAssignment x y z)
theorem
UnrestrictedBooleanMul.N4.typeB_slice_eq_of_active
{factor target : ANF 8}
{delta rho sigma : F₂}
(leftConst : F₂)
(leftLinear : LinearForm)
(rightConst : F₂)
(rightLinear : LinearForm)
(correctionConst : F₂)
(correctionLinear : LinearForm)
(correctionCoeff : Fin 3 → F₂)
(targetConst eps : F₂)
(targetLinear : LinearForm)
{x y : F₂}
(hsource :
target = (representedLowFactor leftConst leftLinear (rationalSingleton 0) * representedLowFactor rightConst rightLinear (rationalSingleton 1 + rationalSingleton 2) + representedLowFactor correctionConst correctionLinear correctionCoeff) * factor)
(htarget : target = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps))
(hfactor : factor = affineANF delta (rho • sliceX + sigma • sliceY) + rationalANF (rationalSingleton 0))
(hactive : feedbackCorner delta rho sigma x y = 1)
(z : Fin 6 → F₂)
:
eval
(sliceTypeBFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear correctionCoeff x
y)
(sliceAssignment x y z) = eval (sliceTangentModel targetConst targetLinear eps x y) (sliceAssignment x y z)
theorem
UnrestrictedBooleanMul.N4.typeInfinity_slice_eq_of_active
{factor target : ANF 8}
{delta rho sigma : F₂}
(leftConst : F₂)
(leftLinear : LinearForm)
(rightConst : F₂)
(rightLinear : LinearForm)
(correctionConst : F₂)
(correctionLinear : LinearForm)
(correctionCoeff : Fin 3 → F₂)
(targetConst eps : F₂)
(targetLinear : LinearForm)
{x y : F₂}
(hsource :
target = (representedLowFactor leftConst leftLinear (rationalSingleton 0) * representedLowFactor rightConst rightLinear (rationalSingleton 2) + representedLowFactor correctionConst correctionLinear correctionCoeff) * factor)
(htarget : target = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps))
(hfactor : factor = affineANF delta (rho • sliceX + sigma • sliceY) + rationalANF (rationalSingleton 0))
(hactive : feedbackCorner delta rho sigma x y = 1)
(z : Fin 6 → F₂)
:
eval
(sliceTypeInfinityFullModel leftConst leftLinear rightConst rightLinear correctionConst correctionLinear
correctionCoeff x y)
(sliceAssignment x y z) = eval (sliceTangentModel targetConst targetLinear eps x y) (sliceAssignment x y z)
theorem
UnrestrictedBooleanMul.N4.exists_distinct_active_corner_pair
{delta rho sigma : F₂}
(h : ExactlyThreeActiveCorners delta rho sigma)
:
Extract a concrete pair of distinct active corners from the three-corner statement.
theorem
UnrestrictedBooleanMul.N4.no_normalized_typeA_feedback_target
{factor target : ANF 8}
{delta rho sigma : F₂}
(leftConst : F₂)
(leftLinear : LinearForm)
(rightConst : F₂)
(rightLinear : LinearForm)
(correctionConst : F₂)
(correctionLinear : LinearForm)
(correctionCoeff : Fin 3 → F₂)
(targetConst eps : F₂)
(targetLinear : LinearForm)
(hsource :
target = (representedLowFactor leftConst leftLinear (rationalSingleton 0) * representedLowFactor rightConst rightLinear (rationalSingleton 1) + representedLowFactor correctionConst correctionLinear correctionCoeff) * factor)
(htarget : target = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps))
(hfactor : factor = affineANF delta (rho • sliceX + sigma • sliceY) + rationalANF (rationalSingleton 0))
(hright : target * factor = target)
:
theorem
UnrestrictedBooleanMul.N4.no_normalized_typeB_feedback_target
{factor target : ANF 8}
{delta rho sigma : F₂}
(leftConst : F₂)
(leftLinear : LinearForm)
(rightConst : F₂)
(rightLinear : LinearForm)
(correctionConst : F₂)
(correctionLinear : LinearForm)
(correctionCoeff : Fin 3 → F₂)
(targetConst eps : F₂)
(targetLinear : LinearForm)
(hsource :
target = (representedLowFactor leftConst leftLinear (rationalSingleton 0) * representedLowFactor rightConst rightLinear (rationalSingleton 1 + rationalSingleton 2) + representedLowFactor correctionConst correctionLinear correctionCoeff) * factor)
(htarget : target = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps))
(hfactor : factor = affineANF delta (rho • sliceX + sigma • sliceY) + rationalANF (rationalSingleton 0))
(hright : target * factor = target)
:
theorem
UnrestrictedBooleanMul.N4.no_normalized_typeInfinity_feedback_target
{factor target : ANF 8}
{delta rho sigma : F₂}
(leftConst : F₂)
(leftLinear : LinearForm)
(rightConst : F₂)
(rightLinear : LinearForm)
(correctionConst : F₂)
(correctionLinear : LinearForm)
(correctionCoeff : Fin 3 → F₂)
(targetConst eps : F₂)
(targetLinear : LinearForm)
(hsource :
target = (representedLowFactor leftConst leftLinear (rationalSingleton 0) * representedLowFactor rightConst rightLinear (rationalSingleton 2) + representedLowFactor correctionConst correctionLinear correctionCoeff) * factor)
(htarget : target = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps))
(hfactor : factor = affineANF delta (rho • sliceX + sigma • sliceY) + rationalANF (rationalSingleton 0))
(hright : target * factor = target)
:
theorem
UnrestrictedBooleanMul.N4.zeroAnchored_seed_second_is_infinity
{g correction factor target : ANF 8}
{targetConst eps delta rho sigma : F₂}
{targetLinear : LinearForm}
(hseed : ZeroAnchoredQuarticSeedForm g correction)
(hsource : target = (g + correction) * factor)
(htarget : target = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps))
(hfactor : factor = affineANF delta (rho • sliceX + sigma • sliceY) + rationalANF (rationalSingleton 0))
(hright : target * factor = target)
:
∃ (leftConst : F₂) (rightConst : F₂) (correctionConst : F₂) (leftLinear : LinearForm) (rightLinear : LinearForm)
(correctionLinear : LinearForm) (correctionCoeff : Fin 3 → F₂),
target = (representedLowFactor leftConst leftLinear (rationalSingleton 0) * representedLowFactor rightConst rightLinear (rationalSingleton 2) + representedLowFactor correctionConst correctionLinear correctionCoeff) * factor
After the two main slice exclusions, the only zero-anchored seed-plane representative that can remain is the infinity singleton.
theorem
UnrestrictedBooleanMul.N4.no_zeroAnchored_quartic_feedback_target
{g correction factor target : ANF 8}
{targetConst eps delta rho sigma : F₂}
{targetLinear : LinearForm}
(hseed : ZeroAnchoredQuarticSeedForm g correction)
(hsource : target = (g + correction) * factor)
(htarget : target = affineANF targetConst targetLinear + targetANF (rationalTangentAt 0 eps))
(hfactor : factor = affineANF delta (rho • sliceX + sigma • sliceY) + rationalANF (rationalSingleton 0))
(hright : target * factor = target)
:
Complete zero-place quartic exclusion: all three complementary seed directions are impossible.