[PerAlexandersson]

Closed as superseded — 2026-10-24. Do not use the historical checklist below as current project status.

The author approved retirement without merging. The draft uses older endpoint/fault-line conventions; see the reconciliation review. Branch formalize/ferrers-tilings at 332976573fe1cd261346830f81ccc86a49f8ba9b is preserved. No new general library theorem requiring extraction was identified.

---

Historical worker report (unmodified)

Draft, unverified by the integrator. Layer 1 of the formalization of Ahlberg–Alexandersson, Polynomials from tilings of rectangles (arXiv:2605.03473), drafted by a Codex worker. The worker reports a passing full default build (11120 jobs) and guards.

Still to do: golfw/verify_lane.sh, my review of the code, and the partial targets (T1, T4, T5, T6). Layer 2, the combinatorial model with tilings, anchor words, 1/(1-B) and claw-freeness, goes to AlexanderssonFormalizations as Papers/FerrersTilings, by the user's decision of 2026-10-22.

Ferrers tilings, layer 1 report

Target status

T1 — partial

The paper's refined transfer recursion is formalized, and every vector
(Q_(d,n,∞), Q_(d,n,1), ..., Q_(d,n,d)) is proved to be a zero-aware
nonnegative interlacing sequence whose nonzero entries are real-rooted. Thus
Q_(d,n) = Q_(d,n+1,∞) is real-rooted. Independently, the closed-form
algebraic P_(d,n) and Q_(d,n) are definitionally equal and are proved PF,
real-rooted with nonpositive zeros, and consecutively interlacing.

The missing bridge is a proof that the total produced by the refined transfer
recursion equals the closed-form anchorPolynomial; the umbral recurrence
P_(d,n+1) = Σ_(k≤d) binom(d,k) t^k P_(d,n-k) is also not yet formalized.

Public declarations:

• anchorTransferEntry: entry formula for the paper's transfer matrix.
• anchorTransferMatrix: the (d+1) × (d+1) refined transfer matrix.
• anchorRefinedList: refined vectors initialized by (1,0,...,0).
• anchorRefinedList_succ: exact matrix recursion for refined vectors.
• anchorRefinedPolynomial: a terminal-state component of the refined vector.
• anchorRefined_interlacing: every refined vector is zero-aware interlacing,
  coefficientwise nonnegative, and real-rooted componentwise.
• anchorRefinedPolynomial_interl: ordered refined components interlace.
• anchorRefinedPolynomial_splits: every refined component splits over ℝ.
• anchorRefinedTotal: the component Q_(d,n+1,∞).
• anchorRefinedTotal_splits: the total refined polynomial is real-rooted.
• lTilingPolynomial, anchorPolynomial: closed-form algebraic P and Q.
• lTilingPolynomial_eq_anchorPolynomial: the closed-form P and Q agree.
• coeff_lTilingPolynomial: coefficient j is binom(d(n-j),j).
• lTilingPolynomial_isPFPolynomial, lTilingPolynomial_splits,
  lTilingPolynomial_roots_nonpos: PF, real-rootedness, and nonpositive roots.
• lTilingPolynomial_interl_succ: consecutive closed-form polynomials interlace.

Files: RealRooted/FerrersTiling/AnchorRefined.lean and
RealRooted/FerrersTiling/LTiling.lean.

T2 — done

twoColumnPolynomial is defined by the closed form, with initial values,
recurrence, real-rootedness, and consecutive interlacing proved. Its formula
does not depend on k; the hypothesis d ≤ k belongs to the later tiling-model
identification.

Public declarations:

• twoColumnPolynomial: pathPowerCliquePolynomial 2 n scaled by d.
• coeff_twoColumnPolynomial, twoColumnPolynomial_eq_sum: coefficient and
  finite-sum formulas Σ_j binom(n-j,j)d^j t^j.
• twoColumnPolynomial_zero, twoColumnPolynomial_one: initial values.
• twoColumnPolynomial_add_two: P_(n+2)=P_(n+1)+d t P_n.
• twoColumnPolynomial_splits: real-rootedness.
• twoColumnPolynomial_interl_succ: consecutive interlacing.

File: RealRooted/FerrersTiling/TwoColumn.lean.

T3 — done

The coefficient-reversed two-column family is defined and its initial values,
recurrence R_(n+2)=tR_(n+1)+dtR_n, and real-rootedness are proved.

Public declarations:

• twoColumnPolynomial_natDegree_le: degree bound needed for reflection.
• faultLinePolynomial: reflect n (twoColumnPolynomial d n).
• faultLinePolynomial_zero, faultLinePolynomial_one: initial values.
• faultLinePolynomial_add_two: the paper's fault-line recurrence.
• faultLinePolynomial_splits: real-rootedness.

File: RealRooted/FerrersTiling/FaultLines.lean.

T4 — partial

The closed coefficient formula, recurrence, initial values, consecutive
interlacing, PF property, and real-rootedness are proved for the nondegenerate
range k ≥ 2. PF and real-rootedness hold in the formalization for all
natural k,d. The paper's boundary case k=1 is not covered by the stated
recurrence/initial/interlacing theorems.

Public declarations:

• rectangleFaultFreePolynomial: the corresponding path-power polynomial.
• coeff_rectangleFaultFreePolynomial: the L2015 bars-and-stars coefficient.
• rectangleFaultFreePolynomial_eq_add: B_d=B_(d-1)+tB_(d-k).
• rectangleFaultFreePolynomial_eq_one_add: B_d=1+dt for d≤k.
• rectangleFaultFreePolynomial_interl: B_(d-1) ≼ B_d.
• rectangleFaultFreePolynomial_isPFPolynomial,
  rectangleFaultFreePolynomial_splits: PF and real-rootedness.

File: RealRooted/FerrersTiling/FaultFreeRectangle.lean.

T5 — partial

The closed coefficients binom(d(n-jℓ),j), the finite polynomial sum, PF
property, real-rootedness, and nonpositive roots are proved. The equivalent
formal power-series coefficient identity with
1/(1-x(1+t x^ℓ)^d) is not encoded.

Public declarations:

• rigidPolynomial: the closed-form rigid family.
• coeff_rigidPolynomial, rigidPolynomial_eq_sum: coefficient and sum forms.
• rigidPolynomial_isPFPolynomial, rigidPolynomial_splits,
  rigidPolynomial_roots_nonpos: PF, real-rootedness, and nonpositive roots.

File: RealRooted/FerrersTiling/Rigid.lean.

T6 — partial

The univariate specialization
Σ_j binom(n-j,j)(s+d-1)^j and its real-rootedness are formalized. The full
multivariate closed form and generating functions are not. The L2335 theorem
states that for ℓ≥1, μ_ℓ=1, and μ_(ℓ-1)≥d,
Σ_n S_(μ,d,n)(s_1,...,s_d)x^n = 1/(1-x∏_(r=1)^d(1+s_r x^ℓ)); specializing s_1=s and the other variables to
one gives 1/(1-x(1+x^ℓ)^(d-1)(1+s x^ℓ)).

Public declarations:

• rowRefinedSpecialization: the univariate specialization.
• rowRefinedSpecialization_eq_sum: its closed finite sum.
• rowRefinedSpecialization_splits: real-rootedness.

File: RealRooted/FerrersTiling/RowRefined.lean.

T7 — skipped

This optional target is not a real-rootedness result. Formalizing the stated
unimodality/no-internal-zero argument would require a separate finite-support
coefficient and log-concavity development, so it was kept out of layer 1.

T8 — skipped for layer 2

The cylindric polynomial was not defined. The paper's proof needs the
cylindric anchor-word conflict graph and its claw-freeness; the alternative
route needs a substantial formal power-series derivative/coefficient theorem.
Both fit the combinatorial layer better than this algebraic checkpoint.

Reused library results

• matrix_preserves_interlacing_seq0_of_2x2_weak,
  Atomic2x2Matrix.hasAffineProperty_of_isAffineAdmissible, and
  isInterlacingSeq0NonnegRealRooted_oneSupportSeq for T1.
• coeff_pathPowerCliquePolynomial,
  pathPowerCliquePolynomial_add_lag,
  splits_pathPowerCliquePolynomial,
  isPFPolynomial_pathPowerCliquePolynomial, and
  strictInterl_pathPowerCliquePolynomial_add for T1, T2, T4, T5, and T6.
• Polynomial.Splits.comp_of_natDegree_le_one and
  Interl.comp_C_mul_X for scaled/translated specializations.
• pathPowerCliquePolynomial_subsequence_natDegree_le, polynomial reflection
  identities, and Polynomial.Splits.reflect for T3.

No existing real-rootedness theorem was duplicated.

Integration

The seven new modules are imported by RealRooted.lean and
RealRooted/Production.lean; import budgets were updated. The curated catalog
page is RealRooted/Challenges/FerrersTilings.lean. The SymCat snapshot was
refreshed with AhlbergAlexandersson2026, updating
website/symcat/bibliography.json and website/symcat/labels.json.

Verification

Full default build (./build.sh):

Build completed successfully (11120 jobs).

Guard suite (./guards.sh):

check_import_architecture ok
check_example_namespaces ok
check_proof_status ok
check_root_imports ok
check_upstream_headers ok
ok: validated 106 curated catalog pages
lint-style rc=0

git diff --check also passed. No git write command was run.

Layer 2 plan

1. Define rectangular boards, translated Ferrers tiles, placements, tilings,
   fault lines, and anchor words, with finite encodings suitable for sums.
2. Prove the tiling/anchor-word bijections and connect tile count, row weights,
   and fault-line statistics to the algebraic polynomials in this layer.
3. Define fault-free blocks and prove unique block decomposition, followed by
   the general 1/(1-B) generating-function theorem and the rigid/row-refined
   specializations.
4. Define ordinary and cylindric conflict graphs; identify their independence
   polynomials and prove the required claw-freeness statements, including the
   cylindric (h,1), d=h case.
5. Use those bridges to prove the two missing T1 identifications, the formal
   generating-function identities from T5/T6, and cylindric real-rootedness.

Estimated size: 10--14 modules and roughly 2,500--4,000 lines of Lean,
including finite-set infrastructure, bijections, graph proofs, and focused
regression examples.

🤖 Generated with Claude Code

[PerAlexandersson]

Closing as superseded at the author's request, without merging or deleting the branch.

This draft is based on older conventions and should not be integrated unchanged:

• anchorRefinedTotal uses the infinity component one step later, requiring reconciliation with the corrected same-width convention.
• faultLinePolynomial reflects at width n and has R_1=X; for internal fault lines on a nonempty width-n board, the reflection exponent is n-1 and R_1=1.

The reusable matrix-preservation, path-power coefficient/recurrence/PF/interlacing, reflection and affine-composition results used here already exist in the library. The seven family modules are specializations and paper-specific wrappers; review identified no new general theorem requiring extraction before closing.

Preserve branch formalize/ferrers-tilings at 332976573fe1cd261346830f81ccc86a49f8ba9b as candidate/provenance material. This closure is not a claim that this PR's revision was integrator-validated. Any future extraction should use corrected conventions and a focused validated change.