Remove forwarding wrapper theorems with no callers

[PerAlexandersson]

Continues the Statement-wrapper cleanup with plain forwarding theorems: declarations whose whole proof applies one other declaration.

Method. A source scan found 575 declarations of this shape on main. I excluded:

• Challenges/ entry points;
• files touched by the open PRs Hurwitz/Hadamard cluster: state proved results directly, drop Statement wrappers #1093, Remove Statement-wrapper scaffolding (GeneralizedSnakePosets) #1099, CommonInterleaver: state the Chudnovsky–Seymour pair chain directly (part 2) #1101 and Rewrite README: shorter, current, and organized by reader #1106;
• OEIS-number names;
• forwarders that are still used anywhere in the repository, in SuperEulerian/, or in the downstream workspace projects that import RealRooted (including real-rooted-oeis-proofs).

I reviewed each remaining candidate by hand and deleted 41:

• renamed or argument-reordered duplicates: strictInterl_shift', deriv_sum_collapse, the Liu–Wang tR aliases, the Set.Iio and right-family restatements, and the affine-family _nonneg aliases;
• forwarders that carry hypotheses they never use: the threshold sine bound, the finite Pólya–Schur low-degree backward cases, and the first Brändén basis image;
• fixed-index instances of normalized_coeff_nonneg_of_isPF;
• one-direction halves of hasCommonInterleaver_pair and its left version, plus structure-field projection aliases;
• the warmupP compatibility abbrev with its nine mirrored lemmas, and the complexifyLinearMap abbrev. Its X_pow simp lemma is kept, restated for complexificationLinearMap, so simp behaviour is unchanged;
• two Mathlib-folder shims that only restate their hypothesis.

Kept on purpose:

• simp and API lemmas about a different constant;
• worked examples and smoke tests;
• genuine corollaries;
• "predicate-face" forms that state a result through the canonical predicate, such as isPolyaFreqSeq_of_orderedCertificates;
• the public names for PF-sequence tactic internals.

Checks:

• The only proof change is the restated simp lemma. A focused lake-workspace build RealRooted.BorceaBranden.Applications.AffineFiniteSymbol passed (9125 jobs).
• Every other change is a deletion with zero remaining references, rechecked after merging current main.
• Root-import, import-architecture, proof-status and catalog checks pass.
• The full default build is left to CI.

🤖 Generated with Claude Code