About
This page collects a small number of public mathematical drafts and related formalization projects. Some items are kept anonymous while they are being prepared for arXiv or journal submission.
Preprints and notes
-
A Rank (2g−1) Affine-Prym Construction and Its Scalar Two-Block Optimality
A construction and restricted optimality result for scalar two-block triangular Prym extensions.
-
An Endpoint Observation and a Petri-Type Bottleneck for Landesman–Litt Isomonodromy
An endpoint observation and a conditional rank s+1 refinement in the closed unpointed case.
Lean formalization
Lean 4 examples and the Affine-Prym formalization subproject are collected in FDmd233/lean4-math-showcase.
The Affine-Prym subproject records the linear-algebraic dependency skeleton of the lower-bound argument, with Looijenga and Westwick inputs treated as named external assumptions rather than re-proved in Lean.