Refactor threshold matrix theorem layers

[PerAlexandersson]

Summary

• split the historical ThresholdMatrix theorem monolith into a generic core
  and independent Haglund--Zhang/A046802 and Gustafsson--Solus layers behind
  the existing compatibility import
• extract the affine proper-position facts shared with VeroneseMatrix into
  AffineProperPosition
• narrow direct consumer imports and centralize the duplicated fixed-right
  Prec0 addition lemma in PFPolynomial
• document the new boundaries and add exact import-closure budgets

Verification

• lake-workspace build for all new layers, direct consumers,
  VeroneseMatrix, and both VeroneseSectionPair modules
• lake-workspace build RealRooted (9,420 jobs)
• import-architecture self-test and live check
• proof-status self-test and live check
• root-import check (861 source modules)
• declaration-preservation audit against c03abebb
• five representative #print axioms checks; each reports only propext,
  Classical.choice, and Quot.sound
• git diff --check and 100-column audit

The focused owner-labeled Aristotle proof-golf task remains optional and is
not part of this checkpoint.