Prove adjacent-degree gamma interlacing transfer

[PerAlexandersson]

Priority

Erik priority 4.

Source

E. Hoster and C. Stump, Chow polynomials of simplicial posets with positive
h-vector are real-rooted, arXiv:2508.15538, Proposition 2.5.

The paper proves that for nonnegative palindromic polynomials of adjacent
degrees, f << g iff gamma(f) << gamma(g).

Goal

Add a checked theorem witnessing
GammaAdjacentInterlacingTransferStatement using the existing
IdTransform, IsGammaExpansion, and Prec APIs.

Acceptance criteria

• Prove both directions of Prec f g <-> Prec gamma delta.
• Retain the current exact degree, symmetry, gamma-expansion, and coefficient
  hypotheses unless a source comparison proves a correction is required.
• Check the local Prec orientation against the paper before formalizing.
• Add a theorem, not another def ...Statement : Prop, axiom, or target-shaped
  hypothesis.

[PerAlexandersson]

Source audit update: Hoster--Stump Proposition 2.5 defines interlacing on nonnegative-coefficient polynomials, whereas this repository's Prec predicate is unrestricted. The Lean statement therefore also needs HasNonnegCoeffs γ and HasNonnegCoeffs δ.

Without those premises the former statement is false: take d = 2 and γ = δ = 1 - X. Then Prec γ δ holds, while gammaTransform 2 γ = X^2 + X + 1 is not real-rooted, even though its coefficients are nonnegative and the remaining transform/symmetry/degree premises hold.

Draft PR #325 makes this source-faithful correction and adds the source/counterexample comment. It does not claim the transfer theorem is proved yet.

[PerAlexandersson]

Commit 8a84a02c formalizes the first genuine proof step from
Hoster--Stump Proposition 2.5.

Added:

• gammaRootMap ρ = ρ / (1 + ρ)^2;
• gammaRootMap_inv, matching reciprocal root pairing;
• strictMonoOn_gammaRootMap, proving the map is strictly increasing on
  (-1,0).

The monotonicity proof is the exact algebraic source argument:
φ(b)-φ(a) has sign
(b-a)(1-ab) / ((1+a)^2(1+b)^2).

The transform evaluation/root-pullback identity already existed as
eval_gammaTransform_eq_mul_eval_gammaUntransform, so it was reused rather
than duplicated. Remaining source work is equation (2.2), the multiplicity of
-1, and the two ordered-root-list cases. No local build was run; comparator
CI is pending.

[PerAlexandersson]

Commit 1ed471bd adds the algebraic content of Hoster--Stump
equation (2.2):

• gammaTransform_add_two_mul iterates the existing two-degree padding
  identity;
• gammaTransform_eq_X_add_one_pow_mul_minimal proves
  gammaTransform d γ = (X+1)^(d-2*natDegree γ) * gammaTransform (2*natDegree γ) γ;
• gammaTransform_minimal_eval_neg_one_ne_zero proves the remaining factor
  does not vanish at -1.

Thus the source multiplicity exponent has been isolated without assuming any
root or interlacing conclusion. The next source step is to package this as the
exact rootMultiplicity (-1) equality and then handle the two ordered-list
degree cases. No local build was run; comparator CI is pending.

[PerAlexandersson]

Mandatory third-run cleanup commit a604e805 normalizes
gammaTransform_eq_X_add_one_pow_mul_minimal around
n = natDegree γ and m = d / 2.

This removes repeated unfolding and duplicated transform/exponent expressions
(net four lines) without changing any theorem statement, hypothesis, source
route, or conclusion. Comparator CI has restarted on the cleanup head; no local
build was run.

[PerAlexandersson]

Pushed the next source-faithful slice in commit a56cfe67 (PR #325):

• added rootMultiplicity_neg_one_gammaTransform;
• this is exactly Hoster--Stump, Proposition 2.5, equation (2.2):
  μ_{gammaTransform d γ}(-1) = d - 2 * natDegree γ;
• the proof uses the previously established ambient-degree factorization and nonvanishing of the minimal gamma core at -1;
• the Lean doc comment links the source: https://arxiv.org/abs/2508.15538.

This does not yet claim GammaAdjacentInterlacingTransferStatement. The next source step is the ordered root-list transport in the two cases distinguished by the gamma degrees.

[PerAlexandersson]

Pushed proof run 2 in commit b3b2b2c6 (PR #325).

Added interleaves_map_gammaRootMap_iff, the exact monotonicity step used after equations (2.1)--(2.2) in Hoster--Stump Proposition 2.5. For ascending root lists contained in (-1,0), mapping by x / (1+x)^2 preserves and reflects List.Interleaves. The declaration links the paper source.

The source case split is now fixed in HANDOFF.md:

• equal gamma degrees: the larger-degree transform has one extra -1;
• gamma degrees differing by one: the smaller-degree transform has one extra -1.

The remaining polynomial endpoint is the multiset identity reconstructing transform roots from mapped gamma roots, reciprocal partners, and the equation (2.2) copies of -1. The next continuation is the required cleanup/golf run, not a new proof slice.

[PerAlexandersson]

Required third-run cleanup completed in commit b545c654 (PR #325).

The cleanup replaces four manually enumerated base cases in interleaves_map_gammaRootMap_iff with two cases using the existing List.Interleaves simp API. The theorem statement, hypotheses, source route, and conclusion are unchanged. AXLE accepted the isolated golf under Lean 4.31; no local Lake build or post-edit reread was run.

The next continuation returns to proof work on the source multiset identity for mapped roots, reciprocal partners, and equation (2.2) copies of -1.

[PerAlexandersson]

Pushed commit 332fd47d to PR #325.

Repair:

• moved interleaves_map_gammaRootMap_iff after gammaRootMap and strictMonoOn_gammaRootMap, fixing the forward-reference failure reported by CI;
• statement and proof are unchanged.

New source-faithful equation (2.1) content:

• gammaQuadraticFactor_eq_mul_reciprocal factors the quadratic gamma-root factor as the reciprocal pair (X-x)(X-x⁻¹) with the exact scalar;
• gammaTransform_X_sub_C_gammaRootMap composes this with the existing gammaTransform_X_sub_C_mul_two, so extracting one gamma root explicitly produces its two transform roots.

Both new lemmas were accepted in isolated AXLE checks against Lean 4.31. No local Lake build or post-edit reread was run.

[PerAlexandersson]

Pushed proof run 2 in commit 3a5451d8 (PR #325).

• gammaTransform_X_sub_C_pow_mul_two iterates the existing quadratic transform factor through an arbitrary extracted multiplicity m.
• gammaTransform_X_sub_C_pow_gammaRootMap specializes this to Hoster--Stump equation (2.1): a gamma root represented by x ∈ (-1,0) yields the reciprocal transform-root pair x, x⁻¹, with the extracted multiplicity preserved.
• The induction-stage degree bound uses only natDegree_mul_le, natDegree_pow_le, and the original degree-box hypothesis.

AXLE accepted both isolated lemmas under Lean 4.31. No local Lake build or post-edit reread was run. The next continuation is the required cleanup/golf pass; after that, proof work can package the exact rootMultiplicity and multiset-count identities.

[PerAlexandersson]

Required cleanup pass pushed in commit 4a8403a0 (PR #325).

gammaTransform_X_sub_C_gammaRootMap remains as a public one-root convenience lemma, but its duplicated quadratic-factor proof is replaced by the m = 1 specialization of gammaTransform_X_sub_C_pow_gammaRootMap. The statement, hypotheses, source route, and conclusion are unchanged. AXLE accepted the isolated wrapper under Lean 4.31; no local Lake build or post-edit reread was run.

The next continuation returns to proof work on the exact away-from--1 rootMultiplicity equality in Hoster--Stump equation (2.1).

[PerAlexandersson]

Pushed commit 93739cfb to PR #325.

Declaration-order repair:

• moved the power-iteration and reciprocal-specialization block after its existing dependency gammaTransform_X_sub_C_mul_two, eliminating a forward reference before CI reported it.

New source endpoint:

• added rootMultiplicity_gammaTransform_of_mem_Ioo;
• for nonzero γ in the degree box and x ∈ (-1,0), it proves
  rootMultiplicity x (gammaTransform d γ) = rootMultiplicity (gammaRootMap x) γ;
• this is the exact multiplicity form of Hoster--Stump Proposition 2.5, equation (2.1).

Proof route: extract the full gamma-root multiplicity, apply the reciprocal-pair factor iteration at residual ambient degree, use the existing root-pullback theorem to show the residual transform is not rooted at x, and isolate (X-C x)^m. AXLE accepted the complete isolated proof under Lean 4.31. No local Lake build or post-edit reread was run.

Next: convert the pointwise count equality to the filtered root-multiset identity γ.roots = S.map gammaRootMap.

[PerAlexandersson]

Pushed the inverse-branch component of Hoster--Stump equation (2.1): exists_mem_Ioo_gammaRootMap_eq proves that every y < 0 is gammaRootMap x for some unique-branch representative x in (-1,0). The proof follows the source normalization directly: apply IVT to q(x)=x-y(1+x)^2, using q(-1)=-1 and q(0)=-y>0, then rearrange. Together with the existing strict monotonicity and exact rootMultiplicity theorem, this supplies the missing surjectivity needed for the filtered root-multiset identity. Remaining gap after the required cleanup continuation: package those three ingredients as the exact multiset form of (2.1), then combine with the -1 multiplicity formula (2.2).