Theorems 1.1–1.3 — Symplectic polynomial modules and Hamiltonian application
OpenSymplecticFreeModules.symplecticFreeModulesMainFor every integer , prove that there is a concrete presentation of with its abelian maximal-parabolic nilradical and a single two-parameter family of polynomial representations
that realizes the source's explicit generator formulas and is free of rank one over the nilradical. For this same family, prove the complete isomorphism and weight-module classification, the simplicity criterion outside
the Noetherian, Artinian, and composition-factor conclusions at exceptional parameters, and the canonical Shen--Larsson Hamiltonian-module application, including its exact degree-weight spaces and simplicity properties. The existential witnesses are quantified only once, so every clause refers to the same presentation and the same representation family.
import Definitions.Def_frame_2026_symplectic_free_modules_interfaces
namespace SymplecticFreeModules
open scoped TensorProduct
theorem symplecticFreeModulesMain
(l : ℕ) (hl : 2 ≤ l) :
∃ P : GeneratorPresentation l,
IsAbelianNilradicalSystem P ∧
∃ tau : ℂ → Poly l → LieRepresentation (Sp l) (Poly l),
IsTauFamily P tau ∧
HasCoreClassification P tau ∧
HasExceptionalFiniteLength tau ∧
HasCanonicalHamiltonianApplication tau := by sorry
end SymplecticFreeModules
Read-back
What the Lean code literally says, in plain math · gpt-5.6-sol
Theorems.SymplecticFreeModulesMain / theorem declarations
SymplecticFreeModules.symplecticFreeModulesMain. For every natural together with a proof that , there exist, in this order, one generator presentation and one common family . The presentation chooses concrete elements whose underlying matrices are exactly
and
All commute, and the family with one index per symmetric pair is complex-linearly independent. The family
is chosen once before any parameters, where . For every and every polynomial , is a genuine Lie representation and acts for all by
and
where
For each , there is also a complex-linear equivalence witnessing rank-one freeness in the literal sense
for every ; the witness may depend on .
The same satisfy all five core claims. First, for every small-universe complex module and every representation of on , if there is a complex-linear equivalence intertwining multiplication by each with , then there exist and a complex-linear equivalence intertwining with for every Lie element . Second,
Third, the span of simultaneous eigenvectors for all diagonal is the whole polynomial module exactly when is constant. Fourth, when is constant, there exists the last index , with , such that is killed by , has -eigenvalue , is killed by all displayed reverse-adjacent , has equal adjacent diagonal weights, and generates the whole module in the sense that every invariant submodule containing is the whole module. Fifth,
This simplicity criterion is independent of .
For every exceptional with positive natural , and every , every ascending and every descending chain of invariant complex submodules of stabilizes; at least one finite strictly increasing composition series from to the full module exists; and for any two such finite series there is a permutation of their step indices under which corresponding quotient representations are complex-linearly intertwining-equivalent. Because existence of a composition series is also required, the Jordan–Hölder clause is not left true merely because no series exists. The statement does not enumerate the factors.
Finally, the explicit vector space with basis for nonzero and for the coordinate indices, with , has the explicitly defined bracket
extended by finite double sums. The theorem requires this operation to be additive and complex homogeneous in each argument, alternating, and Jacobi. For every nonexceptional , every polynomial , and arbitrary , there exists a complex-linear bracket-preserving action of this explicit algebra on
and elements whose matrices are , such that for every exponents and polynomial ,
This is nontrivial and simple, is spanned by simultaneous -weight vectors, and, for every , its common eigenspace of weight is exactly the set , as equality of sets. The action may depend on .
The existential witnesses and may depend on , but are fixed simultaneously for the classification, exceptional-length, and Hamiltonian conclusions; their uniqueness is not asserted. The hypothesis excludes the empty and one-index ranks, so none of the displayed finite-index systems is empty. The classification implication ranges only over representations satisfying the explicit freeness premise, but that class is not empty within the conclusion because every is itself required to be free. Exceptional and nonexceptional branches are conditional at each ; both classes of complex parameters have members.
SymplecticFreeModules.polynomialModuleMain. For every , there exist one concrete presentation with the exact matrices above, commuting and linearly independent symmetric , and one family of genuine polynomial representations satisfying the exact , multiplication-, and diagonal- formulas and the explicit rank-one freeness condition for every . Every free-rank-one representation is equivalent to some member of this family; two members are equivalent exactly when their ’s agree and their ’s differ by a constant; the family is a weight representation exactly for constant ; constant gives the explicit cyclic lowest-weight vector of weight ; and simplicity is equivalent to not being for any positive natural . At every exceptional parameter and every , the representation is Noetherian, Artinian, has a finite composition series, and has the stated permutation-and-quotient-intertwiner Jordan–Hölder uniqueness. This theorem makes no assertion about the explicit Hamiltonian bracket or Shen–Larsson tensor action.
SymplecticFreeModules.classificationAndSimplicity. For every , there exist one exact concrete generator presentation with an independent commuting symmetric -system and one family of genuine representations satisfying the exact candidate generator formulas and rank-one freeness for all . The family classifies every representation satisfying the same literal freeness condition up to an intertwining complex-linear equivalence; its parameters are unique exactly modulo adding a constant to ; it is a weight representation exactly for constant ; constant gives the explicit lowest-weight cyclic generator ; and it is simple exactly at the nonexceptional values of . This declaration omits both the exceptional finite-length/Jordan–Hölder conjunction and the canonical Hamiltonian application.
SymplecticFreeModules.exceptionalFiniteLength. For every , there exist one exact concrete presentation with commuting linearly independent symmetric -generators and one family of genuine representations satisfying all exact candidate generator formulas and the literal rank-one freeness condition for every , such that whenever for some positive natural , is Noetherian and Artinian, has at least one finite composition series, and any two such series have the same quotient representations up to a permutation and intertwining equivalences. This declaration does not itself assert the core classification, parameter uniqueness, weight, lowest-weight, or simplicity equivalences, despite using the same family shape.
SymplecticFreeModules.hamiltonianApplicationMain. For every , there exist one exact presentation with its commuting independent -system and one common exact-formula, rank-one-free family satisfying all five core classification, uniqueness, weight, lowest-weight, and simplicity claims. In addition, the explicit bracket above satisfies complex bilinearity, alternation, and Jacobi; and for every nonexceptional , every , and every , there exists a simple weight representation on satisfying the exact Shen–Larsson pure-tensor formulas and having exactly the degree- weight spaces . This declaration omits the exceptional Noetherian, Artinian, finite-composition-series, and Jordan–Hölder conjunction.
Confirmed by the mission captain (proposal self-audit).