The first algebraic lemmas in this file simply expand the pair operations
used in the paper's peeling identities. They let Lean normalize expressions
such as A_u(v_η) and σ(v_η) into the polynomial formulas appearing in
\eqref{eq:Au-identity-factored} and \eqref{eq:sig-identity-factored}.
A PeelingStepWitness packages one quadratic family v_η from the proof
of \Cref{prop:second_order_property_factor}. The key data are:
qQuad, whose pairing with the residual is already known to vanish from the
previous stage; the constant A_u(v_η) term; and the exact quadratic expansion
of σ(v_η) in the parameter η.
Instances For
RotatedPeelingData is the paper-friendly way to build a peeling witness.
The pair quad is the pure peeling direction, const is the correction term,
quad is orthogonal to u, its square already lies in the previous image,
and the mixed term is exactly the target polynomial q.
Instances For
HasPeelingWitness u uImgPrev uImgNext means that every element of the new
image im(A_{uImgNext}) admits one of the quadratic families required for a
single peeling step. This is the local input used to transport orthogonality
from one stage of the factor-peeling argument to the next.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A QuadraticFactorStep records one peeled factor r from the paper's
decomposition of the bad factor h. The relation gNext * r = X^2 * gStart
formalizes the replacement of one complex quadratic factor by x_1^2
(represented here by X^2).
- r : Poly
Instances For
A FOCP is automatically orthogonal to its own image: this is just the
first-order condition \eqref{eq:gradA} rewritten as a statement about the
entire image of A_u.
One peeling witness is enough to prove orthogonality to a specific target
q. The proof follows the paper's Hessian-family argument: substitute the
family v_η into the SOCP inequality, note that the quadratic coefficient is
already zero by the previous stage, and conclude from nonnegativity for all
η that the linear coefficient ⟨q, σ(u)-p⟩ must vanish.
The explicit one-parameter family v_η = η·quad + const used in the
peeling step. This is the formal version of the v_η family in the proof of
\Cref{prop:second_order_property_factor}.
Instances For
Any RotatedPeelingData yields a PeelingStepWitness. The proof is a
direct expansion of A_u(v_η) and σ(v_η) using the orthogonality and mixed
term identities recorded in the structure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One algebraic factor step gStart -> gNext produces the rotated data
needed for the analytic peeling argument. This is where divisibility of the
peeled factor by σ(u₀) is converted into the statement that the quadratic
term already lies in the previous image.
If rotated peeling data exist for every target in the next image, then we
get a full HasPeelingWitness statement. This is just packaging.
A single QuadraticFactorStep gives the witness package required for one
peeling move. This is the local algebraic input used later by the recursive
schedule construction.
Orthogonality propagates across one peeling step: if the residual is already orthogonal to the previous image, and every element of the next image has a peeling witness, then it is also orthogonal to the next image.
A PeelingPath is an iterated chain of one-step peeling moves. It mirrors
the paper's repeated passage from
A_{u g} to A_{u X^2 / r_1} to A_{u X^4 /(r_1 r_2)}, and so on.
- refl {u : UPair} (uStart : UPair) : PeelingPath u uStart uStart
- step {u uStart uMid uEnd : UPair} : PeelingPath u uStart uMid → HasPeelingWitness u uMid uEnd → PeelingPath u uStart uEnd
Instances For
Concatenation of peeling paths. This is the formal analogue of composing several factor-replacement steps in the paper.
A PeelingSchedule is the same iteration written at the level of scalar
factors rather than scaled pairs. It records the successive updates of the
common factor in the proof of \Cref{prop:second_order_property_factor}.
- done {u u0 : UPair} (g : Poly) : PeelingSchedule u u0 g g
- peel {u u0 : UPair} {gStart gMid gEnd : Poly} : HasPeelingWitness u (scalePair gStart u0) (scalePair gMid u0) → PeelingSchedule u u0 gMid gEnd → PeelingSchedule u u0 gStart gEnd
Instances For
After peeling a list of bad factors, the terminal scale is obtained by
replacing each peeled factor by one copy of X^2. This is the Lean version of
the paper's x_1^k / h replacement.
Equations
- LowRankUnivariateSOS.peelTerminalScale gBase [] = gBase
- LowRankUnivariateSOS.peelTerminalScale gBase (head :: rs) = LowRankUnivariateSOS.peelTerminalScale (Polynomial.X ^ 2 * gBase) rs
Instances For
Every peeling schedule induces a path of scaled pairs. This simply turns the scalar recursion into the pair-valued recursion used by the orthogonality lemmas.
The terminal scale never becomes zero if the initial coprime scale is nonzero. This prevents the peeled target from degenerating during the iteration.
A list of peeled factors, together with a local theorem for each factor,
builds the full recursive peeling schedule. This is the formal implementation
of the paper's instruction to peel the factors of h one at a time.
Orthogonality propagates along an entire peeling path by iterating the one-step propagation lemma. This is the abstract form of the paper's repeated factor-peeling argument.