Prove adjacent gamma interlacing transfer

[PerAlexandersson]

Summary

Completes issue #315 along the exact proof of Hoster--Stump Proposition 2.5.

• corrects the challenge endpoint to include the source's nonnegative gamma
  coefficient and nonzero exact-degree hypotheses;
• formalizes equations (2.1)--(2.2), including reciprocal root pairs and the
  exceptional -1 multiplicity;
• transports ordered preferred-root lists through
  gammaRootMap ρ = ρ / (1 + ρ)^2;
• proves the reusable backend prec_gammaTransform_succ_iff;
• replaces def GammaAdjacentInterlacingTransferStatement : Prop with a
  checked theorem wrapper;
• removes the proved transfer theorem from StrategyInputs.

The endpoint derives the backend's nonzero constant coefficients from the
source's nonzero exact-degree hypotheses via
coeff_ambient_gammaTransform; it introduces no target-shaped assumption.

Source

E. Hoster and C. Stump, Chow polynomials of simplicial posets with positive
h-vector are real-rooted, arXiv:2508.15538, Proposition 2.5, equations
(2.1)--(2.2) (paper-cache record 90).

Validation

• focused RealRooted.Challenges.HosterStump build: 8620/8620 jobs;
• full aggregate build: 8951/8951 jobs.

All reported warnings are pre-existing and confined to untouched modules.

Closes #315.

[PerAlexandersson]

Source-shape follow-up: adding HasNonnegCoeffs gamma and HasNonnegCoeffs delta fixes the main Proposition 2.5 mismatch. For an exact source transcription, also exclude the Lean-only d = 0, f = 0 edge: the paper assumes deg f = d and deg g = d+1, so both polynomials are nonzero, whereas Lean has natDegree 0 = 0. Add f ≠ 0 (and preferably g ≠ 0 symmetrically/documentarily) or state explicitly that the theorem deliberately proves a harmless zero extension rather than claiming exact-degree hypotheses alone encode the source assumptions.

[PerAlexandersson]

Commit a56cfe67 adds the exact -1 root-multiplicity identity from Hoster--Stump Proposition 2.5, equation (2.2), with a source link in the Lean declaration. It derives the identity directly from the source factorization and the proved nonvanishing of the minimal core. No broader adjacent-interlacing endpoint is asserted in this slice, and no local build was run; comparator CI remains the validation oracle.

[PerAlexandersson]

Commit b3b2b2c6 adds the Proposition 2.5 ordered-root transport bridge. The recursive proof was checked in isolation with AXLE against Lean 4.31 and uses only strict monotonicity of gammaRootMap on (-1,0). No local Lake build or post-edit reread was run; comparator CI remains authoritative. Per the project cadence, the next continuation is cleanup/dedup/golf only.

[PerAlexandersson]

Cleanup-only commit b545c654: deduplicated the base-case handling in interleaves_map_gammaRootMap_iff using the project shim's existing simp lemmas. Net change: 3 insertions, 6 deletions, with no API or mathematical change. Comparator CI remains authoritative.

[PerAlexandersson]

Commit 332fd47d fixes the CI-confirmed forward reference by relocating interleaves_map_gammaRootMap_iff after its dependencies. It also adds the exact reciprocal quadratic factor and its composition with gammaTransform_X_sub_C_mul_two, following Hoster--Stump Proposition 2.5, equation (2.1). AXLE accepted the isolated new lemmas under Lean 4.31; comparator CI remains authoritative.

[PerAlexandersson]

Commit 3a5451d8 adds the arbitrary-multiplicity iteration of the equation (2.1) quadratic factor and its reciprocal-pair specialization. This is the algebraic engine for the pending rootMultiplicity/multiset equality. AXLE accepted the isolated proofs under Lean 4.31. Per cadence, the next continuation is cleanup-only.

[PerAlexandersson]

Cleanup-only commit 4a8403a0: retained the one-root API while deduplicating its proof through the m = 1 case of the arbitrary-multiplicity theorem. No mathematical or API change. Comparator CI remains authoritative.

[PerAlexandersson]

Commit 93739cfb adds the exact equation (2.1) root-multiplicity theorem and repairs dependency order for the power-iteration block. The complete proof was accepted in isolation by AXLE under Lean 4.31. The remaining source packaging is the filtered root-multiset identity, then reciprocal and -1 reconstruction.

[PerAlexandersson]

New proof slice: exists_mem_Ioo_gammaRootMap_eq formalizes the inverse/surjectivity part of Hoster--Stump (2.1) on (-1,0) via IVT on x-y(1+x)^2. AXLE Lean 4.31 accepted the isolated proof (request b860c65c-bdc7-4708-9165-08ee260ec3eb). No local Lake build or post-edit validation was run; comparator CI is authoritative. Next continuation is cleanup-only by cadence; afterward the route is the filtered root-multiset identity and equation (2.2).

[PerAlexandersson]

Cleanup-only slice pushed: shortened exists_mem_Ioo_gammaRootMap_eq with no API, hypothesis, or mathematical change. AXLE accepted the golfed theorem (request 78958025-b0f1-49b6-8162-17634412a0b8); its automated simplifier found no additional safe cleanup (request 905bc05a-30f2-4801-92b7-46ef1d0aa7c8). No local Lake build or post-edit validation ran; comparator CI remains authoritative.

[PerAlexandersson]

Compiled proof slice pushed. Added roots_eq_map_filter_roots_gammaTransform, the exact multiplicity-preserving root-multiset form of Hoster--Stump (2.1), and repaired two earlier proof defects exposed by local compilation. Verification: AXLE accepted the generic multiset argument (request c0c50105-6125-4e66-a2ba-38d7836fc729) and reciprocal repair (request cbec6cc6-2b03-490c-85fd-753100f7eb1f); the focused external-cache build lake ... build RealRooted.GammaRealRoots then completed successfully with no warnings in the touched module. Erik (sqrt-of-2) currently has no open PRs. Remaining endpoint: equation (2.2) root-list reconstruction and adjacent interlacing transfer.

[PerAlexandersson]

Pushed a9d1073f, following Hoster--Stump Proposition 2.5, equations (2.1) and (2.2). This slice generalizes reciprocal-pair root multiplicity to every negative root other than -1 and proves roots_gammaTransform_eq_reciprocal_add_neg_one_add: the full transform root multiset is the reciprocal branch below -1, exactly d - 2 * γ.natDegree copies of -1, and the preferred branch in (-1,0). The focused external-cache build of RealRooted.GammaRealRoots passed. PR #322 still owns the challenge endpoint file, so this PR does not touch it.

[PerAlexandersson]

Mandatory cleanup continuation pushed. The proof of roots_gammaTransform_eq_reciprocal_add_neg_one_add now unfolds its local preferred-root multiset once and removes four duplicated full RHS expansions and terminal rfl steps, with no theorem-surface or mathematical changes. The focused RealRooted.GammaRealRoots build passed.

[PerAlexandersson]

Pushed the next Proposition 2.5 proof slice. GammaRealRoots.lean now contains the ordered reciprocal/center/preferred root completion and two proved fixed-case equivalences matching Hoster--Stump after equations (2.1)--(2.2): equal gamma degrees add one central -1 on the right and reduce to ListAlternates; successive gamma degrees remove one central -1 on the right and reduce to ListInterlaces. The proof uses the existing List.Interleaves merged-chain API. The focused module build passed.

[PerAlexandersson]

Pushed the reusable endpoint prec_gammaTransform_succ_iff, a complete formalization of Hoster--Stump Proposition 2.5 for adjacent gamma transforms. The backward direction derives the equal/successive gamma-degree split from the two-sided -1 root-multiplicity bound rootMultiplicity_bounds_of_prec; both directions canonicalize preferred roots, apply equation (2.1), reconstruct full roots via equation (2.2), and use the two proved center cases. The focused dependency build completed successfully: 8619/8619 jobs.

[PerAlexandersson]

Mandatory cleanup continuation pushed. Removed the duplicated private ListInterlaces root-count proof block from GarloffWagner.lean; rootMultiplicity_sub_one_le_of_prec_right remains available unchanged as a one-line projection from the new generic rootMultiplicity_bounds_of_prec. Focused RealRooted.GarloffWagner build passed all 8618 jobs.

[PerAlexandersson]

Completed endpoint pushed as e6c8320a after rebasing onto merged PR #322.

GammaAdjacentInterlacingTransferStatement is now a checked theorem, not a
def ... : Prop placeholder. Its constant-coefficient premises are derived
from nonzero exact degree and the supplied gamma expansions before applying
prec_gammaTransform_succ_iff. The redundant StrategyInputs assumption
was removed.

Validation passed:

• focused challenge build: 8620/8620 jobs;
• full aggregate build: 8951/8951 jobs.