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::{
    AffinoidSpace, ColemanPowerSeries, ContinuousCohomology, HenselsLemma, IwasawaAlgebra,
    IwasawaInvariants, IwasawaModule, KubotaLeopoldt, LocalField, LocallyAnalyticFunctions,
    LubinTateFormalGroup, MahlerExpansion, MahlerTransform, NewtonPolygon, OverconvergentFunctions,
    PAdicAbsoluteValue, PAdicBanachSpace, PAdicDifferentialEquation, PAdicDistributions, PAdicExp,
    PAdicInteger, PAdicLieGroup, PAdicLog, PAdicNumber, PAdicValuation, PAdicValuationRing,
    PolynomialMod, ProfiniteGroup, RigidAnalyticSpace, TateAlgebra, UnramifiedExtension,
    VolkenbornIntegral, WeierstrausPrepTheorem, WittRing, WittVector, ZpStar,
};

/// Statement of the ultrametric triangle inequality for p-adic absolute values.
pub fn ultrametric_triangle_inequality_statement() -> &'static str {
    "For the p-adic absolute value |·|_p, the ultrametric triangle inequality holds: \
     for all x, y ∈ ℚ_p, |x + y|_p ≤ max(|x|_p, |y|_p). \
     This is stronger than the ordinary triangle inequality."
}
/// Statement of Ostrowski's theorem.
pub fn ostrowski_theorem_statement() -> &'static str {
    "Ostrowski's Theorem: Every non-trivial absolute value on ℚ is equivalent to either \
     the real absolute value |·|_∞ or the p-adic absolute value |·|_p for some prime p. \
     In particular, there are no other absolute values on ℚ up to equivalence."
}
/// Hensel lifting: given f and a simple root `root` mod p, lift to precision `p^precision`.
///
/// Returns `Some(digits)` where `digits\[k\]` is the k-th digit in the p-adic expansion of the
/// lifted root, or `None` if lifting fails (e.g. f'(root) ≡ 0 mod p).
pub fn hensel_lift(f: &PolynomialMod, root: i64, p: u64, precision: u32) -> Option<Vec<i64>> {
    let fp = f.derivative();
    let p_i64 = p as i64;
    let fp_val = fp.evaluate(root).rem_euclid(p_i64);
    if fp_val == 0 {
        return None;
    }
    let mut current = root.rem_euclid(p_i64);
    let mut modulus = p_i64;
    let mut digits = Vec::new();
    for _ in 0..precision {
        let digit = current.rem_euclid(p_i64);
        digits.push(digit);
        current /= p_i64;
        let f_mod = PolynomialMod::new(f.coeffs.clone(), (modulus * p_i64) as u64);
        let fp_mod = PolynomialMod::new(fp.coeffs.clone(), (modulus * p_i64) as u64);
        let fval = f_mod.evaluate(current * modulus + digit);
        let fpval = fp_mod.evaluate(digit);
        if fpval == 0 {
            break;
        }
        current -= fval / fpval;
        modulus *= p_i64;
    }
    Some(digits)
}
/// Statement of Hensel's Lemma.
pub fn hensel_lemma_statement() -> &'static str {
    "Hensel's Lemma: Let f ∈ ℤ_p[X] and suppose r ∈ ℤ_p satisfies f(r) ≡ 0 (mod p) \
     but f'(r) ≢ 0 (mod p). Then there exists a unique a ∈ ℤ_p such that f(a) = 0 and a ≡ r (mod p). \
     More generally, if |f(r)|_p < |f'(r)|_p^2 then the Newton iteration converges."
}
/// Radius of convergence of the p-adic exponential.
///
/// For odd p: r = p^{-1/(p-1)}.  For p = 2: r = 2^{-2} = 1/4.
pub fn padic_exp_convergence(p: u64) -> f64 {
    if p == 2 {
        0.25
    } else {
        let exponent = -1.0 / (p as f64 - 1.0);
        (p as f64).powf(exponent)
    }
}
/// Statement of the Iwasawa Main Conjecture (now a theorem due to Mazur-Wiles).
pub fn iwasawa_main_conjecture_statement() -> &'static str {
    "Iwasawa Main Conjecture (Mazur-Wiles, 1984): For an odd prime p, let χ be an \
     odd Dirichlet character and let X_∞ be the projective limit of the p-parts of the \
     ideal class groups along the cyclotomic ℤ_p-extension. Then the characteristic ideal \
     of X_∞(χ) as a Λ-module is generated by the p-adic L-function L_p(s, χ)."
}
/// A human-readable description of the Witt vector addition formula.
pub fn witt_vector_addition_formula(p: u64, n: usize) -> String {
    format!(
        "For Witt vectors over a ring of characteristic {p}, the n={n} addition formula \
         is given by (x + y)_n = S_n(x_0, …, x_n, y_0, …, y_n) where S_n are universal \
         polynomials with ℤ-coefficients determined by the ghost component identity \
         w_n(x + y) = w_n(x) + w_n(y) with w_n = Σ_{{k=0}}^n p^k X_k^{{p^{{n-k}}}}."
    )
}
/// Statement of local class field theory.
pub fn local_class_field_theory_statement() -> &'static str {
    "Local Class Field Theory: For a local field K (finite extension of ℚ_p), there is a \
     canonical isomorphism rec_K : K^× → Gal(K^{ab}/K)^{op} called the local Artin map. \
     It sends uniformizers to arithmetic Frobenii, units to inertia, and the kernel of the \
     map to subgroups corresponding to abelian extensions. The theory classifies all finite \
     abelian extensions of K via the norm group N_{L/K}(L^×) ≤ K^×."
}
/// Compute C(n, k) as f64 for small n, k.
pub(super) fn mahler_binomial(n: i64, k: usize) -> f64 {
    if k == 0 {
        return 1.0;
    }
    if n < k as i64 {
        return 0.0;
    }
    let mut result = 1.0f64;
    for i in 0..k {
        result *= (n - i as i64) as f64 / (i + 1) as f64;
    }
    result
}
/// Compute C(n, k) as f64 (alias).
pub(super) fn binomial_f64(n: i64, k: usize) -> f64 {
    mahler_binomial(n, k)
}
/// Krasner's lemma: algebraic proximity implies field containment.
pub fn krasners_lemma_statement() -> &'static str {
    "Krasner's Lemma: Let K be a complete non-archimedean field and α a root of \
     an irreducible polynomial f over K. If β is another algebraic element satisfying \
     |β - α| < |α - αᵢ| for all conjugates αᵢ ≠ α of α, then K(α) ⊆ K(β). \
     This implies the irreducibility criterion: if β is very close to α, f is still \
     irreducible over K(β)."
}
/// Statement that the p-adic power series ring ℤ_p[\[T\]] is a UFD.
pub fn power_series_ring_ufd_statement() -> &'static str {
    "The power series ring ℤ_p[[T]] is a UFD: the irreducible elements are p and \
     the Weierstrass polynomials with coefficients in pℤ_p except for leading coefficient 1. \
     Every non-zero element factors as a product of irreducibles times a unit."
}
/// Evaluate a polynomial (coefficients in increasing degree) at x.
pub(super) fn evaluate_poly(coeffs: &[f64], x: f64) -> f64 {
    let mut result = 0.0f64;
    let mut power = 1.0f64;
    for &c in coeffs {
        result += c * power;
        power *= x;
    }
    result
}
/// The Shnirelman integral over a p-adic circle.
pub fn shnirelman_integral_statement() -> &'static str {
    "The Shnirelman integral (or Tate integral) ∮_{|z|_p = 1} f(z) dz/z for meromorphic \
     functions on the p-adic disk: computes residues as in the complex case but using \
     the p-adic ultrametric topology. For rational functions it equals the sum of \
     residues inside the disk."
}
/// Dwork's p-adic hypergeometric function and its unit root.
pub fn dwork_hypergeometric_statement() -> &'static str {
    "Dwork's p-adic hypergeometric function F_p(λ) arises as the unit root of the \
     zeta function of the Legendre family of elliptic curves y^2 = x(x-1)(x-λ) over 𝔽_p. \
     Dwork proved that F_p extends to a p-adic analytic function on |λ|_p < 1, \
     satisfying a p-adic hypergeometric differential equation."
}
/// p-adic regulator via Coleman integration.
pub fn coleman_integration_statement() -> &'static str {
    "Coleman integration provides a p-adic analogue of the complex line integral for \
     1-forms on a curve. For a smooth proper curve X/ℚ_p and a 1-form ω, the Coleman \
     integral ∫_a^b ω is well-defined for points a, b in the same residue disk (and \
     can be extended globally via the Frobenius action). This gives the p-adic regulator \
     in the theory of p-adic heights."
}
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 app3(f: Expr, a: Expr, b: Expr, c: Expr) -> Expr {
    app(app2(f, a, b), c)
}
pub fn cst(s: &str) -> Expr {
    Expr::Const(Name::str(s), vec![])
}
pub fn prop_k() -> Expr {
    Expr::Sort(Level::zero())
}
pub fn type0_k() -> Expr {
    Expr::Sort(Level::succ(Level::zero()))
}
pub fn pi_k(name: &str, dom: Expr, body: Expr) -> Expr {
    Expr::Pi(
        BinderInfo::Default,
        Name::str(name),
        Box::new(dom),
        Box::new(body),
    )
}
pub fn arrow_k(a: Expr, b: Expr) -> Expr {
    pi_k("_", a, b)
}
pub fn nat_k() -> Expr {
    cst("Nat")
}
pub fn real_k() -> Expr {
    cst("Real")
}
pub fn bvar_k(n: u32) -> Expr {
    Expr::BVar(n)
}
/// `PAdicBanachSpace : Nat → Type`
pub fn padic_banach_space_ty() -> Expr {
    arrow_k(nat_k(), type0_k())
}
/// `MahlerBasis : Nat → Prop` — the Mahler basis is orthonormal for C(ℤ_p, ℚ_p).
pub fn mahler_basis_ty() -> Expr {
    arrow_k(nat_k(), prop_k())
}
/// `BanachSteinhausPadic : Prop`
pub fn banach_steinhaus_padic_ty() -> Expr {
    prop_k()
}
/// `WeierstraussPrep : Nat → Nat → Prop`
pub fn weierstrauss_prep_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(nat_k(), prop_k()))
}
/// `KrasnersLemma : Prop`
pub fn krasners_lemma_ty() -> Expr {
    prop_k()
}
/// `LocallyAnalyticFunctions : Nat → Type`
pub fn locally_analytic_functions_ty() -> Expr {
    arrow_k(nat_k(), type0_k())
}
/// `PAdicDistributions : Nat → Type`
pub fn padic_distributions_ty() -> Expr {
    arrow_k(nat_k(), type0_k())
}
/// `AmiceTransform : Nat → Prop` — the Amice transform isomorphism.
pub fn amice_transform_ty() -> Expr {
    arrow_k(nat_k(), prop_k())
}
/// `VolkenbornIntegral : Nat → (Nat → Real) → Real`
pub fn volkenborn_integral_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(arrow_k(nat_k(), real_k()), real_k()))
}
/// `ShnirelmanIntegral : Prop`
pub fn shnirelman_integral_ty() -> Expr {
    prop_k()
}
/// `KubotaLeopoldt : Nat → Nat → Real` — the p-adic L-function L_p(s, χ).
pub fn kubota_leopoldt_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(nat_k(), real_k()))
}
/// `IwasawaInvariants : Nat → Nat × Nat` — μ and λ invariants.
pub fn iwasawa_invariants_ty() -> Expr {
    arrow_k(nat_k(), app2(cst("Prod"), nat_k(), nat_k()))
}
/// `MuZeroConjecture : Nat → Prop`
pub fn mu_zero_conjecture_ty() -> Expr {
    arrow_k(nat_k(), prop_k())
}
/// `PAdicDifferentialEquation : Nat → Nat → Type`
pub fn padic_differential_eq_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(nat_k(), type0_k()))
}
/// `DworkTheorem : Nat → Prop`
pub fn dwork_theorem_ty() -> Expr {
    arrow_k(nat_k(), prop_k())
}
/// `MonodromyTheorem : Prop` — the p-adic monodromy theorem.
pub fn monodromy_theorem_ty() -> Expr {
    prop_k()
}
/// `FrobeniusStructure : Nat → Nat → Prop`
pub fn frobenius_structure_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(nat_k(), prop_k()))
}
/// `ContinuousCohomology : Type → Type → Nat → Type`
pub fn continuous_cohomology_ty() -> Expr {
    arrow_k(type0_k(), arrow_k(type0_k(), arrow_k(nat_k(), type0_k())))
}
/// `ExtGroup : Nat → Type → Type → Type`
pub fn ext_group_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(type0_k(), arrow_k(type0_k(), type0_k())))
}
/// `TateAlgebra : Nat → Nat → Type`
pub fn tate_algebra_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(nat_k(), type0_k()))
}
/// `AffinoidSpace : Nat → Nat → Type`
pub fn affinoid_space_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(nat_k(), type0_k()))
}
/// `RigidAnalyticSpace : Nat → Nat → Type`
pub fn rigid_analytic_space_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(nat_k(), type0_k()))
}
/// `RigidGAGA : Prop` — Kiehl's GAGA for rigid analytic spaces.
pub fn rigid_gaga_ty() -> Expr {
    prop_k()
}
/// `OverconvergentFunctions : Nat → Real → Type`
pub fn overconvergent_functions_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(real_k(), type0_k()))
}
/// `RobbaRing : Nat → Type`
pub fn robba_ring_ty() -> Expr {
    arrow_k(nat_k(), type0_k())
}
/// `DworkHypergeometric : Nat → Real → Real`
pub fn dwork_hypergeometric_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(real_k(), real_k()))
}
/// `LubinTateFormalGroup : Nat → Nat → Type`
pub fn lubin_tate_formal_group_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(nat_k(), type0_k()))
}
/// `FormalExponential : Nat → Real → Real`
pub fn formal_exponential_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(real_k(), real_k()))
}
/// `FormalLogarithm : Nat → Real → Real`
pub fn formal_logarithm_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(real_k(), real_k()))
}
/// `LubinTateCFT : Nat → Prop` — Lubin-Tate local class field theory.
pub fn lubin_tate_cft_ty() -> Expr {
    arrow_k(nat_k(), prop_k())
}
/// `ColemanPowerSeries : Nat → Type`
pub fn coleman_power_series_ty() -> Expr {
    arrow_k(nat_k(), type0_k())
}
/// `ColemanTheorem : Nat → Prop` — norm-compatible sequences and power series.
pub fn coleman_theorem_ty() -> Expr {
    arrow_k(nat_k(), prop_k())
}
/// `ColemanIntegration : Nat → Prop`
pub fn coleman_integration_ty() -> Expr {
    arrow_k(nat_k(), prop_k())
}
/// `NormCompatibleSequence : Nat → Type`
pub fn norm_compatible_sequence_ty() -> Expr {
    arrow_k(nat_k(), type0_k())
}
/// `MahlerTransform : Nat → Type` — the Mahler transform bijection.
pub fn mahler_transform_ty() -> Expr {
    arrow_k(nat_k(), type0_k())
}
/// `CharacteristicSeries : Nat → Type` — characteristic series of an Iwasawa module.
pub fn characteristic_series_ty() -> Expr {
    arrow_k(nat_k(), type0_k())
}
/// `PAdicMeasure : Nat → Type` — a p-adic measure (bounded distribution).
pub fn padic_measure_ty() -> Expr {
    arrow_k(nat_k(), type0_k())
}
/// `IwasawaMainConjectureGen : Nat → Prop` — generalized Iwasawa main conjecture.
pub fn iwasawa_main_conjecture_gen_ty() -> Expr {
    arrow_k(nat_k(), prop_k())
}
/// `GaloisRepresentation : Nat → Nat → Type` — p-adic Galois representation.
pub fn galois_representation_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(nat_k(), type0_k()))
}
/// `DeRhamRepresentation : Nat → Nat → Prop`
pub fn de_rham_representation_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(nat_k(), prop_k()))
}
/// `CrystallineRepresentation : Nat → Nat → Prop`
pub fn crystalline_representation_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(nat_k(), prop_k()))
}
/// `SemistableRepresentation : Nat → Nat → Prop`
pub fn semistable_representation_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(nat_k(), prop_k()))
}
/// `PhiGammaModule : Nat → Nat → Type` — (φ, Γ)-module.
pub fn phi_gamma_module_ty() -> Expr {
    arrow_k(nat_k(), arrow_k(nat_k(), type0_k()))
}
/// `BergerEquivalence : Prop` — Berger's equivalence of categories.
pub fn berger_equivalence_ty() -> Expr {
    prop_k()
}
/// `FontaineTheory : Nat → Prop` — Fontaine's classification of p-adic representations.
pub fn fontaine_theory_ty() -> Expr {
    arrow_k(nat_k(), prop_k())
}
#[allow(unused_variables)]
pub fn _use_kernel_helpers() {
    let _ = app3(cst("_"), cst("_"), cst("_"), cst("_"));
    let _ = bvar_k(0);
}
/// Build an `Environment` populated with p-adic analysis axioms.
pub fn build_env() -> oxilean_kernel::Environment {
    use oxilean_kernel::{Declaration, Environment, Expr, Level, Name};
    fn prop() -> Expr {
        Expr::Sort(Level::zero())
    }
    fn type0() -> Expr {
        Expr::Sort(Level::succ(Level::zero()))
    }
    fn nat_ty() -> Expr {
        Expr::Const(Name::str("Nat"), vec![])
    }
    fn real_ty() -> Expr {
        Expr::Const(Name::str("Real"), vec![])
    }
    fn arrow(a: Expr, b: Expr) -> Expr {
        Expr::Pi(
            oxilean_kernel::BinderInfo::Default,
            Name::str("_"),
            Box::new(a),
            Box::new(b),
        )
    }
    let mut env = Environment::new();
    let axioms: &[(&str, Expr)] = &[
        ("PAdicInteger", arrow(nat_ty(), type0())),
        ("PAdicNumber", arrow(nat_ty(), type0())),
        ("PAdicValuation", arrow(nat_ty(), arrow(nat_ty(), nat_ty()))),
        (
            "PAdicAbsoluteValue",
            arrow(nat_ty(), arrow(nat_ty(), real_ty())),
        ),
        ("HenselsLemma", prop()),
        ("PAdicExp", arrow(nat_ty(), arrow(real_ty(), real_ty()))),
        ("PAdicLog", arrow(nat_ty(), arrow(real_ty(), real_ty()))),
        ("MahlerExpansion", prop()),
        (
            "TeichmullerLift",
            arrow(nat_ty(), arrow(nat_ty(), nat_ty())),
        ),
        ("IwasawaAlgebra", arrow(nat_ty(), type0())),
        ("IwasawaMainConjecture", prop()),
        ("LocalClassFieldTheory", prop()),
        ("PAdicLieGroup", arrow(nat_ty(), arrow(nat_ty(), type0()))),
        ("WittVector", arrow(nat_ty(), arrow(nat_ty(), type0()))),
        ("StickelbergerElement", arrow(nat_ty(), type0())),
        ("StickelbergerTheorem", prop()),
        (
            "UnramifiedExtension",
            arrow(nat_ty(), arrow(nat_ty(), type0())),
        ),
        (
            "TotallyRamifiedExtension",
            arrow(nat_ty(), arrow(nat_ty(), type0())),
        ),
        ("OstrowskiTheorem", prop()),
        ("PAdicCompleteness", prop()),
        ("MahlerTheoremContinuity", prop()),
        ("PAdicBanachSpace", arrow(nat_ty(), type0())),
        ("MahlerBasis", arrow(nat_ty(), prop())),
        ("BanachSteinhausPadic", prop()),
        ("WeierstraussPrep", arrow(nat_ty(), arrow(nat_ty(), prop()))),
        ("KrasnersLemma", prop()),
        ("LocallyAnalyticFunctions", arrow(nat_ty(), type0())),
        ("PAdicDistributions", arrow(nat_ty(), type0())),
        ("AmiceTransform", arrow(nat_ty(), prop())),
        (
            "VolkenbornIntegral",
            arrow(nat_ty(), arrow(arrow(nat_ty(), real_ty()), real_ty())),
        ),
        ("ShnirelmanIntegral", prop()),
        (
            "KubotaLeopoldt",
            arrow(nat_ty(), arrow(nat_ty(), real_ty())),
        ),
        (
            "IwasawaInvariants",
            arrow(nat_ty(), arrow(nat_ty(), nat_ty())),
        ),
        ("MuZeroConjecture", arrow(nat_ty(), prop())),
        (
            "PAdicDifferentialEquation",
            arrow(nat_ty(), arrow(nat_ty(), type0())),
        ),
        ("DworkTheorem", arrow(nat_ty(), prop())),
        ("MonodromyTheorem", prop()),
        (
            "FrobeniusStructure",
            arrow(nat_ty(), arrow(nat_ty(), prop())),
        ),
        (
            "ContinuousCohomology",
            arrow(type0(), arrow(type0(), arrow(nat_ty(), type0()))),
        ),
        (
            "ExtGroup",
            arrow(nat_ty(), arrow(type0(), arrow(type0(), type0()))),
        ),
        ("TateAlgebra", arrow(nat_ty(), arrow(nat_ty(), type0()))),
        ("AffinoidSpace", arrow(nat_ty(), arrow(nat_ty(), type0()))),
        (
            "RigidAnalyticSpace",
            arrow(nat_ty(), arrow(nat_ty(), type0())),
        ),
        ("RigidGAGA", prop()),
        (
            "OverconvergentFunctions",
            arrow(nat_ty(), arrow(real_ty(), type0())),
        ),
        ("RobbaRing", arrow(nat_ty(), type0())),
        (
            "DworkHypergeometric",
            arrow(nat_ty(), arrow(real_ty(), real_ty())),
        ),
        (
            "LubinTateFormalGroup",
            arrow(nat_ty(), arrow(nat_ty(), type0())),
        ),
        (
            "FormalExponential",
            arrow(nat_ty(), arrow(real_ty(), real_ty())),
        ),
        (
            "FormalLogarithm",
            arrow(nat_ty(), arrow(real_ty(), real_ty())),
        ),
        ("LubinTateCFT", arrow(nat_ty(), prop())),
        ("ColemanPowerSeries", arrow(nat_ty(), type0())),
        ("ColemanTheorem", arrow(nat_ty(), prop())),
        ("ColemanIntegration", arrow(nat_ty(), prop())),
        ("NormCompatibleSequence", arrow(nat_ty(), type0())),
        ("MahlerTransform", arrow(nat_ty(), type0())),
        ("CharacteristicSeries", arrow(nat_ty(), type0())),
        ("PAdicMeasure", arrow(nat_ty(), type0())),
        ("IwasawaMainConjectureGen", arrow(nat_ty(), prop())),
        (
            "GaloisRepresentation",
            arrow(nat_ty(), arrow(nat_ty(), type0())),
        ),
        (
            "DeRhamRepresentation",
            arrow(nat_ty(), arrow(nat_ty(), prop())),
        ),
        (
            "CrystallineRepresentation",
            arrow(nat_ty(), arrow(nat_ty(), prop())),
        ),
        (
            "SemistableRepresentation",
            arrow(nat_ty(), arrow(nat_ty(), prop())),
        ),
        ("PhiGammaModule", arrow(nat_ty(), arrow(nat_ty(), type0()))),
        ("BergerEquivalence", prop()),
        ("FontaineTheory", arrow(nat_ty(), prop())),
    ];
    for (name, ty) in axioms {
        env.add(Declaration::Axiom {
            name: Name::str(*name),
            univ_params: vec![],
            ty: ty.clone(),
        })
        .ok();
    }
    env
}
#[cfg(test)]
mod tests {
    use super::*;
    #[test]
    fn test_padic_integer_new() {
        let x = PAdicInteger::new(5, 37);
        assert_eq!(x.p, 5);
        assert_eq!(x.digits, vec![2, 2, 1]);
    }
    #[test]
    fn test_padic_integer_zero_one() {
        let z = PAdicInteger::zero(7);
        assert_eq!(z.digits, vec![0]);
        let o = PAdicInteger::one(7);
        assert_eq!(o.digits, vec![1]);
    }
    #[test]
    fn test_padic_number_valuation() {
        let x = PAdicNumber::new(5, 25);
        assert_eq!(x.p_adic_valuation(), 2);
        assert!(x.is_integer());
        assert!(!x.is_unit());
    }
    #[test]
    fn test_padic_valuation_ring() {
        let ring = PAdicValuationRing::new(5);
        let x = PAdicNumber::new(5, 25);
        assert!(ring.contains(&x));
    }
    #[test]
    fn test_padic_absolute_value() {
        let abs = PAdicAbsoluteValue::new(5);
        let val = abs.evaluate(25);
        assert!((val - 0.04).abs() < 1e-10);
        assert!(abs.ultrametric_inequality());
    }
    #[test]
    fn test_ultrametric_statement() {
        let s = ultrametric_triangle_inequality_statement();
        assert!(s.contains("ultrametric"));
    }
    #[test]
    fn test_ostrowski_statement() {
        let s = ostrowski_theorem_statement();
        assert!(s.contains("Ostrowski"));
    }
    #[test]
    fn test_polynomial_mod_evaluate() {
        let f = PolynomialMod::new(vec![-1, 0, 1], 5);
        assert_eq!(f.evaluate(1), 0);
        assert_eq!(f.evaluate(4), 0);
    }
    #[test]
    fn test_polynomial_mod_derivative() {
        let f = PolynomialMod::new(vec![-1, 0, 1], 5);
        let fp = f.derivative();
        assert_eq!(fp.evaluate(1), 2);
    }
    #[test]
    fn test_hensel_lemma_statement() {
        let s = hensel_lemma_statement();
        assert!(s.contains("Hensel"));
    }
    #[test]
    fn test_hensel_lift_simple() {
        let f = PolynomialMod::new(vec![-2, 0, 1], 7);
        let result = hensel_lift(&f, 3, 7, 3);
        assert!(result.is_some());
    }
    #[test]
    fn test_newton_polygon() {
        let poly = PolynomialMod::new(vec![5, 0, 1], 5);
        let np = NewtonPolygon::new(poly);
        assert!(!np.vertices.is_empty());
    }
    #[test]
    fn test_padic_exp_convergence() {
        let r = padic_exp_convergence(5);
        assert!(r > 0.0 && r < 1.0);
        let r2 = padic_exp_convergence(2);
        assert!((r2 - 0.25).abs() < 1e-10);
    }
    #[test]
    fn test_padic_exp_series() {
        let exp5 = PAdicExp::new(5);
        let val = exp5.evaluate_series(0.1, 10);
        assert!((val - 1.10517).abs() < 0.01);
    }
    #[test]
    fn test_padic_log_series() {
        let log5 = PAdicLog::new(5);
        let val = log5.evaluate_series(1.1, 20);
        assert!((val - 0.09531).abs() < 0.01);
    }
    #[test]
    fn test_iwasawa_algebra() {
        let alg = IwasawaAlgebra::new(5);
        assert!(alg.is_noetherian());
        assert_eq!(alg.krull_dimension(), 2);
        assert!(alg.group_ring.contains("5"));
    }
    #[test]
    fn test_iwasawa_module() {
        let alg = IwasawaAlgebra::new(5);
        let m = IwasawaModule::new(alg, 0, "X_∞".to_string());
        let stmt = m.structural_theorem_statement();
        assert!(stmt.contains("pseudo-isomorphic"));
    }
    #[test]
    fn test_iwasawa_main_conjecture() {
        let s = iwasawa_main_conjecture_statement();
        assert!(s.contains("Iwasawa"));
    }
    #[test]
    fn test_profinite_group() {
        let g = ProfiniteGroup::new("ℤ_p");
        assert!(g.is_abelian());
    }
    #[test]
    fn test_zp_star() {
        let g = ZpStar::new(5);
        assert!(g.order().is_none());
        let gens = g.generators();
        assert!(!gens.is_empty());
    }
    #[test]
    fn test_padic_lie_group() {
        let g = PAdicLieGroup::new(5, 1);
        assert!(g.is_compact());
        assert!(g.is_abelian());
        let g2 = PAdicLieGroup::new(5, 2);
        assert!(!g2.is_abelian());
    }
    #[test]
    fn test_witt_vector() {
        let w = WittVector::new(5, 3);
        assert_eq!(w.components.len(), 3);
        let gh = w.ghost_components();
        assert_eq!(gh.len(), 3);
    }
    #[test]
    fn test_witt_vector_formula() {
        let s = witt_vector_addition_formula(5, 2);
        assert!(s.contains("Witt"));
    }
    #[test]
    fn test_witt_ring_characteristic() {
        let wr = WittRing::new(5);
        assert_eq!(wr.characteristic(), 0);
    }
    #[test]
    fn test_local_field() {
        let lf = LocalField::new(5, 3, 1);
        assert_eq!(lf.degree, 3);
        assert!(lf.is_tamely_ramified());
        assert!(!lf.is_wildly_ramified());
    }
    #[test]
    fn test_local_field_wild() {
        let lf = LocalField::new(5, 5, 1);
        assert!(lf.is_wildly_ramified());
        assert!(!lf.is_tamely_ramified());
    }
    #[test]
    fn test_unramified_extension() {
        let ue = UnramifiedExtension::new(5, 3);
        assert_eq!(ue.residue_field_size(), 125);
    }
    #[test]
    fn test_local_cft_statement() {
        let s = local_class_field_theory_statement();
        assert!(s.contains("Local Class Field Theory"));
    }
    #[test]
    fn test_padic_banach_space() {
        let bs = PAdicBanachSpace::new(5, "C(ℤ_p, ℚ_p)", true);
        assert!(bs.is_complete());
        assert!(bs.mahler_basis_orthonormal());
        let stmt = bs.banach_steinhaus_statement();
        assert!(stmt.contains("Banach-Steinhaus"));
    }
    #[test]
    fn test_mahler_transform() {
        let mt = MahlerTransform::new(5, vec![0.0, 1.0, 4.0, 9.0]);
        let a0 = mt.mahler_coefficient(0);
        assert!((a0 - 0.0).abs() < 1e-9);
        let a1 = mt.mahler_coefficient(1);
        assert!((a1 - 1.0).abs() < 1e-9);
        assert!(mt.is_bijection_onto_null_sequences());
        let desc = mt.characteristic_series_description();
        assert!(desc.contains("characteristic series"));
    }
    #[test]
    fn test_weierstrauss_prep() {
        let w = WeierstrausPrepTheorem::new(5, 2);
        assert!(w.factorization_exists());
        assert!(w.factorization_is_unique());
        let stmt = w.statement();
        assert!(stmt.contains("Weierstrass Preparation"));
    }
    #[test]
    fn test_krasners_lemma() {
        let s = krasners_lemma_statement();
        assert!(s.contains("Krasner"));
    }
    #[test]
    fn test_power_series_ring_ufd() {
        let s = power_series_ring_ufd_statement();
        assert!(s.contains("UFD"));
    }
    #[test]
    fn test_locally_analytic_functions() {
        let laf = LocallyAnalyticFunctions::new(5, "ℚ_p");
        assert!(laf.dense_in_continuous());
        let stmt = laf.locally_analytic_rep_statement();
        assert!(stmt.contains("locally analytic"));
    }
    #[test]
    fn test_padic_distributions() {
        let d = PAdicDistributions::new(5);
        assert!(d.is_locally_convex());
        let stmt = d.amice_transform_statement();
        assert!(stmt.contains("Amice"));
    }
    #[test]
    fn test_volkenborn_integral() {
        let vi = VolkenbornIntegral::new(5);
        assert!(vi.normalizes_to_one());
        let approx = vi.finite_sum_approximation(&[1.0], 2);
        assert!((approx - 1.0).abs() < 1e-9);
        let stmt = vi.bernoulli_connection_statement();
        assert!(stmt.contains("Bernoulli"));
    }
    #[test]
    fn test_shnirelman_integral() {
        let s = shnirelman_integral_statement();
        assert!(s.contains("Shnirelman") || s.contains("Tate"));
    }
    #[test]
    fn test_kubota_leopoldt() {
        let kl = KubotaLeopoldt::new(5, 1);
        assert!(kl.is_padic_analytic());
        let stmt = kl.interpolation_statement();
        assert!(stmt.contains("Kubota-Leopoldt") || stmt.contains("interpolation"));
    }
    #[test]
    fn test_iwasawa_invariants() {
        let inv = IwasawaInvariants::new(5, 0, 3);
        assert_eq!(inv.mu_invariant, 0);
        assert_eq!(inv.lambda_invariant, 3);
        let stmt = inv.mu_zero_conjecture_statement();
        assert!(stmt.contains("μ-conjecture") || stmt.contains("mu"));
    }
    #[test]
    fn test_padic_differential_equation() {
        let de = PAdicDifferentialEquation::new(5, 2);
        let stmt1 = de.dworks_theorem_statement();
        assert!(stmt1.contains("Dwork"));
        let stmt2 = de.monodromy_theorem_statement();
        assert!(stmt2.contains("Monodromy") || stmt2.contains("monodromy"));
        let stmt3 = de.frobenius_structure_statement();
        assert!(stmt3.contains("Frobenius"));
    }
    #[test]
    fn test_continuous_cohomology() {
        let cc = ContinuousCohomology::new("Gal(ℚ̄_p/ℚ_p)", "ℚ_p", 1);
        let desc = cc.description();
        assert!(desc.contains("cohomology"));
        assert!(!cc.vanishes_above_dimension(2));
        let stmt = cc.ext_group_statement();
        assert!(stmt.contains("Ext"));
    }
    #[test]
    fn test_tate_algebra() {
        let ta = TateAlgebra::new(5, 3);
        assert!(ta.is_noetherian());
        assert!(ta.is_ufd());
        assert_eq!(ta.krull_dimension(), 3);
        let stmt = ta.polydisk_statement();
        assert!(stmt.contains("polydisk") || stmt.contains("Tate"));
    }
    #[test]
    fn test_affinoid_space() {
        let af = AffinoidSpace::new(5, 2, "T^2 - T - 1 = 0");
        assert!(af.is_noetherian());
        assert_eq!(af.tate_algebra.num_vars, 2);
    }
    #[test]
    fn test_rigid_analytic_space() {
        let ras = RigidAnalyticSpace::new(5, 1, "Drinfeld upper half-plane");
        assert!(ras.is_separated());
        let stmt = ras.gaga_statement();
        assert!(stmt.contains("GAGA") || stmt.contains("Kiehl"));
    }
    #[test]
    fn test_overconvergent_functions() {
        let ocf = OverconvergentFunctions::new(5, 1.05);
        assert!(ocf.is_subspace_of_formal_series());
        let stmt = ocf.robba_ring_statement();
        assert!(stmt.contains("Robba"));
    }
    #[test]
    fn test_dwork_hypergeometric() {
        let s = dwork_hypergeometric_statement();
        assert!(s.contains("Dwork"));
    }
    #[test]
    fn test_lubin_tate_formal_group() {
        let lt = LubinTateFormalGroup::new(5, 5);
        let stmt1 = lt.formal_group_law_description();
        assert!(stmt1.contains("Lubin-Tate") || stmt1.contains("formal"));
        let stmt2 = lt.formal_exponential_statement();
        assert!(stmt2.contains("exponential"));
        let stmt3 = lt.formal_logarithm_statement();
        assert!(stmt3.contains("logarithm"));
        let stmt4 = lt.local_cft_via_lubin_tate();
        assert!(stmt4.contains("abelian"));
    }
    #[test]
    fn test_coleman_power_series() {
        let cps = ColemanPowerSeries::new(5, vec![1.0, 0.5, 0.25]);
        assert!(cps.converges_on_unit_disk());
        let stmt = cps.colemans_theorem_statement();
        assert!(stmt.contains("Coleman"));
        let val = cps.evaluate_at(0.1);
        assert!((val - 1.0525).abs() < 1e-9);
    }
    #[test]
    fn test_coleman_integration_statement() {
        let s = coleman_integration_statement();
        assert!(s.contains("Coleman"));
    }
    #[test]
    fn test_build_env_new_axioms() {
        let env = build_env();
        use oxilean_kernel::Name;
        assert!(env.get(&Name::str("PAdicBanachSpace")).is_some());
        assert!(env.get(&Name::str("TateAlgebra")).is_some());
        assert!(env.get(&Name::str("LubinTateFormalGroup")).is_some());
        assert!(env.get(&Name::str("ColemanTheorem")).is_some());
        assert!(env.get(&Name::str("KrasnersLemma")).is_some());
        assert!(env.get(&Name::str("PhiGammaModule")).is_some());
        assert!(env.get(&Name::str("BergerEquivalence")).is_some());
        assert!(env.get(&Name::str("FontaineTheory")).is_some());
    }
}