Documentation

LeanPool.ConwayRefinement.ConwayRefinement.HahnSeries.OrdinalValue.Tests.ResidualPoint

API checks for Berarducci residual points #

The approach-zero series has ordinal value ω, hence principal value ω and residual value one. Its least support exponent is -1. Closed truncation at that exponent retains the coefficient-one monomial, and translation turns it into the constant-one series, so -1 belongs to X(b).

This example separates Definition 6.6 from two nearby errors. Replacing residual value by principal value would reject -1, while using strict rather than closed truncation would give the zero series at -1. The endpoint zero is also excluded, but this is not a semantic separator for the printed strict inequality: on the domain 1 < v_J(b), the value equation itself already excludes zero, as proved in the definition module.

The final test uses the same residual point to distinguish the strict tail cutoff (η, 0) from the nearby closed cutoff [η, 0): the point -1 lies above -2, but not strictly above itself.

The cofinality certificate produces a residual point strictly between -1/1000 and zero. It therefore distinguishes the proved conclusion of Lemma 6.8 from the nearby false assertion that the residual-point set of this series consists only of its least exponent -1.

source
noncomputable def Tests.approachZeroResidualInput :
Berarducci.SeriesWithOrdinalValueAboveOne ℚ

The approach-zero series in the exact domain of principal, residual, and residual-point operations.

Equations
Instances For
    source
    @[simp]
    theorem Tests.coe_approachZeroResidualInput :
    ↑approachZeroResidualInput = approachZeroNonpositive

    The packaged residual-point input has the intended underlying Hahn series.

    source
    theorem Tests.approachZero_ordinalValue_eq_omega :
    Berarducci.ordinalValue approachZeroNonpositive = NatOrdinal.of Ordinal.omega0

    The Berarducci ordinal value of the approach-zero series is ω.

    source
    theorem Tests.approachZero_principalValue_eq_omega_and_residualValue_eq_one :
    approachZeroResidualInput.principalValue = NatOrdinal.of Ordinal.omega0 ∧ approachZeroResidualInput.residualValue = 1

    The approach-zero series has principal value ω and residual value one.

    source
    theorem Tests.translatedTruncation_approachZero_neg_one :
    Berarducci.translatedTruncation approachZero (-1) = HahnSeries.Nonpositive.C 1

    Closed truncation of the approach-zero series at its least exponent, translated to zero, is the constant-one series.

    source
    theorem Tests.approachZero_residualPointSet_boundary :
    -1 ∈ Berarducci.residualPointSet approachZeroResidualInput ∧ 0 ∉ Berarducci.residualPointSet approachZeroResidualInput

    The least exponent is a residual point, whereas zero fails the value equation and is excluded.

    source
    theorem Tests.approachZero_residualPointSet_cofinal_near_zero :
    ∃ γ ∈ Berarducci.residualPointSet approachZeroResidualInput, -1 / 1000 < γ ∧ γ < 0

    The residual-point set contains a point strictly between -1/1000 and zero.

    source
    theorem Tests.approachZero_residualPointTail_strict_cutoff :
    -1 ∈ Berarducci.residualPointTail approachZeroResidualInput (-2) ∧ -1 ∉ Berarducci.residualPointTail approachZeroResidualInput (-1)

    The least exponent belongs to the tail cut at -2 but not to the tail cut at -1. This separates the strict cutoff in residualPointTail from a closed cutoff.