oxilean-std 0.1.2

//! Auto-generated module
//!
//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)

use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};

use super::types::{
    ArnoldConjecture, CanonicalTransformation, ContactForm, ContactManifold, ContactManifoldData,
    DiophantineCondition, EllipsoidEmbedding, FloerComplex, FloerCplxExt, FloerHomology,
    FloerHomologyData, FukayaCategory, GromovWittenInvariant, HamiltonianFunction, HoferMetric,
    KAMTorus, LagrangianFloer, LagrangianSubmanifoldData, LiouvilleMeasure, LiouvilleTorus,
    MomentMap, PhaseSpacePoint, PoissonBracket, PseudoHolomorphicCurve, QuantumCohomology,
    RabinowitzFloerHomology, SympCapExt, SympCapMid, SymplecticForm, SymplecticManifold,
    SymplecticMatrix, SymplecticReduction, WeinsteinManifold,
};

pub fn app(f: Expr, a: Expr) -> Expr {
    Expr::App(Box::new(f), Box::new(a))
}
pub fn app2(f: Expr, a: Expr, b: Expr) -> Expr {
    app(app(f, a), b)
}
pub fn cst(s: &str) -> Expr {
    Expr::Const(Name::str(s), vec![])
}
pub fn prop() -> Expr {
    Expr::Sort(Level::zero())
}
pub fn type0() -> Expr {
    Expr::Sort(Level::succ(Level::zero()))
}
pub fn pi(bi: BinderInfo, name: &str, dom: Expr, body: Expr) -> Expr {
    Expr::Pi(bi, Name::str(name), Box::new(dom), Box::new(body))
}
pub fn arrow(a: Expr, b: Expr) -> Expr {
    pi(BinderInfo::Default, "_", a, b)
}
pub fn nat_ty() -> Expr {
    cst("Nat")
}
pub fn real_ty() -> Expr {
    cst("Real")
}
pub fn bool_ty() -> Expr {
    cst("Bool")
}
pub fn int_ty() -> Expr {
    cst("Int")
}
/// Symplectic form type: a closed non-degenerate 2-form ω on a manifold
pub fn symplectic_form_ty() -> Expr {
    arrow(type0(), type0())
}
/// Symplectic manifold type: (M, ω) with dω = 0 and ω non-degenerate
pub fn symplectic_manifold_ty() -> Expr {
    arrow(type0(), arrow(symplectic_form_ty(), type0()))
}
/// Liouville measure type: the canonical volume form ωⁿ/n! on (M²ⁿ, ω)
pub fn liouville_measure_ty() -> Expr {
    arrow(symplectic_manifold_ty(), real_ty())
}
/// Hamiltonian function type: H : T*M → ℝ (energy function on phase space)
pub fn hamiltonian_function_ty() -> Expr {
    arrow(type0(), real_ty())
}
/// Phase space point type: (q₁,...,qₙ, p₁,...,pₙ) ∈ T*M
pub fn phase_space_point_ty() -> Expr {
    arrow(nat_ty(), type0())
}
/// Poisson bracket type: {f, g} = Σ (∂f/∂qᵢ ∂g/∂pᵢ - ∂f/∂pᵢ ∂g/∂qᵢ)
pub fn poisson_bracket_ty() -> Expr {
    arrow(
        arrow(type0(), real_ty()),
        arrow(arrow(type0(), real_ty()), arrow(type0(), real_ty())),
    )
}
/// Canonical transformation type: a symplectomorphism (Q,P) = φ(q,p)
pub fn canonical_transformation_ty() -> Expr {
    arrow(type0(), arrow(type0(), prop()))
}
/// Symplectic matrix type: J^T Ω J = Ω where Ω is the standard symplectic matrix
pub fn symplectic_matrix_ty() -> Expr {
    arrow(nat_ty(), type0())
}
/// Symplectic group Sp(2n) type: the group of 2n×2n symplectic matrices
pub fn symplectic_group_ty() -> Expr {
    arrow(nat_ty(), type0())
}
/// Action variables type: adiabatic invariants Iᵢ = (1/2π) ∮ p dq
pub fn action_variables_ty() -> Expr {
    arrow(nat_ty(), arrow(arrow(real_ty(), real_ty()), real_ty()))
}
/// Angle variables type: θᵢ conjugate to action variables Iᵢ
pub fn angle_variables_ty() -> Expr {
    arrow(nat_ty(), real_ty())
}
/// Liouville torus type: the invariant torus Tⁿ in the Arnold-Liouville theorem
pub fn liouville_torus_ty() -> Expr {
    arrow(arrow(nat_ty(), real_ty()), type0())
}
/// Moment map type: μ : M → g* (dual of Lie algebra)
pub fn moment_map_ty() -> Expr {
    arrow(type0(), arrow(type0(), type0()))
}
/// Symplectic reduction type: M//G = μ⁻¹(0)/G (Marsden-Weinstein quotient)
pub fn symplectic_reduction_ty() -> Expr {
    arrow(moment_map_ty(), type0())
}
/// Contact form type: a 1-form α on M²ⁿ⁺¹ such that α ∧ (dα)ⁿ ≠ 0
pub fn contact_form_ty() -> Expr {
    arrow(type0(), type0())
}
/// Contact manifold type: (M²ⁿ⁺¹, α) with contact structure ker α
pub fn contact_manifold_ty() -> Expr {
    arrow(type0(), arrow(contact_form_ty(), type0()))
}
/// Reeb vector field type: the unique vector field Rα with α(Rα) = 1, ι(Rα)dα = 0
pub fn reeb_vector_field_ty() -> Expr {
    arrow(contact_form_ty(), arrow(type0(), type0()))
}
/// KAM torus type: a perturbed invariant torus surviving small Hamiltonian perturbations
pub fn kam_torus_ty() -> Expr {
    arrow(liouville_torus_ty(), arrow(real_ty(), prop()))
}
/// Diophantine condition type: |k · ω| ≥ γ/|k|^τ for all k ∈ ℤⁿ \ {0}
pub fn diophantine_condition_ty() -> Expr {
    arrow(arrow(nat_ty(), real_ty()), arrow(real_ty(), prop()))
}
/// Floer complex type: generated by periodic orbits of a Hamiltonian
pub fn floer_complex_ty() -> Expr {
    arrow(hamiltonian_function_ty(), type0())
}
/// Pseudo-holomorphic curve type: J-holomorphic map u : Σ → M
pub fn pseudo_holomorphic_curve_ty() -> Expr {
    arrow(type0(), arrow(symplectic_manifold_ty(), type0()))
}
/// Floer homology type: HF*(H) = ker ∂ / im ∂
pub fn floer_homology_ty() -> Expr {
    arrow(floer_complex_ty(), type0())
}
/// Darboux theorem: every symplectic manifold is locally isomorphic to (ℝ²ⁿ, Σ dqᵢ∧dpᵢ)
pub fn darboux_theorem_ty() -> Expr {
    arrow(symplectic_manifold_ty(), prop())
}
/// Liouville theorem: Hamiltonian flow preserves the Liouville measure
pub fn liouville_theorem_ty() -> Expr {
    arrow(hamiltonian_function_ty(), prop())
}
/// Arnold-Liouville theorem: n conserved quantities in involution → action-angle vars
pub fn arnold_liouville_theorem_ty() -> Expr {
    arrow(
        symplectic_manifold_ty(),
        arrow(arrow(nat_ty(), hamiltonian_function_ty()), prop()),
    )
}
/// Marsden-Weinstein theorem: symplectic reduction at a regular value of μ
pub fn marsden_weinstein_theorem_ty() -> Expr {
    arrow(moment_map_ty(), arrow(type0(), prop()))
}
/// Arnold conjecture: #fixed points of φ_H ≥ sum of Betti numbers
pub fn arnold_conjecture_ty() -> Expr {
    arrow(
        symplectic_manifold_ty(),
        arrow(hamiltonian_function_ty(), prop()),
    )
}
/// KAM theorem: most tori survive small analytic Hamiltonian perturbations
pub fn kam_theorem_ty() -> Expr {
    arrow(liouville_torus_ty(), arrow(real_ty(), prop()))
}
/// Contact Darboux theorem: every contact manifold is locally standard
pub fn contact_darboux_theorem_ty() -> Expr {
    arrow(contact_manifold_ty(), prop())
}
/// Register all symplectic geometry axioms into the environment.
pub fn build_symplectic_geometry_env(env: &mut Environment) {
    let axioms: &[(&str, Expr)] = &[
        ("SymplecticForm", symplectic_form_ty()),
        ("SymplecticManifold", symplectic_manifold_ty()),
        ("LiouvilleMeasure", liouville_measure_ty()),
        ("HamiltonianFunction", hamiltonian_function_ty()),
        ("PhaseSpacePoint", phase_space_point_ty()),
        ("PoissonBracket", poisson_bracket_ty()),
        ("CanonicalTransformation", canonical_transformation_ty()),
        ("SymplecticMatrix", symplectic_matrix_ty()),
        ("SymplecticGroup", symplectic_group_ty()),
        ("ActionVariables", action_variables_ty()),
        ("AngleVariables", angle_variables_ty()),
        ("LiouvilleTorus", liouville_torus_ty()),
        ("MomentMap", moment_map_ty()),
        ("SymplecticReduction", symplectic_reduction_ty()),
        ("ContactForm", contact_form_ty()),
        ("ContactManifold", contact_manifold_ty()),
        ("ReebVectorField", reeb_vector_field_ty()),
        ("KAMTorus", kam_torus_ty()),
        ("DiophantineCondition", diophantine_condition_ty()),
        ("FloerComplex", floer_complex_ty()),
        ("PseudoHolomorphicCurve", pseudo_holomorphic_curve_ty()),
        ("FloerHomology", floer_homology_ty()),
        ("DarbouxTheorem", darboux_theorem_ty()),
        ("LiouvilleTheorem", liouville_theorem_ty()),
        ("ArnoldLiouvilleTheorem", arnold_liouville_theorem_ty()),
        ("MarsdenWeinsteinTheorem", marsden_weinstein_theorem_ty()),
        ("ArnoldConjecture", arnold_conjecture_ty()),
        ("KAMTheorem", kam_theorem_ty()),
        ("ContactDarbouxTheorem", contact_darboux_theorem_ty()),
    ];
    for (name, ty) in axioms {
        let decl = Declaration::Axiom {
            name: Name::str(*name),
            univ_params: vec![],
            ty: ty.clone(),
        };
        let _ = env.add(decl);
    }
}
/// Darboux theorem statement as a string.
pub fn darboux_theorem_statement() -> &'static str {
    "Darboux's theorem: For any symplectic manifold (M, ω) of dimension 2n and any \
     point p ∈ M, there exist local coordinates (q₁,...,qₙ, p₁,...,pₙ) around p \
     such that ω = Σᵢ dqᵢ ∧ dpᵢ. In particular, all symplectic manifolds of the \
     same dimension are locally symplectomorphic — there is no local symplectic \
     geometry, only global topology."
}
/// Arnold-Liouville theorem statement.
pub fn arnold_liouville_theorem_statement() -> &'static str {
    "Arnold-Liouville theorem: Let (M²ⁿ, ω, H) be a Hamiltonian system with n \
     independent first integrals f₁ = H, f₂,...,fₙ that are in involution \
     ({fᵢ, fⱼ} = 0 for all i,j) and whose common level sets are compact. Then \
     each connected component of {f₁ = c₁,...,fₙ = cₙ} is diffeomorphic to the \
     n-torus Tⁿ, and in a neighbourhood of each such torus there exist \
     action-angle coordinates (I₁,...,Iₙ, θ₁,...,θₙ) in which H = H(I) and \
     the Hamiltonian flow is linear: dθᵢ/dt = ∂H/∂Iᵢ = ωᵢ(I)."
}
/// Marsden-Weinstein theorem statement.
pub fn marsden_weinstein_theorem() -> &'static str {
    "Marsden-Weinstein theorem (symplectic reduction): Let (M, ω) be a symplectic \
     manifold with a free and proper Hamiltonian action of a Lie group G, with \
     equivariant moment map μ : M → g*. If λ ∈ g* is a regular value of μ, then \
     the quotient M_λ = μ⁻¹(λ)/G_λ is a symplectic manifold of dimension \
     dim M − 2 dim G, with symplectic form ω_λ uniquely determined by \
     π* ω_λ = ι* ω."
}
/// Contact Darboux theorem statement.
pub fn contact_darboux_theorem() -> &'static str {
    "Contact Darboux theorem: For any contact manifold (M²ⁿ⁺¹, α) and any \
     point p ∈ M, there exist local coordinates (x₁,...,xₙ, y₁,...,yₙ, z) \
     around p such that α = dz − Σᵢ yᵢ dxᵢ.  Hence all contact manifolds of \
     the same dimension are locally contactomorphic."
}
/// KAM theorem statement.
pub fn kam_theorem_statement() -> &'static str {
    "KAM theorem (Kolmogorov-Arnold-Moser): Let H = H₀(I) + εH₁(q,I) be a \
     nearly-integrable Hamiltonian system with non-degenerate H₀ \
     (det ∂²H₀/∂I² ≠ 0). For sufficiently small ε, a large measure set of \
     Diophantine tori (satisfying |k·ω| ≥ γ/|k|^τ for all k ∈ ℤⁿ \\ {0}) \
     survive as slightly deformed invariant tori of the perturbed system. \
     The measure of destroyed tori tends to 0 as ε → 0."
}
/// Arnold conjecture statement.
pub fn arnold_conjecture_statement() -> &'static str {
    "Arnold conjecture: For a non-degenerate Hamiltonian diffeomorphism φ of a \
     closed symplectic manifold (M, ω), the number of fixed points of φ is at \
     least the sum of Betti numbers Σₖ bₖ(M; ℤ₂). Equivalently, the number of \
     1-periodic orbits of a non-degenerate Hamiltonian H : S¹ × M → ℝ is at \
     least Σₖ bₖ(M). This was proved using Floer homology HF*(H) ≅ H*(M)."
}
/// Factorial for natural numbers (used in volume formula).
pub(super) fn gamma_natural(n: usize) -> f64 {
    (1..=n).map(|k| k as f64).product::<f64>().max(1.0)
}
/// Check whether a floating-point number is approximately rational (p/q with small q).
pub(super) fn is_rational_approx(x: f64, tol: f64) -> bool {
    for q in 1usize..=100 {
        let p = (x * q as f64).round() as i64;
        if (x - p as f64 / q as f64).abs() < tol {
            return true;
        }
    }
    false
}
/// Convenience alias to mirror the spec name `build_env`.
pub fn build_env(env: &mut Environment) {
    build_symplectic_geometry_env(env);
}
/// Lagrangian intersection Floer homology HF*(L₀, L₁; J) type.
pub fn lagrangian_floer_homology_ty() -> Expr {
    arrow(type0(), arrow(type0(), arrow(type0(), type0())))
}
/// Symplectic cohomology SH*(M) type — Floer theory for the Liouville completion.
pub fn symplectic_cohomology_ty() -> Expr {
    arrow(type0(), type0())
}
/// PSS isomorphism HF*(H) ≅ QH*(M) type.
pub fn pss_isomorphism_ty() -> Expr {
    arrow(floer_homology_ty(), arrow(type0(), prop()))
}
/// Continuation map between Floer complexes for different Hamiltonians.
pub fn continuation_map_ty() -> Expr {
    arrow(floer_complex_ty(), arrow(floer_complex_ty(), type0()))
}
/// Fukaya category Fuk(M, ω) type — an A∞-category with Lagrangians as objects.
pub fn fukaya_category_ty() -> Expr {
    arrow(symplectic_manifold_ty(), type0())
}
/// A∞-algebra type: a graded vector space with operations μᵏ satisfying A∞ relations.
pub fn a_infinity_algebra_ty() -> Expr {
    arrow(nat_ty(), type0())
}
/// A∞-functor between two Fukaya categories.
pub fn a_infinity_functor_ty() -> Expr {
    arrow(fukaya_category_ty(), arrow(fukaya_category_ty(), type0()))
}
/// Yoneda embedding for the Fukaya category — A∞ Yoneda lemma.
pub fn fukaya_yoneda_embedding_ty() -> Expr {
    arrow(fukaya_category_ty(), type0())
}
/// Moduli space of pseudo-holomorphic curves M̄_{g,n}(M, A; J) type.
pub fn moduli_space_curves_ty() -> Expr {
    arrow(
        nat_ty(),
        arrow(nat_ty(), arrow(symplectic_manifold_ty(), type0())),
    )
}
/// Gromov-Witten invariant GW_{g,n,A}(α₁,...,αₙ) type (rational number).
pub fn gromov_witten_invariant_ty() -> Expr {
    arrow(
        moduli_space_curves_ty(),
        arrow(arrow(nat_ty(), type0()), real_ty()),
    )
}
/// Quantum cohomology ring QH*(M) type — deformation of H*(M) by GW invariants.
pub fn quantum_cohomology_ty() -> Expr {
    arrow(symplectic_manifold_ty(), type0())
}
/// WDVV equations (Witten-Dijkgraaf-Verlinde-Verlinde) for GW potential.
pub fn wdvv_equations_ty() -> Expr {
    arrow(quantum_cohomology_ty(), prop())
}
/// SFT algebra for a contact manifold — generated by Reeb orbits.
pub fn sft_algebra_ty() -> Expr {
    arrow(contact_manifold_ty(), type0())
}
/// SFT homology H_*(SFT(M, α)) type.
pub fn sft_homology_ty() -> Expr {
    arrow(sft_algebra_ty(), type0())
}
/// Linearised contact homology CH*(M, α) type — simplification of SFT.
pub fn contact_homology_ty() -> Expr {
    arrow(contact_manifold_ty(), type0())
}
/// Relative SFT invariant for a symplectic cobordism (W, J) : (M₋, ξ₋) → (M₊, ξ₊).
pub fn sft_cobordism_map_ty() -> Expr {
    arrow(type0(), arrow(sft_homology_ty(), sft_homology_ty()))
}
/// Legendrian knot type: a knot K ⊂ (M³, ξ) everywhere tangent to ξ.
pub fn legendrian_knot_ty() -> Expr {
    arrow(contact_manifold_ty(), type0())
}
/// Legendrian contact homology LCH*(K) type — Chekanov-Eliashberg DGA.
pub fn legendrian_contact_homology_ty() -> Expr {
    arrow(legendrian_knot_ty(), type0())
}
/// Transverse knot type: a knot K ⊂ (M³, ξ) everywhere transverse to ξ.
pub fn transverse_knot_ty() -> Expr {
    arrow(contact_manifold_ty(), type0())
}
/// Bennequin inequality: sl(K) ≤ -χ(Σ) for a Seifert surface Σ.
pub fn bennequin_inequality_ty() -> Expr {
    arrow(transverse_knot_ty(), arrow(type0(), prop()))
}
/// Overtwisted disk type: a disk D² ↪ (M, ξ) tangent to ξ along ∂D².
pub fn overtwisted_disk_ty() -> Expr {
    arrow(contact_manifold_ty(), type0())
}
/// Tight contact structure type: one that admits no overtwisted disk.
pub fn tight_contact_structure_ty() -> Expr {
    arrow(contact_manifold_ty(), prop())
}
/// Weinstein manifold type: (M, ω, X, φ) with Liouville vector field X and Morse function φ.
pub fn weinstein_manifold_ty() -> Expr {
    arrow(type0(), arrow(arrow(type0(), real_ty()), type0()))
}
/// Weinstein handle type: a symplectic handle attachment along an isotropic sphere.
pub fn weinstein_handle_ty() -> Expr {
    arrow(nat_ty(), arrow(type0(), type0()))
}
/// Stein structure type: a Stein domain (complex manifold with plurisubharmonic exhaustion).
pub fn stein_structure_ty() -> Expr {
    arrow(type0(), prop())
}
/// Eliashberg's theorem: Stein structures ↔ Weinstein structures (in dim ≥ 6).
pub fn stein_weinstein_equivalence_ty() -> Expr {
    arrow(stein_structure_ty(), arrow(weinstein_manifold_ty(), prop()))
}
/// Symplectic capacity type: a monotone, conformally symplectic invariant c(M, ω) > 0.
pub fn symplectic_capacity_ty() -> Expr {
    arrow(symplectic_manifold_ty(), real_ty())
}
/// Gromov non-squeezing theorem: B²ⁿ(r) ↪_s Z²ⁿ(R) iff r ≤ R.
pub fn gromov_non_squeezing_ty() -> Expr {
    arrow(real_ty(), arrow(real_ty(), prop()))
}
/// Ekeland-Hofer capacity c_k(M, ω) type — sequence of capacities.
pub fn ekeland_hofer_capacity_ty() -> Expr {
    arrow(nat_ty(), symplectic_capacity_ty())
}
/// Cylindrical capacity c_cyl(M, ω) type — defined via symplectic embeddings in cylinders.
pub fn cylindrical_capacity_ty() -> Expr {
    arrow(symplectic_manifold_ty(), real_ty())
}
/// Liouville domain type: a compact manifold with boundary (W, ω, λ) with dλ = ω.
pub fn liouville_domain_ty() -> Expr {
    arrow(type0(), arrow(type0(), type0()))
}
/// Liouville vector field type: the dual of the Liouville form λ with ι_X ω = λ.
pub fn liouville_vector_field_ty() -> Expr {
    arrow(liouville_domain_ty(), arrow(type0(), type0()))
}
/// Completion of a Liouville domain: attach a cylindrical end ∂W × [1,∞).
pub fn liouville_completion_ty() -> Expr {
    arrow(liouville_domain_ty(), type0())
}
/// Viterbo transfer map SH*(W') → SH*(W) for Liouville subdomain W ↪ W'.
pub fn viterbo_transfer_map_ty() -> Expr {
    arrow(
        liouville_domain_ty(),
        arrow(
            liouville_domain_ty(),
            arrow(symplectic_cohomology_ty(), symplectic_cohomology_ty()),
        ),
    )
}
/// Homological Mirror Symmetry (HMS) type: Fuk(M) ≃ D^b(Coh(M̌)).
pub fn homological_mirror_symmetry_ty() -> Expr {
    arrow(fukaya_category_ty(), arrow(type0(), prop()))
}
/// SYZ (Strominger-Yau-Zaslow) fibration type: special Lagrangian T^n-fibration.
pub fn syz_fibration_ty() -> Expr {
    arrow(symplectic_manifold_ty(), arrow(type0(), prop()))
}
/// Mirror pair type: two symplectic manifolds (M, M̌) related by HMS.
pub fn mirror_pair_ty() -> Expr {
    arrow(
        symplectic_manifold_ty(),
        arrow(symplectic_manifold_ty(), prop()),
    )
}
/// Lagrangian surgery type: modified Lagrangian obtained by surgery at an intersection.
pub fn lagrangian_surgery_ty() -> Expr {
    arrow(type0(), arrow(type0(), type0()))
}
/// Lagrangian cobordism type: a Lagrangian in (M × ℂ, ω ⊕ ω_std) connecting L₋ and L₊.
pub fn lagrangian_cobordism_ty() -> Expr {
    arrow(type0(), arrow(type0(), type0()))
}
/// Polterovich surgery formula: cobordism induces map on Lagrangian Floer homology.
pub fn polterovich_surgery_ty() -> Expr {
    arrow(
        lagrangian_cobordism_ty(),
        arrow(
            lagrangian_floer_homology_ty(),
            lagrangian_floer_homology_ty(),
        ),
    )
}
/// Polyfold type: a generalized smooth space for compactified moduli problems.
pub fn polyfold_ty() -> Expr {
    arrow(type0(), type0())
}
/// Kuranishi structure type: a finite-dimensional obstruction theory for moduli spaces.
pub fn kuranishi_structure_ty() -> Expr {
    arrow(moduli_space_curves_ty(), type0())
}
/// Abstract virtual fundamental class from a Kuranishi structure.
pub fn virtual_fundamental_class_ty() -> Expr {
    arrow(kuranishi_structure_ty(), type0())
}
/// Hofer metric type: d_H(φ, ψ) = inf ∫ (max H - min H) dt on Ham(M, ω).
pub fn hofer_metric_ty() -> Expr {
    arrow(type0(), arrow(type0(), real_ty()))
}
/// Hofer norm type: ||φ||_H = d_H(φ, id).
pub fn hofer_norm_ty() -> Expr {
    arrow(type0(), real_ty())
}
/// Energy-capacity inequality: ||φ||_H ≥ c(φ) for any symplectic capacity c.
pub fn energy_capacity_inequality_ty() -> Expr {
    arrow(hofer_norm_ty(), arrow(symplectic_capacity_ty(), prop()))
}
/// Rabinowitz action functional type — Lagrange multiplier for energy hypersurface.
pub fn rabinowitz_action_ty() -> Expr {
    arrow(type0(), arrow(real_ty(), real_ty()))
}
/// Rabinowitz Floer homology RFH*(Σ, W) type.
pub fn rabinowitz_floer_homology_ty() -> Expr {
    arrow(type0(), arrow(liouville_domain_ty(), type0()))
}
/// Albers-Kang isomorphism: RFH*(Σ) ≅ SH*(W) for a Liouville domain.
pub fn albers_kang_isomorphism_ty() -> Expr {
    arrow(
        rabinowitz_floer_homology_ty(),
        arrow(symplectic_cohomology_ty(), prop()),
    )
}
/// Equivariant symplectic form type: ω on (M, G-action) with G-invariant ω.
pub fn equivariant_symplectic_form_ty() -> Expr {
    arrow(type0(), arrow(symplectic_form_ty(), prop()))
}
/// Atiyah-Guillemin-Sternberg convexity theorem: μ(M) is a convex polytope.
pub fn ags_convexity_theorem_ty() -> Expr {
    arrow(moment_map_ty(), prop())
}
/// Delzant polytope type: the moment polytope of a Hamiltonian torus action on a toric manifold.
pub fn delzant_polytope_ty() -> Expr {
    arrow(nat_ty(), type0())
}
/// Delzant's theorem: compact toric symplectic manifolds ↔ Delzant polytopes.
pub fn delzant_theorem_ty() -> Expr {
    arrow(
        delzant_polytope_ty(),
        arrow(symplectic_manifold_ty(), prop()),
    )
}
/// Symplectic ball embedding type: B^{2n}(r) ↪_s (M, ω).
pub fn symplectic_ball_embedding_ty() -> Expr {
    arrow(real_ty(), arrow(symplectic_manifold_ty(), prop()))
}
/// Symplectic packing number p_k(M) type: max fraction of volume packed by k balls.
pub fn symplectic_packing_number_ty() -> Expr {
    arrow(nat_ty(), arrow(symplectic_manifold_ty(), real_ty()))
}
/// McDuff-Polterovich packing obstruction type.
pub fn packing_obstruction_ty() -> Expr {
    arrow(symplectic_packing_number_ty(), prop())
}
/// Register all advanced symplectic topology axioms (§10) into the environment.
pub fn build_symplectic_geometry_ext_env(env: &mut Environment) {
    let axioms: &[(&str, Expr)] = &[
        ("LagrangianFloerHomology", lagrangian_floer_homology_ty()),
        ("SymplecticCohomology", symplectic_cohomology_ty()),
        ("PSSIsomorphism", pss_isomorphism_ty()),
        ("ContinuationMap", continuation_map_ty()),
        ("FukayaCategory", fukaya_category_ty()),
        ("AInfinityAlgebra", a_infinity_algebra_ty()),
        ("AInfinityFunctor", a_infinity_functor_ty()),
        ("FukayaYonedaEmbedding", fukaya_yoneda_embedding_ty()),
        ("ModuliSpaceCurves", moduli_space_curves_ty()),
        ("GromovWittenInvariant", gromov_witten_invariant_ty()),
        ("QuantumCohomology", quantum_cohomology_ty()),
        ("WDVVEquations", wdvv_equations_ty()),
        ("SFTAlgebra", sft_algebra_ty()),
        ("SFTHomology", sft_homology_ty()),
        ("ContactHomology", contact_homology_ty()),
        ("SFTCobordismMap", sft_cobordism_map_ty()),
        ("LegendrianKnot", legendrian_knot_ty()),
        (
            "LegendrianContactHomology",
            legendrian_contact_homology_ty(),
        ),
        ("TransverseKnot", transverse_knot_ty()),
        ("BennequinInequality", bennequin_inequality_ty()),
        ("OvertwistedDisk", overtwisted_disk_ty()),
        ("TightContactStructure", tight_contact_structure_ty()),
        ("WeinsteinManifold", weinstein_manifold_ty()),
        ("WeinsteinHandle", weinstein_handle_ty()),
        ("SteinStructure", stein_structure_ty()),
        (
            "SteinWeinsteinEquivalence",
            stein_weinstein_equivalence_ty(),
        ),
        ("SymplecticCapacity", symplectic_capacity_ty()),
        ("GromovNonSqueezing", gromov_non_squeezing_ty()),
        ("EkelandHoferCapacity", ekeland_hofer_capacity_ty()),
        ("CylindricalCapacity", cylindrical_capacity_ty()),
        ("LiouvilleDomain", liouville_domain_ty()),
        ("LiouvilleVectorField", liouville_vector_field_ty()),
        ("LiouvilleCompletion", liouville_completion_ty()),
        ("ViterboTransferMap", viterbo_transfer_map_ty()),
        (
            "HomologicalMirrorSymmetry",
            homological_mirror_symmetry_ty(),
        ),
        ("SYZFibration", syz_fibration_ty()),
        ("MirrorPair", mirror_pair_ty()),
        ("LagrangianSurgery", lagrangian_surgery_ty()),
        ("LagrangianCobordism", lagrangian_cobordism_ty()),
        ("PolterovichSurgery", polterovich_surgery_ty()),
        ("Polyfold", polyfold_ty()),
        ("KuranishiStructure", kuranishi_structure_ty()),
        ("VirtualFundamentalClass", virtual_fundamental_class_ty()),
        ("HoferMetric", hofer_metric_ty()),
        ("HoferNorm", hofer_norm_ty()),
        ("EnergyCapacityInequality", energy_capacity_inequality_ty()),
        ("RabinowitzAction", rabinowitz_action_ty()),
        ("RabinowitzFloerHomology", rabinowitz_floer_homology_ty()),
        ("AlbersKangIsomorphism", albers_kang_isomorphism_ty()),
        (
            "EquivariantSymplecticForm",
            equivariant_symplectic_form_ty(),
        ),
        ("AGSConvexityTheorem", ags_convexity_theorem_ty()),
        ("DelzantPolytope", delzant_polytope_ty()),
        ("DelzantTheorem", delzant_theorem_ty()),
        ("SymplecticBallEmbedding", symplectic_ball_embedding_ty()),
        ("SymplecticPackingNumber", symplectic_packing_number_ty()),
        ("PackingObstruction", packing_obstruction_ty()),
    ];
    for (name, ty) in axioms {
        let decl = Declaration::Axiom {
            name: Name::str(*name),
            univ_params: vec![],
            ty: ty.clone(),
        };
        let _ = env.add(decl);
    }
}
#[cfg(test)]
mod extended_symplectic_tests {
    use super::*;
    #[test]
    fn test_lagrangian() {
        let zs = LagrangianSubmanifoldData::zero_section(3);
        assert_eq!(zs.dimension(), 3);
        assert!(zs.is_exact);
        assert!(zs.arnold_conjecture_description().contains("Floer"));
    }
    #[test]
    fn test_symplectic_capacity() {
        let gw = SympCapMid::gromov_width("B^4(1)", 1.0);
        assert!(gw.is_gromov);
        assert!(gw.nonsqueezing_description().contains("Non-squeezing"));
    }
    #[test]
    fn test_floer_homology() {
        let fh = FloerHomologyData::new("T^2", "H", vec!["p1", "p2", "p3"], vec![0, 1, 2]);
        assert_eq!(fh.num_generators(), 3);
    }
    #[test]
    fn test_contact_manifold() {
        let s3 = ContactManifoldData::standard_sphere(2);
        assert_eq!(s3.dimension, 3);
        assert!(s3.is_tight);
        assert!(!s3.is_overtwisted);
        assert!(s3.eliashberg_classified());
        assert!(s3.reeb_flow_description().contains("Reeb flow"));
    }
}
#[cfg(test)]
mod tests_sympl_geom_ext {
    use super::*;
    #[test]
    fn test_floer_complex() {
        let fc = FloerCplxExt::new("H", "M", vec!["x".to_string(), "y".to_string()]);
        let pss = fc.pss_isomorphism();
        assert!(pss.contains("PSS"));
        let arnold = fc.arnold_conjecture_connection();
        assert!(arnold.contains("Arnold"));
        let grom = fc.gromov_compactness();
        assert!(grom.contains("Gromov"));
        let nov = fc.novikov_ring();
        assert!(nov.contains("Novikov"));
    }
    #[test]
    fn test_lagrangian_floer() {
        let lf = LagrangianFloer::new("L0", "L1", "M", 3);
        let desc = lf.floer_cohomology_description();
        assert!(desc.contains("Floer cohomology"));
        let oh = lf.oh_theorem();
        assert!(oh.contains("Oh"));
        assert_eq!(lf.intersection_lower_bound(), 3);
    }
    #[test]
    fn test_gromov_witten() {
        let gw = GromovWittenInvariant::plane_curves(0, 3);
        let vdim = gw.virtual_dimension();
        assert!(vdim >= 0);
        let konts = gw.kontsevich_recursion();
        assert!(konts.contains("Kontsevich"));
        let mirror = gw.mirror_symmetry_connection();
        assert!(mirror.contains("mirror"));
    }
    #[test]
    fn test_quantum_cohomology() {
        let qh = QuantumCohomology::small_qh_cpn(2);
        assert!(qh.is_small_quantum);
        let prod = qh.quantum_product_description();
        assert!(prod.contains("QH*"));
        let rel = qh.relation_cpn();
        assert!(rel.contains("hyperplane") || rel.contains("quantum"));
        let wdvv = qh.wdvv_equations();
        assert!(wdvv.contains("WDVV"));
    }
    #[test]
    fn test_symplectic_capacity() {
        let gw = SympCapExt::gromov_width("M");
        assert!(gw.is_normalized);
        let nonsq = gw.nonsqueezing_theorem();
        assert!(nonsq.contains("Gromov"));
        let eh1 = SympCapExt::ekeland_hofer_capacity("M", 1);
        assert!(eh1.is_normalized);
        assert_eq!(eh1.value_on_ball, 1.0);
        let eh2 = SympCapExt::ekeland_hofer_capacity("M", 2);
        assert!(!eh2.is_normalized);
    }
    #[test]
    fn test_ellipsoid_embedding() {
        let emb = EllipsoidEmbedding::new(vec![1.0, 2.0], vec![3.0, 3.0]);
        let ms = emb.mcduff_schlenk_staircase();
        assert!(ms.contains("McDuff"));
        let obs = emb.obstructions_from_capacities();
        assert!(obs.contains("Obstruction"));
        let suf = emb.sufficient_condition_4d();
        assert!(suf.contains("4D"));
    }
}