logicaffeine_base/

tower.rs

//! The exact real types in a program's value model: real algebraic numbers, computable reals, the
//! program's infinitesimal and the hyperreals it generates, infinite integers, ordinals, and the
//! values a supertask leaves.
//!
//! Each type lives in its own module of this crate; this module decides how they mix with the
//! numeric tower and with each other, once, for every value model that holds them. A value model
//! (the interpreter's runtime value, a compiled program's value) implements [`TowerValue`]: how to
//! see one of its values as an exact type or a standard number, and how to build one. Everything
//! here is generic over it, so every tier computes, compares and prints these values identically.
//!
//! - an integer, rational or float operand is lifted exactly (a float is the dyadic rational it
//!   denotes, never a rounding of the other side) into the exact type it meets;
//! - real algebraic numbers sit below computable reals; the hyperreals are generated by the
//!   infinitesimal over the algebraic numbers, exactly as rational functions of `dt`; a value a flow
//!   leaves, or a computable transcendental meeting the infinitesimal, is a germ — known by its
//!   series in `dt` with exact coefficients, compared by the sign of its first nonzero one;
//! - an infinite integer meets a standard integer as an infinite integer (`+ − ×`, floor division
//!   and remainder keep integer meaning) and anything fractional as a hyperreal;
//! - a value that depends on the residue of `1/dt` lifts every operation branch by branch, and a
//!   comparison of infinite integers can itself depend on that residue;
//! - an ordinal meets only ordinals and naturals.
//!
//! Every result is held in its smallest exact form — a hyperreal with no infinitesimal part is
//! its standard value, a hyperreal that is an integer for every admitted `⌈1/dt⌉` is that infinite
//! integer, an algebraic number that is rational is a rational — so a value has one representation
//! whatever route produced it, exactly as the tower downsizes `BigInt` to `Int`.

use std::cell::RefCell;
use std::cmp::Ordering;
use std::sync::Arc;

use crate::algebraic::{negative_root, Algebraic};
use crate::exact_codec::ExactCodec;
use crate::exact_real::{ExactReal, DEFAULT_BUDGET};
use crate::germ::Germ;
use crate::hypernatural::Hypernatural;
use crate::hyperreal::Hyperreal;
use crate::limit_value::{Converging, Depends, LimitRule, ResidueError, ResidueType};
use crate::multi::Multi;
use crate::nested::NestedGerm;
use crate::number::Number;
use crate::numeric::{BigInt, Rational};
use crate::ordered_field::{OrderedField, PolyOver};
use crate::ordinal::Ordinal;
use crate::poly::Poly;
use crate::puiseux::{Closed, Puiseux};

/// An infinitesimal of the program: the name it was declared under, what is known about the
/// residues of its reciprocal, the infinite natural `⌈1/dt⌉`, and where it stands among the others.
///
/// `dx` declared much smaller than `dt` is smaller than every positive number made from `dt`, so the
/// two are ordered as levels: every value of `dx` with coefficients made from `dt` has the sign of
/// its lowest-order coefficient in `dx`. A declaration names at most one infinitesimal it is much
/// smaller than and one it is much larger than, and the order of any two is what those statements
/// give by transitivity ([`Scale::order`]); two the declarations do not order are never combined.
#[derive(Debug, PartialEq, Eq, Hash)]
pub struct Scale {
    pub name: String,
    pub residues: ResidueType,
    /// The infinitesimal this one was declared much smaller than.
    pub much_smaller_than: Option<Arc<Scale>>,
    /// The infinitesimal this one was declared much larger than.
    pub much_larger_than: Option<Arc<Scale>>,
    /// The declared infinitesimal this is, read on one residue class of its reciprocal: the
    /// engine's copy for a class keeps the declaration it refines, and is that infinitesimal.
    pub refines: Option<Arc<Scale>>,
}

impl Scale {
    /// An infinitesimal declared on its own.
    pub fn new(name: &str, residues: ResidueType) -> Scale {
        Scale {
            name: name.to_string(),
            residues,
            much_smaller_than: None,
            much_larger_than: None,
            refines: None,
        }
    }

    /// An infinitesimal declared much smaller than `larger` and much larger than `smaller`, each
    /// when given; refused when the bounds are not already ordered, smaller below larger, or when it
    /// would share a name with an infinitesimal it is ordered with.
    pub fn ordered(
        name: &str,
        residues: ResidueType,
        larger: Option<Arc<Scale>>,
        smaller: Option<Arc<Scale>>,
    ) -> Result<Scale, String> {
        if let (Some(l), Some(s)) = (&larger, &smaller) {
            match s.order(l) {
                Some(Ordering::Less) => {}
                Some(Ordering::Equal) => {
                    return Err(format!("{name} cannot be both much smaller and much larger than {}", l.name))
                }
                Some(Ordering::Greater) => {
                    return Err(format!(
                        "{name} is declared much smaller than {} and much larger than {}, but {} is much larger than {}",
                        l.name, s.name, s.name, l.name
                    ))
                }
                None => {
                    return Err(format!(
                        "{name} is declared much smaller than {} and much larger than {}, but the program does not state that {} is much smaller than {}",
                        l.name, s.name, s.name, l.name
                    ))
                }
            }
        }
        let related = larger
            .iter()
            .flat_map(|l| l.larger_chain())
            .chain(smaller.iter().flat_map(|s| s.smaller_chain()));
        if let Some(clash) = related.into_iter().find(|s| s.name == name) {
            return Err(format!(
                "{name} is ordered with the infinitesimal {}, so it needs a name of its own",
                clash.name
            ));
        }
        Ok(Scale {
            name: name.to_string(),
            residues,
            much_smaller_than: larger,
            much_larger_than: smaller,
            refines: None,
        })
    }

    /// The same infinitesimal on a narrower residue type of its reciprocal.
    pub fn with_residues(self: &Arc<Scale>, residues: ResidueType) -> Scale {
        Scale {
            name: self.name.clone(),
            residues,
            much_smaller_than: self.much_smaller_than.clone(),
            much_larger_than: self.much_larger_than.clone(),
            refines: Some(self.declaration_arc()),
        }
    }

    fn declaration_arc(self: &Arc<Scale>) -> Arc<Scale> {
        match &self.refines {
            Some(d) => d.clone(),
            None => self.clone(),
        }
    }

    /// The declaration this infinitesimal is: itself, or the one a residue class's copy refines.
    fn declaration(&self) -> &Scale {
        self.refines.as_deref().unwrap_or(self)
    }

    /// Whether the two are one infinitesimal: one declaration, whatever residue class either is read on.
    pub fn same_infinitesimal(&self, o: &Scale) -> bool {
        std::ptr::eq(self.declaration(), o.declaration()) || self.declaration() == o.declaration()
    }

    /// This infinitesimal and each it was declared much smaller than, in turn.
    fn larger_chain(&self) -> Vec<&Scale> {
        let mut out = vec![self];
        let mut at = self;
        while let Some(next) = at.much_smaller_than.as_deref() {
            out.push(next);
            at = next;
        }
        out
    }

    /// This infinitesimal and each it was declared much larger than, in turn.
    fn smaller_chain(&self) -> Vec<&Scale> {
        let mut out = vec![self];
        let mut at = self;
        while let Some(next) = at.much_larger_than.as_deref() {
            out.push(next);
            at = next;
        }
        out
    }

    /// `Less` when this infinitesimal is much smaller than `o`, `Greater` when much larger, `Equal`
    /// for one infinitesimal; `None` when the declarations do not order them. `a` is much smaller than
    /// `b` when some infinitesimal reached from `a` through the ones declared above it is reached
    /// from `b` through the ones declared below it: every declaration states its bounds' order
    /// already known, so no later one orders two earlier ones, and that meeting is the only route.
    pub fn order(&self, o: &Scale) -> Option<Ordering> {
        if self.same_infinitesimal(o) {
            return Some(Ordering::Equal);
        }
        let meets = |low: &Scale, high: &Scale| {
            let up = low.declaration().larger_chain();
            let down = high.declaration().smaller_chain();
            up.iter().any(|u| down.iter().any(|d| u.same_infinitesimal(d)))
        };
        if meets(self, o) {
            Some(Ordering::Less)
        } else if meets(o, self) {
            Some(Ordering::Greater)
        } else {
            None
        }
    }

    /// The refusal for two infinitesimals whose order the program does not state.
    pub fn unordered(&self, o: &Scale) -> String {
        format!(
            "cannot combine values of two infinitesimals, {} and {}, whose order the program does not state; declare one much smaller than the other",
            self.name, o.name
        )
    }

    /// How the infinite generator is written in a dependence: `⌈1/dt⌉`.
    pub fn generator_text(&self) -> String {
        format!("⌈1/{}⌉", self.name)
    }

    /// A residue system the value would need, refused in the program's own words.
    fn refuse(&self, e: ResidueError) -> String {
        e.describe(&self.generator_text())
    }
}

/// A hyperreal's representations: an exact rational function of `dt`; a real algebraic Puiseux
/// series that is none, a root of one ([`crate::puiseux`]); the germ a flow leaves, known by its
/// series in `dt`; or a value of several ordered infinitesimals ([`Multi`]). A Puiseux series compares
/// and hashes by its value, a germ by its canonical encoding.
#[derive(Debug, Clone)]
pub enum HyperForm {
    Rational(Hyperreal),
    Puiseux(Puiseux),
    Germ(Germ),
    Multi(Multi),
    /// An infinite integer of several infinitesimals — `⌊1/dt + 1/dx⌋`, a step count of `⌈1/(dt·dx)⌉`: a
    /// value of several that is a polynomial in their reciprocals with rational coefficients and an
    /// integer on every class the facts its scales carry admit (`Multi::is_integral`), as a polynomial
    /// in one infinitesimal's reciprocal that is one is an infinite integer of it. It computes and
    /// compares as the value it is, and prints as an infinite integer does.
    Integer(Multi),
    Nested(Arc<NestedGerm>),
}

impl PartialEq for HyperForm {
    fn eq(&self, o: &Self) -> bool {
        match (self, o) {
            (HyperForm::Rational(a), HyperForm::Rational(b)) => a == b,
            (HyperForm::Puiseux(a), HyperForm::Puiseux(b)) => {
                Closed::Series(a.clone()) == Closed::Series(b.clone())
            }
            (HyperForm::Germ(a), HyperForm::Germ(b)) => a.to_bytes() == b.to_bytes(),
            (HyperForm::Multi(a) | HyperForm::Integer(a), HyperForm::Multi(b) | HyperForm::Integer(b)) => a == b,
            (HyperForm::Nested(a), HyperForm::Nested(b)) => NestedGerm::same_recipe(a, b),
            _ => false,
        }
    }
}

impl Eq for HyperForm {}

impl std::hash::Hash for HyperForm {
    fn hash<H: std::hash::Hasher>(&self, state: &mut H) {
        match self {
            HyperForm::Rational(h) => {
                0u8.hash(state);
                h.hash(state);
            }
            HyperForm::Germ(g) => {
                1u8.hash(state);
                g.to_bytes().hash(state);
            }
            HyperForm::Puiseux(p) => {
                2u8.hash(state);
                Closed::Series(p.clone()).hash(state);
            }
            HyperForm::Multi(m) | HyperForm::Integer(m) => {
                3u8.hash(state);
                m.hash(state);
            }
            HyperForm::Nested(g) => {
                4u8.hash(state);
                g.scale.name.hash(state);
            }
        }
    }
}

impl HyperForm {
    /// The rational function, when the value is one.
    pub fn rational(&self) -> Option<&Hyperreal> {
        match self {
            HyperForm::Rational(h) => Some(h),
            HyperForm::Puiseux(_)
            | HyperForm::Germ(_)
            | HyperForm::Multi(_)
            | HyperForm::Integer(_)
            | HyperForm::Nested(_) => None,
        }
    }

    /// How the value prints, its infinitesimal written `name`; a value of several prints each by its
    /// own name.
    pub fn render(&self, name: &str) -> String {
        match self {
            HyperForm::Rational(h) => h.render(name),
            HyperForm::Puiseux(p) => Closed::Series(p.clone()).render(name),
            HyperForm::Germ(g) => g.render(name),
            HyperForm::Multi(m) | HyperForm::Integer(m) => m.render(),
            HyperForm::Nested(g) => g.render(),
        }
    }
}

/// A hyperreal value with the infinitesimal it is written in.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct HyperValue {
    pub value: HyperForm,
    pub scale: Arc<Scale>,
}

/// An infinite integer with the infinitesimal whose reciprocal generates it.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct NaturalValue {
    pub value: Hypernatural,
    pub scale: Arc<Scale>,
}

/// One branch of a residue-dependent value, compared by value.
#[derive(Debug, Clone)]
pub struct Branch<V>(pub V);

impl<V: TowerValue> PartialEq for Branch<V> {
    fn eq(&self, o: &Self) -> bool {
        self.0.values_equal(&o.0)
    }
}

/// A value that depends on the residue of `⌈1/dt⌉`.
#[derive(Debug, Clone)]
pub struct DependsValue<V> {
    pub value: Depends<Branch<V>>,
    pub scale: Arc<Scale>,
}

/// A value of a value model seen as one of the types this module governs.
pub enum ExactRef<'a, V> {
    Algebraic(&'a Algebraic),
    Real(&'a ExactReal),
    Hyper(&'a HyperValue),
    Natural(&'a NaturalValue),
    Ordinal(&'a Ordinal),
    Depends(&'a DependsValue<V>),
    Converging(&'a Converging<V>),
}

/// A value model that holds the exact types: how to see a value as one of them or as a standard
/// number, and how to build one. The interpreter's runtime value and a compiled program's value
/// each implement it; every operation in this module is generic over it.
pub trait TowerValue: Clone + Sized {
    /// The value as one of the exact types, or `None` for any other value.
    fn exact(&self) -> Option<ExactRef<'_, Self>>;
    /// An integer, rational, decimal or finite float as the rational it denotes exactly.
    fn standard_rational(&self) -> Option<Rational>;
    /// An `Int` or big integer.
    fn integer(&self) -> Option<BigInt>;
    /// An integer or a rational: a number held exactly, never a float or a decimal.
    fn exact_rational(&self) -> Option<Rational>;
    /// An integer, rational, decimal or float: its own standard part.
    fn is_standard_number(&self) -> bool;
    /// A `Text` value's characters.
    fn text(&self) -> Option<&str>;
    /// The value's type as the language names it.
    fn type_name(&self) -> String;
    /// How the value prints.
    fn display_string(&self) -> String;
    /// The language's equality on two values.
    fn values_equal(&self, other: &Self) -> bool;
    /// Whether the value is `nothing`.
    fn is_nothing(&self) -> bool;

    /// A rational in its smallest form: an `Int` when it fits, a big integer, else a rational.
    fn from_rational(r: Rational) -> Self;
    /// An integer in its smallest form.
    fn from_bigint(b: BigInt) -> Self;
    fn boolean(b: bool) -> Self;
    fn nothing() -> Self;
    fn algebraic(a: Algebraic) -> Self;
    fn exact_real(x: ExactReal) -> Self;
    fn hyper(h: HyperValue) -> Self;
    fn natural(n: NaturalValue) -> Self;
    fn ordinal(o: Ordinal) -> Self;
    fn depends(d: DependsValue<Self>) -> Self;
    fn converging(c: Converging<Self>) -> Self;
}

/// A value's structure, as far as the supertask runtime reads it: the scalar kinds it treats apart,
/// and the items of a list or a tuple.
pub enum Shape<V> {
    Bool,
    Int(i64),
    Float,
    BigInt(BigInt),
    Rational(Rational),
    Decimal,
    /// Text of this many bytes.
    Text(usize),
    List(Vec<V>),
    Tuple(Vec<V>),
    Other,
}

/// A value model's whole arithmetic and its lists: what the supertask runtime computes with. Each
/// operation is the language's own on that model, exact types and standard numbers alike.
pub trait ValueAlgebra: TowerValue {
    fn add(a: Self, b: Self) -> Result<Self, String>;
    fn subtract(a: Self, b: Self) -> Result<Self, String>;
    fn multiply(a: Self, b: Self) -> Result<Self, String>;
    /// `/` in an exact context: field division, integers included.
    fn exact_divide(a: Self, b: Self) -> Result<Self, String>;
    /// The language's `%`.
    fn modulo(a: Self, b: Self) -> Result<Self, String>;
    /// Whether `a rel b` holds, decided: an answer that depends on the residue, or a provisional
    /// one, is the refusal of the branch.
    fn holds(rel: Rel, a: &Self, b: &Self) -> Result<bool, String>;
    /// The language's `**`.
    fn power(a: Self, b: Self) -> Result<Self, String>;
    /// The language's `floor`.
    fn floor(v: Self) -> Result<Self, String>;
    /// The language's `ceiling`.
    fn ceil(v: Self) -> Result<Self, String>;
    fn list(values: Vec<Self>) -> Self;
    fn shape(&self) -> Shape<Self>;
}

/// The canonical value of an algebraic number: a rational is an `Int`/`BigInt`/`Rational`.
pub fn from_algebraic<V: TowerValue>(a: Algebraic) -> V {
    match a.to_rational() {
        Some(r) => V::from_rational(r),
        None => V::algebraic(a),
    }
}

/// The canonical value of a computable real: an algebraic one is an algebraic number.
pub fn from_exact_real<V: TowerValue>(x: ExactReal) -> V {
    match x.exact_algebraic() {
        Some(a) => from_algebraic(a),
        None => V::exact_real(x),
    }
}

/// The canonical value of a hyperreal: a standard value is its standard part, and a polynomial in
/// `1/dt` that is an integer for every admitted `⌈1/dt⌉` is that infinite integer.
pub fn from_hyper<V: TowerValue>(value: Hyperreal, scale: &Arc<Scale>) -> V {
    if let Some(s) = value.as_standard() {
        return from_algebraic(s);
    }
    if let Some(n) = value
        .as_reciprocal_powers()
        .and_then(|c| Hypernatural::from_polynomial(Poly::from_coeffs(c), &scale.residues))
    {
        return from_natural(n, scale);
    }
    V::hyper(HyperValue {
        value: HyperForm::Rational(value),
        scale: scale.clone(),
    })
}

/// The canonical value of a value of the real closure: a rational function of `dt` is that
/// hyperreal, in its own smallest form.
pub fn from_closed<V: TowerValue>(c: Closed, scale: &Arc<Scale>) -> V {
    match c {
        Closed::Field(h) => from_hyper(h, scale),
        Closed::Series(p) => V::hyper(HyperValue {
            value: HyperForm::Puiseux(p),
            scale: scale.clone(),
        }),
    }
}

/// The canonical value of a germ: one built as a rational function of `dt` is that hyperreal.
pub fn from_germ<V: TowerValue>(g: Germ, scale: &Arc<Scale>) -> V {
    if let Some(h) = g.as_hyperreal() {
        return from_hyper(h.clone(), scale);
    }
    V::hyper(HyperValue {
        value: HyperForm::Germ(g),
        scale: scale.clone(),
    })
}

/// The canonical value of an infinite integer: a standard one is an `Int`/`BigInt`, and one whose
/// branches are standard but differ is a residue-dependent integer.
pub fn from_natural<V: TowerValue>(value: Hypernatural, scale: &Arc<Scale>) -> V {
    let finite = value.is_infinite();
    if finite.single() == Some(&false) {
        let ints = value.depends().map(|p| {
            Branch(V::from_bigint(
                p.coeff(0).to_bigint().expect("a standard branch is an integer"),
            ))
        });
        return from_depends(ints, scale);
    }
    V::natural(NaturalValue {
        value,
        scale: scale.clone(),
    })
}

/// The canonical value of a residue-dependent value: a branch that itself depends on the residue
/// is read on its own class, a single branch is that value, and a dependence whose every branch is
/// an integer polynomial in `1/dt` on its class is that infinite integer.
pub fn from_depends<V: TowerValue>(value: Depends<Branch<V>>, scale: &Arc<Scale>) -> V {
    let value = flatten(value, scale);
    if let Some(renested) = coarsest_outside(&value, scale) {
        return renested;
    }
    if let Some(b) = value.single() {
        return b.0.clone();
    }
    if let Some(n) = as_infinite_integer(&value, scale) {
        return from_natural(n, scale);
    }
    V::depends(DependsValue {
        value,
        scale: scale.clone(),
    })
}

/// Whether a value is an integer — a standard one, an infinite integer of one infinitesimal or of
/// several.
fn is_integer_value<V: TowerValue>(v: &V) -> bool {
    v.integer().is_some()
        || matches!(v.exact(), Some(ExactRef::Natural(_)))
        || matches!(v.exact(), Some(ExactRef::Hyper(h)) if matches!(h.value, HyperForm::Integer(_)))
}

/// The canonical value of a value of several infinitesimals: a standard number is that number, and a
/// value of one infinitesimal is that infinitesimal's own.
pub fn from_multi<V: TowerValue>(m: Multi) -> V {
    match m {
        Multi::Standard(a) => from_algebraic(a),
        Multi::One(c, scale) => from_closed(c, &scale),
        Multi::Over { .. } | Multi::Alg(_) => {
            let scale = m.top().expect("a value of several infinitesimals has a smallest").clone();
            let value = if m.is_integral() { HyperForm::Integer(m) } else { HyperForm::Multi(m) };
            V::hyper(HyperValue { value, scale })
        }
    }
}

/// A finite ordinal is a natural number.
pub fn from_ordinal<V: TowerValue>(o: Ordinal) -> V {
    match o.to_natural() {
        Some(n) => V::from_bigint(n),
        None => V::ordinal(o),
    }
}

/// `lcm` of residue moduli, when it is within the bound one value may hold.
fn classes_lcm(moduli: impl Iterator<Item = u64>) -> Option<u64> {
    moduli.into_iter().try_fold(1u64, |acc, m| {
        let g = num_gcd(acc, m);
        let l = u128::from(acc / g) * u128::from(m);
        (l <= u128::from(crate::limit_value::MAX_MODULUS)).then_some(l as u64)
    })
}

fn num_gcd(a: u64, b: u64) -> u64 {
    if b == 0 {
        a
    } else {
        num_gcd(b, a % b)
    }
}

fn depends_of<V: TowerValue>(v: &V) -> Option<&DependsValue<V>> {
    match v.exact()? {
        ExactRef::Depends(d) => Some(d),
        _ => None,
    }
}

fn natural_of<V: TowerValue>(v: &V) -> Option<&NaturalValue> {
    match v.exact()? {
        ExactRef::Natural(n) => Some(n),
        _ => None,
    }
}

/// A dependence on `scale`'s generator whose branches read the residue of a coarser one — the
/// generator of a larger infinitesimal — as the dependence on the coarsest of them whose branches
/// read only finer ones: each class of the coarsest is a case, in which every branch is read on that
/// class. `None` when no branch reads a coarser generator, or the classes would pass the bound.
fn coarsest_outside<V: TowerValue>(value: &Depends<Branch<V>>, scale: &Arc<Scale>) -> Option<V> {
    let mut outer = scale.clone();
    for (_, b) in value.branches() {
        if let Some(g) = residue_generator(&b.0) {
            if g.order(&outer) == Some(Ordering::Greater) {
                outer = g.clone();
            }
        }
    }
    if outer.same_infinitesimal(scale) {
        return None;
    }
    let ty = outer.residues.clone();
    let own = value
        .branches()
        .filter_map(|(_, b)| residue_branches(&b.0).filter(|d| d.scale.same_infinitesimal(&outer)))
        .map(|d| d.value.modulus());
    let m = classes_lcm([ty.modulus()].into_iter().chain(own))?;
    let raw = (0..m)
        .map(|h| {
            ty.admits(h).then(|| {
                let on_class = value.map(|b| match residue_branches(&b.0) {
                    Some(d) if d.scale.same_infinitesimal(&outer) => {
                        d.value.at(h).expect("an admitted class has a branch").clone()
                    }
                    _ => b.clone(),
                });
                Branch(from_depends(on_class, scale))
            })
        })
        .collect();
    Some(from_depends(Depends::from_branches(ty, m, raw)?, &outer))
}

/// Every branch that depends on the residue of the same reciprocal, read on its own class. A
/// dependence whose classes together would pass the bound is left as it is.
fn flatten<V: TowerValue>(value: Depends<Branch<V>>, scale: &Scale) -> Depends<Branch<V>> {
    fn same<'v, V: TowerValue>(v: &'v V, scale: &Scale) -> Option<&'v DependsValue<V>> {
        depends_of(v).filter(|d| d.scale.same_infinitesimal(scale))
    }
    let inner: Vec<u64> = value
        .branches()
        .filter_map(|(_, b)| same(&b.0, scale).map(|d| d.value.modulus()))
        .collect();
    if inner.is_empty() {
        return value;
    }
    let ty = value.residue_type().clone();
    let moduli = [value.modulus(), ty.modulus()].into_iter().chain(inner);
    let Some(l) = classes_lcm(moduli) else {
        return value;
    };
    let raw = (0..l)
        .map(|x| {
            let b = value.at(x)?;
            Some(match same(&b.0, scale) {
                Some(d) => d.value.at(x).expect("an admitted class has a branch").clone(),
                None => b.clone(),
            })
        })
        .collect();
    Depends::from_branches(ty, l, raw).expect("the classes are the type's own")
}

/// The dependence as one infinite integer, when every branch is an integer polynomial in `1/dt`
/// on its class and at least one is infinite.
fn as_infinite_integer<V: TowerValue>(value: &Depends<Branch<V>>, scale: &Scale) -> Option<Hypernatural> {
    let ty = value.residue_type().clone();
    let own = value
        .branches()
        .filter_map(|(_, b)| natural_of(&b.0).filter(|n| n.scale.same_infinitesimal(scale)))
        .map(|n| n.value.depends().modulus());
    let l = classes_lcm([value.modulus(), ty.modulus()].into_iter().chain(own))?;
    let mut infinite = false;
    let mut raw = Vec::with_capacity(l as usize);
    for x in 0..l {
        let Some(b) = value.at(x) else {
            raw.push(None);
            continue;
        };
        let p = if let Some(n) = b.0.integer() {
            Poly::constant(Rational::from_bigint(n))
        } else {
            match b.0.exact() {
                Some(ExactRef::Natural(n)) if n.scale.same_infinitesimal(scale) => {
                    infinite = true;
                    n.value.depends().at(x)?.clone()
                }
                Some(ExactRef::Hyper(h)) if h.scale.same_infinitesimal(scale) => {
                    infinite = true;
                    Poly::from_coeffs(h.value.rational()?.as_reciprocal_powers()?)
                }
                _ => return None,
            }
        };
        raw.push(Some(p));
    }
    if !infinite {
        return None;
    }
    Hypernatural::from_branches(Depends::from_branches(ty, l, raw)?)
}

/// True for a value of one of the types this module governs.
pub fn is_exact_value<V: TowerValue>(v: &V) -> bool {
    v.exact().is_some()
}

/// A numeric operand seen through the exact lattice.
enum Num {
    Rat(Rational),
    Alg(Algebraic),
    Real(ExactReal),
    Hyper(Hyperreal, Arc<Scale>),
    Closed(Closed, Arc<Scale>),
    Germ(Germ, Arc<Scale>),
    Nat(Hypernatural, Arc<Scale>),
    Ord(Ordinal),
    Multi(Multi),
    Nested(Arc<NestedGerm>),
}

fn classify<V: TowerValue>(v: &V) -> Option<Num> {
    if let Some(r) = v.standard_rational() {
        return Some(Num::Rat(r));
    }
    Some(match v.exact()? {
        ExactRef::Algebraic(a) => Num::Alg(a.clone()),
        ExactRef::Real(x) => Num::Real(x.clone()),
        ExactRef::Hyper(h) => match &h.value {
            HyperForm::Rational(r) => Num::Hyper(r.clone(), h.scale.clone()),
            HyperForm::Puiseux(p) => Num::Closed(Closed::Series(p.clone()), h.scale.clone()),
            HyperForm::Germ(g) => Num::Germ(g.clone(), h.scale.clone()),
            HyperForm::Multi(m) | HyperForm::Integer(m) => Num::Multi(m.clone()),
            HyperForm::Nested(g) => Num::Nested(g.clone()),
        },
        ExactRef::Natural(n) => Num::Nat(n.value.clone(), n.scale.clone()),
        ExactRef::Ordinal(o) => Num::Ord(o.clone()),
        ExactRef::Depends(_) | ExactRef::Converging(_) => return None,
    })
}

fn scale_of(a: &Num, b: &Num) -> Option<Arc<Scale>> {
    let s = |n: &Num| match n {
        Num::Hyper(_, s) | Num::Closed(_, s) | Num::Germ(_, s) | Num::Nat(_, s) => Some(s.clone()),
        Num::Multi(m) => m.top().cloned(),
        Num::Nested(g) => Some(g.scale.clone()),
        _ => None,
    };
    s(a).or_else(|| s(b))
}

/// Every infinitesimal an operand involves, each once.
fn scales_of(n: &Num) -> Vec<Arc<Scale>> {
    match n {
        Num::Hyper(_, s) | Num::Closed(_, s) | Num::Germ(_, s) | Num::Nat(_, s) => vec![s.clone()],
        Num::Multi(m) => m.scales(),
        Num::Nested(g) => g.scales(),
        Num::Rat(_) | Num::Alg(_) | Num::Real(_) | Num::Ord(_) => Vec::new(),
    }
}

/// Every infinitesimal two operands involve, each once and every two ordered; the refusal naming the
/// first two the program does not order.
fn meeting(a: &Num, b: &Num) -> Result<Vec<Arc<Scale>>, String> {
    let mut all: Vec<Arc<Scale>> = Vec::new();
    for s in scales_of(a).into_iter().chain(scales_of(b)) {
        if !all.iter().any(|t| t.same_infinitesimal(&s)) {
            all.push(s);
        }
    }
    for (i, x) in all.iter().enumerate() {
        if let Some(y) = all[i + 1..].iter().find(|y| x.order(y).is_none()) {
            return Err(x.unordered(y));
        }
    }
    Ok(all)
}

fn same_scale(a: &Num, b: &Num) -> Result<(), String> {
    match (scale_of(a, a), scale_of(b, b)) {
        (Some(x), Some(y)) if !x.same_infinitesimal(&y) => Err(x.unordered(&y)),
        _ => Ok(()),
    }
}

fn to_alg(n: &Num) -> Option<Algebraic> {
    match n {
        Num::Rat(r) => Some(Algebraic::from_rational(r.clone())),
        Num::Alg(a) => Some(a.clone()),
        _ => None,
    }
}

fn to_real(n: &Num) -> Option<ExactReal> {
    match n {
        Num::Rat(r) => Some(ExactReal::from_rational(r.clone())),
        Num::Alg(a) => Some(ExactReal::from_algebraic(a.clone())),
        Num::Real(x) => Some(x.clone()),
        _ => None,
    }
}

/// A standard, algebraic or infinite-integer operand as hyperreal branches.
fn to_hyper_branches(n: &Num, ty: &ResidueType) -> Option<Depends<Hyperreal>> {
    match n {
        Num::Rat(r) => Some(Depends::constant(Hyperreal::from_rational(r.clone()), ty)),
        Num::Alg(a) => Some(Depends::constant(Hyperreal::from_algebraic(a.clone()), ty)),
        Num::Hyper(h, _) => Some(Depends::constant(h.clone(), ty)),
        Num::Nat(n, _) => Some(n.to_hyperreal()),
        _ => None,
    }
}

/// A standard integer or an infinite integer, as an infinite integer.
fn to_natural(n: &Num, ty: &ResidueType) -> Option<Hypernatural> {
    match n {
        Num::Rat(r) if r.is_integer() => Some(Hypernatural::from_integer(
            r.to_bigint().expect("an integer"),
            ty,
        )),
        Num::Nat(n, _) => Some(n.clone()),
        _ => None,
    }
}

/// The arithmetic operators the exact types take.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Op {
    Add,
    Sub,
    Mul,
    /// The polymorphic `/`: field division for the exact types, floor division of two integers.
    Div,
    /// `/` in an exact context (`ExactDivide`): field division on every branch, integers included.
    ExactDiv,
    FloorDiv,
    Mod,
    Pow,
}

impl Op {
    fn word(self) -> &'static str {
        match self {
            Op::Add => "add",
            Op::Sub => "subtract",
            Op::Mul => "multiply",
            Op::Div | Op::ExactDiv => "divide",
            Op::FloorDiv => "floor-divide",
            Op::Mod => "take the remainder of",
            Op::Pow => "raise",
        }
    }
}

/// Apply `op` when either operand is an exact type; `None` when neither is (the tower handles it),
/// and for `+` with a `Text` operand, which joins the other value as it prints by the value model's
/// own rule for every value. `recurse` is the value model's full arithmetic, used to lift an
/// operation over residue branches and through provisional values.
pub fn arith<V: TowerValue>(
    op: Op,
    left: &V,
    right: &V,
    recurse: &dyn Fn(Op, V, V) -> Result<V, String>,
) -> Option<Result<V, String>> {
    if !is_exact_value(left) && !is_exact_value(right) {
        return None;
    }
    if matches!(op, Op::Add) && (left.text().is_some() || right.text().is_some()) {
        return None;
    }
    if let Some(r) = lift(left, right, |a, b| recurse(op, a, b)) {
        return Some(r);
    }
    let (Some(a), Some(b)) = (classify(left), classify(right)) else {
        return Some(Err(format!(
            "cannot {} {} and {}",
            op.word(),
            left.type_name(),
            right.type_name()
        )));
    };
    if let Some(r) = several_arith(op, &a, &b, left, right, recurse) {
        return Some(r);
    }
    if let Some(r) = germ_arith(op, &a, &b, left, right, recurse) {
        return Some(r);
    }
    Some(arith_num(op, a, b, left, right))
}

// ── several infinitesimals ────────────────────────────────────────────────────────────────────

/// Whether two operands together involve more than one infinitesimal, or a value of several; the
/// refusal when they involve two the program does not order.
fn several(a: &Num, b: &Num) -> Result<bool, String> {
    let all = meeting(a, b)?;
    let held = |n: &Num| matches!(n, Num::Multi(_) | Num::Nested(_));
    Ok(all.len() > 1 || held(a) || held(b))
}

/// Whether an operand of several infinitesimals calls for germs: a germ, a computable transcendental,
/// or a germ of several.
fn several_germs(a: &Num, b: &Num) -> bool {
    let lazy = |n: &Num| matches!(n, Num::Germ(..) | Num::Real(_) | Num::Nested(_));
    lazy(a) || lazy(b)
}

/// The smallest infinitesimal two operands involve.
fn smallest_scale(a: &Num, b: &Num) -> Result<Arc<Scale>, String> {
    let all = meeting(a, b)?;
    let mut smallest = all.first().cloned().expect("several infinitesimals are involved");
    for s in &all[1..] {
        if s.order(&smallest) == Some(Ordering::Less) {
            smallest = s.clone();
        }
    }
    Ok(smallest)
}

/// An operand as a germ of several infinitesimals at `scale`, its smallest or one smaller.
fn nested_operand<V: TowerValue>(n: &Num, v: &V, scale: &Arc<Scale>) -> Result<Arc<NestedGerm>, String> {
    let constant = || -> Number { as_number(v) };
    Ok(Arc::new(match n {
        Num::Nested(g) if g.scale.same_infinitesimal(scale) => (**g).clone(),
        Num::Germ(g, s) if s.same_infinitesimal(scale) => NestedGerm::germ(g, scale),
        Num::Rat(_) | Num::Alg(_) | Num::Real(_) | Num::Germ(..) | Num::Nested(_) => NestedGerm::constant(constant(), scale),
        Num::Hyper(..) | Num::Closed(..) | Num::Multi(_) | Num::Nat(..) => match several_operand(n) {
            Some(m) => NestedGerm::exact(&m, scale),
            None => return Err(format!("cannot read {} as a germ of {}", v.display_string(), scale.name)),
        },
        Num::Ord(_) => return Err(format!("an ordinal is no germ of {}", scale.name)),
    }))
}

/// A number as a germ of several infinitesimals at `scale`, its smallest or one smaller.
pub(crate) fn number_germ(n: &Number, scale: &Arc<Scale>) -> Result<Arc<NestedGerm>, String> {
    match classify(n) {
        Some(num) => nested_operand(&num, n, scale),
        None => Err(format!("a {} is not a number", n.type_name())),
    }
}

/// Every infinitesimal a number involves.
pub(crate) fn number_scales(n: &Number) -> Vec<Arc<Scale>> {
    classify(n).map(|num| scales_of(&num)).unwrap_or_default()
}

/// A value of a value model as base's own number, by its own exact form.
pub(crate) fn as_number<V: TowerValue>(v: &V) -> Number {
    if let Some(r) = v.standard_rational() {
        return Number::from_rational(r);
    }
    match v.exact() {
        Some(ExactRef::Algebraic(a)) => Number::algebraic(a.clone()),
        Some(ExactRef::Real(x)) => Number::exact_real(x.clone()),
        Some(ExactRef::Hyper(h)) => Number::hyper(h.clone()),
        Some(ExactRef::Natural(n)) => Number::natural(n.clone()),
        Some(ExactRef::Ordinal(o)) => Number::ordinal(o.clone()),
        Some(ExactRef::Depends(d)) => Number::depends(DependsValue {
            value: d.value.map(|b| Branch(as_number(&b.0))),
            scale: d.scale.clone(),
        }),
        Some(ExactRef::Converging(c)) => Number::converging(c.with_value(as_number(c.value()))),
        None => Number::nothing(),
    }
}

/// Base's own number as a value of a value model.
pub(crate) fn from_number<V: TowerValue>(n: Number) -> V {
    match n {
        Number::Int(b) => V::from_bigint(b),
        Number::Rat(r) => V::from_rational(r),
        Number::Bool(b) => V::boolean(b),
        Number::Nothing => V::nothing(),
        Number::Alg(a) => V::algebraic(a),
        Number::Real(x) => V::exact_real(x),
        Number::Hyper(h) => V::hyper(h),
        Number::Nat(m) => V::natural(m),
        Number::Ord(o) => V::ordinal(o),
        Number::Dep(d) => V::depends(DependsValue {
            value: d.value.map(|b| Branch(from_number(b.0.clone()))),
            scale: d.scale.clone(),
        }),
        Number::Conv(c) => V::converging(c.with_value(from_number(c.value().clone()))),
    }
}

/// A germ of several infinitesimals as a value of a value model.
pub(crate) fn from_nested<V: TowerValue>(g: NestedGerm) -> V {
    let scale = g.scale.clone();
    V::hyper(HyperValue {
        value: HyperForm::Nested(Arc::new(g)),
        scale,
    })
}

fn nested_arith<V: TowerValue>(op: Op, a: &Num, b: &Num, left: &V, right: &V) -> Result<V, String> {
    let scale = smallest_scale(a, b)?;
    let x = nested_operand(a, left, &scale)?;
    let out = match op {
        Op::Pow => match (integer_exponent(right), fractional_exponent(right)) {
            (Some(k), _) => NestedGerm::pow(&x, k)?,
            (None, Some((p, q))) => NestedGerm::pow(&Arc::new(NestedGerm::root(&x, q)?), p)?,
            (None, None) => {
                return Err("a value of the infinitesimal is raised only to an integer or a rational power".to_string())
            }
        },
        Op::FloorDiv | Op::Mod => {
            return Err(
                "the integer part of a quotient of these values is not an exact value; divide exactly".to_string(),
            )
        }
        _ => {
            let y = nested_operand(b, right, &scale)?;
            match op {
                Op::Add => NestedGerm::add(&x, &y),
                Op::Sub if NestedGerm::same_recipe(&x, &y) => return Ok(V::from_bigint(BigInt::from_i64(0))),
                Op::Sub => NestedGerm::sub(&x, &y),
                Op::Mul => NestedGerm::mul(&x, &y),
                Op::Div | Op::ExactDiv => NestedGerm::mul(&x, &Arc::new(NestedGerm::recip(&y)?)),
                _ => unreachable!("handled above"),
            }
        }
    };
    Ok(from_nested(out))
}

/// An operand of a value of several infinitesimals as a value of their field; `None` for a germ, a
/// computable transcendental, an infinite integer that depends on the residue and an ordinal.
fn several_operand(n: &Num) -> Option<Multi> {
    Some(match n {
        Num::Rat(r) => Multi::Standard(Algebraic::from_rational(r.clone())),
        Num::Alg(a) => Multi::Standard(a.clone()),
        Num::Hyper(h, s) => Multi::of_closed(Closed::from_hyperreal(h.clone()), s),
        Num::Closed(c, s) => Multi::of_closed(c.clone(), s),
        Num::Nat(n, s) => Multi::of_closed(Closed::from_hyperreal(n.to_hyperreal().single()?.clone()), s),
        Num::Multi(m) => m.clone(),
        Num::Real(_) | Num::Germ(..) | Num::Ord(_) | Num::Nested(_) => return None,
    })
}

/// Both operands as exact values of their infinitesimals, or the refusal of a value that is none.
fn several_operands(a: &Num, b: &Num, left: &str, right: &str, word: &str) -> Result<(Multi, Multi), String> {
    let (Some(x), Some(y)) = (several_operand(a), several_operand(b)) else {
        return Err(format!(
            "cannot {word} {left} and {right}: only exact values of several infinitesimals combine"
        ));
    };
    Ok((x, y))
}

fn several_arith<V: TowerValue>(
    op: Op,
    a: &Num,
    b: &Num,
    left: &V,
    right: &V,
    recurse: &dyn Fn(Op, V, V) -> Result<V, String>,
) -> Option<Result<V, String>> {
    match several(a, b) {
        Ok(false) => return None,
        Ok(true) => {}
        Err(e) => return Some(Err(e)),
    }
    if let Some(l) = lifted_natural(a) {
        return Some(recurse(op, l, right.clone()));
    }
    if let Some(r) = lifted_natural(b) {
        return Some(recurse(op, left.clone(), r));
    }
    if several_germs(a, b) {
        return Some(nested_arith(op, a, b, left, right));
    }
    let shown = |v: &V| if is_exact_value(v) { v.display_string() } else { v.type_name() };
    let (x, y) = match several_operands(a, b, &shown(left), &shown(right), op.word()) {
        Ok(pair) => pair,
        Err(e) => return Some(Err(e)),
    };
    let out = match op {
        Op::Add => Ok(x.add(&y)),
        Op::Sub => Ok(x.sub(&y)),
        Op::Mul => Ok(x.mul(&y)),
        Op::Div | Op::ExactDiv => y.recip().map(|r| x.mul(&r)).ok_or_else(|| "Division by zero".to_string()),
        Op::Pow => match (integer_exponent(right), fractional_exponent(right)) {
            (Some(k), _) => x.pow(k).map_err(|e| e.describe()),
            (None, Some((p, q))) => x.root(q).and_then(|r| r.pow(p).map_err(|e| e.describe())),
            (None, None) => Err("a hyperreal is raised only to an integer or a rational power".to_string()),
        },
        Op::FloorDiv | Op::Mod if is_integer_value(left) && is_integer_value(right) => {
            let quotient = match y.recip() {
                Some(r) => x.mul(&r),
                None => return Some(Err("Division by zero".to_string())),
            };
            let floor = match floor_number(&from_multi(quotient)) {
                Ok(n) => from_number::<V>(n),
                Err(e) => return Some(Err(e)),
            };
            return Some(match op {
                Op::FloorDiv => Ok(floor),
                _ => recurse(Op::Mul, right.clone(), floor).and_then(|m| recurse(Op::Sub, left.clone(), m)),
            });
        }
        Op::FloorDiv | Op::Mod => Err(
            "the integer part of a hyperreal quotient is not an exact hyperreal; divide exactly".to_string(),
        ),
    };
    Some(out.map(from_multi))
}

fn several_relation<V: TowerValue>(
    rel: Rel,
    a: &Num,
    b: &Num,
    left: &V,
    right: &V,
    recurse: &dyn Fn(Rel, V, V) -> Result<V, String>,
) -> Option<Result<V, String>> {
    match several(a, b) {
        Ok(false) => return None,
        Ok(true) => {}
        Err(e) => return Some(Err(e)),
    }
    if let Some(l) = lifted_natural(a) {
        return Some(recurse(rel, l, right.clone()));
    }
    if let Some(r) = lifted_natural(b) {
        return Some(recurse(rel, left.clone(), r));
    }
    if several_germs(a, b) {
        let difference = smallest_scale(a, b).and_then(|scale| {
            let x = nested_operand(a, left, &scale)?;
            let y = nested_operand(b, right, &scale)?;
            if NestedGerm::same_recipe(&x, &y) {
                return Ok(0);
            }
            NestedGerm::sub(&x, &y).sign()
        });
        return Some(difference.map(|s| V::boolean(rel.holds(s.cmp(&0)))));
    }
    let shown = |v: &V| if is_exact_value(v) { v.display_string() } else { v.type_name() };
    let (x, y) = match several_operands(a, b, &shown(left), &shown(right), "compare") {
        Ok(pair) => pair,
        Err(e) => return Some(Err(e)),
    };
    Some(Ok(V::boolean(rel.holds(x.sub(&y).signum().cmp(&0)))))
}

/// Whether an operation calls for germs: a germ on either side, or a computable transcendental
/// meeting a value of the infinitesimal.
fn calls_for_germs(a: &Num, b: &Num) -> bool {
    let germ = |n: &Num| matches!(n, Num::Germ(..));
    let real = |n: &Num| matches!(n, Num::Real(_));
    germ(a) || germ(b) || (scale_of(a, b).is_some() && (real(a) || real(b)))
}

/// An operand as a germ: a standard number as a constant, a rational function or a value of the
/// real closure by its series, an infinite integer that does not depend on the residue by its
/// series; `None` otherwise.
fn to_germ(n: &Num) -> Option<Germ> {
    Some(match n {
        Num::Rat(r) => Germ::from_hyperreal(&Hyperreal::from_rational(r.clone())),
        Num::Alg(a) => Germ::from_hyperreal(&Hyperreal::from_algebraic(a.clone())),
        Num::Real(x) => Germ::constant(x),
        Num::Hyper(h, _) => Germ::from_hyperreal(h),
        Num::Closed(c, _) => closed_germ(c),
        Num::Germ(g, _) => g.clone(),
        Num::Nat(n, _) => Germ::from_hyperreal(n.to_hyperreal().single()?),
        Num::Ord(_) | Num::Multi(_) | Num::Nested(_) => return None,
    })
}

/// A value of the real closure by its series.
fn closed_germ(c: &Closed) -> Germ {
    match c {
        Closed::Field(h) => Germ::from_hyperreal(h),
        Closed::Series(p) => Germ::from_puiseux(p),
    }
}

/// A number as a germ: a standard number as a constant, a hyperreal by its series or as the germ
/// it is, an infinite integer that does not depend on the residue by its series; `None` otherwise.
pub fn germ_of<V: TowerValue>(v: &V) -> Option<Germ> {
    to_germ(&classify(v)?)
}

/// An infinite integer that depends on the residue as the dependence its classes make — on each, the
/// infinite integer it is there, on that class's own scale, whose facts make it one — so an operation
/// with a germ or a value of another infinitesimal lifts over its classes and an integer stays one. The
/// dependence is left as its classes make it: in its canonical form it is the infinite integer again,
/// and the operation's answer is made canonical as it is joined ([`map_depends`]).
fn lifted_natural<V: TowerValue>(n: &Num) -> Option<V> {
    let Num::Nat(nat, scale) = n else {
        return None;
    };
    let classes = nat.depends();
    if classes.single().is_some() {
        return None;
    }
    let (ty, m) = (classes.residue_type().clone(), classes.modulus());
    let raw = (0..m)
        .map(|h| {
            let p = classes.at(h)?;
            let class = Arc::new(scale.with_residues(ty.and(&ResidueType::congruent(h, m)).ok()?));
            let on_class = Hypernatural::from_polynomial(p.clone(), &class.residues)?;
            Some(Branch(from_natural(on_class, &class)))
        })
        .collect();
    Some(V::depends(DependsValue {
        value: Depends::from_branches(ty, m, raw)?,
        scale: scale.clone(),
    }))
}

fn germ_arith<V: TowerValue>(
    op: Op,
    a: &Num,
    b: &Num,
    left: &V,
    right: &V,
    recurse: &dyn Fn(Op, V, V) -> Result<V, String>,
) -> Option<Result<V, String>> {
    if !calls_for_germs(a, b) {
        return None;
    }
    if let Err(e) = same_scale(a, b) {
        return Some(Err(e));
    }
    if let Some(l) = lifted_natural(a) {
        return Some(recurse(op, l, right.clone()));
    }
    if let Some(r) = lifted_natural(b) {
        return Some(recurse(op, left.clone(), r));
    }
    if let Some(r) = germ_identity(op, a, b, left, right) {
        return Some(Ok(r));
    }
    let scale = scale_of(a, b).expect("a germ or an infinitesimal is on one side");
    let (Some(x), Some(y)) = (to_germ(a), to_germ(b)) else {
        return Some(Err(format!(
            "cannot {} {} and {}",
            op.word(),
            left.type_name(),
            right.type_name()
        )));
    };
    let text = |e: crate::germ::GermError| e.to_string();
    let same = || x.is_transmissible() && y.is_transmissible() && x.to_bytes() == y.to_bytes();
    let result = match op {
        Op::Add => Ok(x.add(&y)),
        Op::Sub if same() => Ok(Germ::from_i64(0)),
        Op::Sub => Ok(x.sub(&y)),
        Op::Mul => Ok(x.mul(&y)),
        Op::Div | Op::ExactDiv => x.div(&y).map_err(text),
        Op::Pow => match (integer_exponent(right), fractional_exponent(right)) {
            (Some(k), _) => germ_power(&x, k).map_err(text),
            (None, Some((p, q))) => x.root(q).and_then(|r| germ_power(&r, p)).map_err(text),
            (None, None) => {
                Err("a value of the infinitesimal is raised only to an integer or a rational power".to_string())
            }
        },
        Op::FloorDiv | Op::Mod => Err(
            "the integer part of a quotient of these values is not an exact value; divide exactly"
                .to_string(),
        ),
    };
    Some(result.map(|g| from_germ(g, &scale)))
}

/// The value an operation with an exact `0` or `1` leaves as it was: `x + 0`, `x − 0`, `x·1`, `x/1`,
/// `x·0`. A germ is known by the recipe that built it, so the identities keep one value one recipe.
fn germ_identity<V: TowerValue>(op: Op, a: &Num, b: &Num, left: &V, right: &V) -> Option<V> {
    let is = |n: &Num, k: i64| matches!(n, Num::Rat(r) if *r == Rational::from_i64(k));
    match op {
        Op::Add if is(a, 0) => Some(right.clone()),
        Op::Add | Op::Sub if is(b, 0) => Some(left.clone()),
        Op::Mul if is(a, 1) => Some(right.clone()),
        Op::Mul | Op::Div | Op::ExactDiv if is(b, 1) => Some(left.clone()),
        Op::Mul if is(a, 0) || is(b, 0) => Some(V::from_bigint(BigInt::from_i64(0))),
        _ => None,
    }
}

fn germ_power(x: &Germ, k: i32) -> Result<Germ, crate::germ::GermError> {
    let mut base = if k < 0 { x.recip()? } else { x.clone() };
    let mut acc = Germ::from_i64(1);
    let mut e = k.unsigned_abs();
    while e > 0 {
        if e & 1 == 1 {
            acc = acc.mul(&base);
        }
        e >>= 1;
        if e > 0 {
            base = base.mul(&base);
        }
    }
    Ok(acc)
}

fn germ_relation<V: TowerValue>(
    rel: Rel,
    a: &Num,
    b: &Num,
    left: &V,
    right: &V,
    recurse: &dyn Fn(Rel, V, V) -> Result<V, String>,
) -> Option<Result<V, String>> {
    if !calls_for_germs(a, b) {
        return None;
    }
    if let Err(e) = same_scale(a, b) {
        return Some(Err(e));
    }
    if let Some(l) = lifted_natural(a) {
        return Some(recurse(rel, l, right.clone()));
    }
    if let Some(r) = lifted_natural(b) {
        return Some(recurse(rel, left.clone(), r));
    }
    let (Some(x), Some(y)) = (to_germ(a), to_germ(b)) else {
        return Some(Err(format!(
            "cannot compare {} and {}",
            left.type_name(),
            right.type_name()
        )));
    };
    if x.is_transmissible() && y.is_transmissible() && x.to_bytes() == y.to_bytes() {
        return Some(Ok(V::boolean(rel.holds(Ordering::Equal))));
    }
    Some(match x.sub(&y).signum() {
        Ok(s) => Ok(V::boolean(rel.holds(s.cmp(&0)))),
        Err(e) => Err(e.to_string()),
    })
}

/// Lift a binary operation over residue branches or provisional values; `None` when neither
/// operand is one.
fn lift<V: TowerValue>(
    left: &V,
    right: &V,
    f: impl Fn(V, V) -> Result<V, String>,
) -> Option<Result<V, String>> {
    match (left.exact(), right.exact()) {
        (Some(ExactRef::Converging(c)), _) => {
            let inner = f(c.value().clone(), right.clone());
            Some(inner.map(|v| carry_evidence(c, v)))
        }
        (_, Some(ExactRef::Converging(c))) => {
            let inner = f(left.clone(), c.value().clone());
            Some(inner.map(|v| carry_evidence(c, v)))
        }
        _ if residue_generators_differ(left, right) => {
            let (a, b) = (residue_generator(left)?, residue_generator(right)?);
            if a.order(b).is_none() {
                return Some(Err(a.unordered(b)));
            }
            Some(map_depends(&residue_branches(left)?, |x| f(x, right.clone())))
        }
        (Some(ExactRef::Depends(a)), Some(ExactRef::Depends(b))) => {
            let err = RefCell::new(None);
            let joined = a
                .value
                .zip_with(&b.value, |x, y| capture(&err, f(x.0.clone(), y.0.clone())));
            Some(match (joined, err.into_inner()) {
                (Err(e), _) => Err(a.scale.refuse(e)),
                (_, Some(e)) => Err(e),
                (Ok(joined), None) => Ok(from_depends(joined, &a.scale)),
            })
        }
        (Some(ExactRef::Depends(a)), _) => Some(map_depends(a, |x| f(x, right.clone()))),
        (_, Some(ExactRef::Depends(b))) => Some(map_depends(b, |y| f(left.clone(), y))),
        _ => None,
    }
}

/// The generator whose residue `v` reads at its top — a residue-dependent value's, or an infinite
/// integer's that depends on the residue — or `None` for any other value.
fn residue_generator<V: TowerValue>(v: &V) -> Option<&Arc<Scale>> {
    match v.exact()? {
        ExactRef::Depends(d) => Some(&d.scale),
        ExactRef::Natural(n) if n.value.depends().single().is_none() => Some(&n.scale),
        _ => None,
    }
}

/// Every generator whose residue `v` reads, coarsest first, its branches' own included, each once.
fn generators_read<V: TowerValue>(v: &V, out: &mut Vec<Arc<Scale>>) {
    let Some(g) = residue_generator(v) else {
        return;
    };
    if !out.iter().any(|o| o.same_infinitesimal(g)) {
        out.push(g.clone());
    }
    if let Some(d) = depends_of(v) {
        for (_, b) in d.value.branches() {
            generators_read(&b.0, out);
        }
    }
}

/// Whether both operands read the residue of a generator and the two are of different
/// infinitesimals. An operation on two such maps over the classes of either, and [`from_depends`]
/// nests the answer in its one form, a dependence on the coarsest — the generator of the largest
/// infinitesimal — whose branches read only finer ones: `(0 when ⌈1/dx⌉ is even, 1 when it is odd)`
/// added to a value that depends on `⌈1/dt⌉` is a dependence on `⌈1/dt⌉` whose branches depend on
/// `⌈1/dx⌉`. The residues of two generators are independent — a program states each one's alone —
/// so every pair of classes is a case.
fn residue_generators_differ<V: TowerValue>(left: &V, right: &V) -> bool {
    matches!((residue_generator(left), residue_generator(right)), (Some(a), Some(b)) if !a.same_infinitesimal(b))
}

/// `v`'s dependence on the residue of its generator, branch by branch: a residue-dependent value's
/// own, and an infinite integer's as the hyperreal it is on each class.
fn residue_branches<V: TowerValue>(v: &V) -> Option<DependsValue<V>> {
    match v.exact()? {
        ExactRef::Depends(d) => Some(d.clone()),
        ExactRef::Natural(n) => Some(DependsValue {
            value: n.value.to_hyperreal().map(|h| Branch(from_hyper(h.clone(), &n.scale))),
            scale: n.scale.clone(),
        }),
        _ => None,
    }
}

/// A branch's value, or the first error any branch raised (kept in `err`; the branch itself is
/// then a placeholder the caller discards).
fn capture<V: TowerValue>(err: &RefCell<Option<String>>, r: Result<V, String>) -> Branch<V> {
    match r {
        Ok(v) => Branch(v),
        Err(e) => {
            err.borrow_mut().get_or_insert(e);
            Branch(V::nothing())
        }
    }
}

/// `f` on every branch of a residue-dependent value, or the first error a branch raises.
pub fn map_depends<V: TowerValue>(
    d: &DependsValue<V>,
    f: impl Fn(V) -> Result<V, String>,
) -> Result<V, String> {
    let err = RefCell::new(None);
    let mapped = d.value.map(|x| capture(&err, f(x.0.clone())));
    match err.into_inner() {
        Some(e) => Err(e),
        None => Ok(from_depends(mapped, &d.scale)),
    }
}

/// `v` carrying the evidence a provisional or settled answer `c` carries. An answer never holds
/// another: when `v` carries evidence of its own, the two join into one ([`Converging::joined`]).
pub fn carry_evidence<V: TowerValue, U>(c: &Converging<U>, v: V) -> V {
    if let Some(ExactRef::Converging(own)) = v.exact() {
        return V::converging(c.joined(own, own.value().clone()));
    }
    match c.certificate() {
        Some(cert) => V::converging(Converging::settled(v, cert)),
        None => V::converging(Converging::provisional(v, c.steps(), c.revisions())),
    }
}

fn arith_num<V: TowerValue>(op: Op, a: Num, b: Num, left: &V, right: &V) -> Result<V, String> {
    same_scale(&a, &b)?;
    let refuse = || {
        Err(format!(
            "cannot {} {} and {}",
            op.word(),
            left.type_name(),
            right.type_name()
        ))
    };
    // Ordinals meet only ordinals and naturals.
    if matches!(a, Num::Ord(_)) || matches!(b, Num::Ord(_)) {
        return ordinal_arith(op, &a, &b).unwrap_or_else(refuse);
    }
    // An infinite integer with a standard integer keeps integer meaning.
    let integral = |n: &Num, v: &V| matches!(n, Num::Nat(..)) || v.integer().is_some();
    if (matches!(a, Num::Nat(..)) || matches!(b, Num::Nat(..)))
        && integral(&a, left)
        && integral(&b, right)
        && !matches!(op, Op::Div | Op::ExactDiv)
    {
        let scale = scale_of(&a, &b).expect("an infinite integer has a scale");
        let x = to_natural(&a, &scale.residues).expect("integral");
        let y = to_natural(&b, &scale.residues).expect("integral");
        return natural_arith(op, x, y, right, &scale);
    }
    if let Some(r) = closed_arith(op, &a, &b, right) {
        return r;
    }
    // The infinitesimal generates the hyperreals over the algebraic numbers.
    if let Some(scale) = scale_of(&a, &b) {
        let x = to_hyper_branches(&a, &scale.residues).expect("hyperreal operand");
        let y = to_hyper_branches(&b, &scale.residues).expect("hyperreal operand");
        let err = RefCell::new(None);
        let out = x.zip_with(&y, |p, q| {
            capture(&err, hyper_op(op, p, q, right, &scale).map(|v| from_hyper(v, &scale)))
        });
        return match (out, err.into_inner()) {
            (Err(e), _) => Err(scale.refuse(e)),
            (_, Some(e)) => Err(e),
            (Ok(out), None) => Ok(from_depends(out, &scale)),
        };
    }
    // Computable reals above the algebraic numbers.
    if matches!(a, Num::Real(_)) || matches!(b, Num::Real(_)) {
        let (x, y) = (to_real(&a).expect("real operand"), to_real(&b).expect("real operand"));
        return real_op(op, &x, &y, right).map(from_exact_real);
    }
    match (to_alg(&a), to_alg(&b)) {
        (Some(x), Some(y)) => alg_op(op, &x, &y, right).map(from_algebraic),
        _ => refuse(),
    }
}

fn integer_exponent<V: TowerValue>(v: &V) -> Option<i32> {
    v.integer()
        .and_then(|b| b.to_i64())
        .and_then(|e| i32::try_from(e).ok())
}

/// An exponent `p/q` held exactly with `q > 1`: a root to take and a power to raise it to.
fn fractional_exponent<V: TowerValue>(v: &V) -> Option<(i32, u32)> {
    let r = v.exact_rational().filter(|r| !r.is_integer())?;
    let p = i32::try_from(r.numerator().to_i64()?).ok()?;
    let q = u32::try_from(r.denominator().to_i64()?).ok()?;
    Some((p, q))
}

/// An operand of the real closure, on each residue class of `⌈1/dt⌉` an infinite integer depends
/// on; `None` for a germ, a computable real or an ordinal.
fn to_closed_branches(n: &Num, ty: &ResidueType) -> Option<Depends<Closed>> {
    match n {
        Num::Rat(r) => Some(Depends::constant(Closed::Field(Hyperreal::from_rational(r.clone())), ty)),
        Num::Alg(a) => Some(Depends::constant(Closed::Field(Hyperreal::from_algebraic(a.clone())), ty)),
        Num::Hyper(h, _) => Some(Depends::constant(Closed::Field(h.clone()), ty)),
        Num::Closed(c, _) => Some(Depends::constant(c.clone(), ty)),
        Num::Nat(n, _) => Some(n.to_hyperreal().map(|h| Closed::Field(h.clone()))),
        Num::Real(_) | Num::Germ(..) | Num::Ord(_) | Num::Multi(_) | Num::Nested(_) => None,
    }
}

/// An operation in the real closure of the hyperreals: when a root of a hyperreal is an operand, or
/// a hyperreal or an infinite integer is raised to a fractional power.
fn closed_arith<V: TowerValue>(op: Op, a: &Num, b: &Num, right: &V) -> Option<Result<V, String>> {
    let rooted = matches!(a, Num::Closed(..)) || matches!(b, Num::Closed(..));
    let fractional = matches!(op, Op::Pow)
        && matches!(a, Num::Hyper(..) | Num::Nat(..))
        && fractional_exponent(right).is_some();
    if !rooted && !fractional {
        return None;
    }
    let scale = scale_of(a, b)?;
    let x = to_closed_branches(a, &scale.residues)?;
    let y = to_closed_branches(b, &scale.residues)?;
    let err = RefCell::new(None);
    let out = x.zip_with(&y, |p, q| capture(&err, closed_op(op, p, q, right, &scale).map(|c| from_closed(c, &scale))));
    Some(match (out, err.into_inner()) {
        (Err(e), _) => Err(scale.refuse(e)),
        (_, Some(e)) => Err(e),
        (Ok(out), None) => Ok(from_depends(out, &scale)),
    })
}

fn closed_op<V: TowerValue>(op: Op, x: &Closed, y: &Closed, right: &V, scale: &Scale) -> Result<Closed, String> {
    match op {
        Op::Add => Ok(x.add(y)),
        Op::Sub => Ok(x.sub(y)),
        Op::Mul => Ok(x.mul(y)),
        Op::Div | Op::ExactDiv => x.div(y).ok_or_else(|| "Division by zero".to_string()),
        Op::Pow => match (integer_exponent(right), fractional_exponent(right)) {
            (Some(k), _) => x.pow(k).map_err(|e| e.describe(&scale.name)),
            (None, Some((p, q))) => x.root(q)?.pow(p).map_err(|e| e.describe(&scale.name)),
            (None, None) => Err("a hyperreal is raised only to an integer or a rational power".to_string()),
        },
        Op::FloorDiv | Op::Mod => Err(
            "the integer part of a hyperreal quotient is not an exact hyperreal; divide exactly".to_string(),
        ),
    }
}

fn alg_op<V: TowerValue>(op: Op, x: &Algebraic, y: &Algebraic, right: &V) -> Result<Algebraic, String> {
    match op {
        Op::Add => Ok(x.add(y)),
        Op::Sub => Ok(x.sub(y)),
        Op::Mul => Ok(x.mul(y)),
        Op::Div | Op::ExactDiv => x.div(y).ok_or_else(|| "Division by zero".to_string()),
        Op::FloorDiv => {
            let q = x.div(y).ok_or_else(|| "Division by zero".to_string())?;
            Ok(Algebraic::from_rational(Rational::from_bigint(q.floor())))
        }
        Op::Mod => {
            let q = x.div(y).ok_or_else(|| "Division by zero".to_string())?;
            Ok(x.sub(&y.mul(&Algebraic::from_rational(Rational::from_bigint(q.floor())))))
        }
        Op::Pow => match (integer_exponent(right), fractional_exponent(right)) {
            (Some(k), _) => x
                .pow(k)
                .ok_or_else(|| "zero cannot be raised to a negative power".to_string()),
            (None, Some((p, q))) => x
                .nth_root(q)
                .ok_or_else(|| negative_root(q))?
                .pow(p)
                .ok_or_else(|| "zero cannot be raised to a negative power".to_string()),
            (None, None) => Err("an algebraic number is raised only to an integer or a rational power".to_string()),
        },
    }
}

fn real_op<V: TowerValue>(op: Op, x: &ExactReal, y: &ExactReal, right: &V) -> Result<ExactReal, String> {
    match op {
        Op::Add => Ok(x.add(y)),
        Op::Sub => Ok(x.sub(y)),
        Op::Mul => Ok(x.mul(y)),
        Op::Div | Op::ExactDiv => x.div(y).map_err(|e| e.to_string()),
        Op::FloorDiv | Op::Mod => {
            let q = x.div(y).map_err(|e| e.to_string())?;
            let f = ExactReal::from_rational(Rational::from_bigint(
                q.floor(DEFAULT_BUDGET).map_err(|e| e.to_string())?,
            ));
            Ok(if op == Op::FloorDiv { f } else { x.sub(&y.mul(&f)) })
        }
        Op::Pow => match (integer_exponent(right), fractional_exponent(right)) {
            (Some(k), _) => x
                .pow(k)
                .ok_or_else(|| "zero cannot be raised to a negative power".to_string()),
            (None, Some((p, q))) => real_fractional_power(x, p, q),
            (None, None) => Err("a computable real is raised only to an integer or a rational power".to_string()),
        },
    }
}

/// `x^(p/q)` for `q > 1`: the power of its real `q`-th root ([`ExactReal::nth_root`]), refused for an
/// even root of a negative `x` and for zero to a negative power.
fn real_fractional_power(x: &ExactReal, p: i32, q: u32) -> Result<ExactReal, String> {
    let sign = x.compare(&ExactReal::from_i64(0), DEFAULT_BUDGET).map_err(|e| e.to_string())?;
    match sign {
        Ordering::Equal if p > 0 => return Ok(ExactReal::from_i64(0)),
        Ordering::Equal => return Err("zero cannot be raised to a negative power".to_string()),
        Ordering::Less if q % 2 == 0 => return Err(negative_root(q)),
        _ => {}
    }
    let root = x.nth_root(q).map_err(|e| e.to_string())?;
    root.pow(p).ok_or_else(|| "zero cannot be raised to a negative power".to_string())
}

fn hyper_op<V: TowerValue>(
    op: Op,
    x: &Hyperreal,
    y: &Hyperreal,
    right: &V,
    scale: &Scale,
) -> Result<Hyperreal, String> {
    match op {
        Op::Add => Ok(x.add(y)),
        Op::Sub => Ok(x.sub(y)),
        Op::Mul => Ok(x.mul(y)),
        Op::Div | Op::ExactDiv => x.div(y).ok_or_else(|| "Division by zero".to_string()),
        Op::Pow => match integer_exponent(right) {
            Some(k) => x.pow(k).map_err(|e| e.describe(&scale.name)),
            None => Err("a hyperreal is raised only to an integer power".to_string()),
        },
        Op::FloorDiv | Op::Mod => Err(
            "the integer part of a hyperreal quotient is not an exact hyperreal; divide exactly"
                .to_string(),
        ),
    }
}

fn natural_arith<V: TowerValue>(
    op: Op,
    x: Hypernatural,
    y: Hypernatural,
    right: &V,
    scale: &Arc<Scale>,
) -> Result<V, String> {
    let standard_divisor = || -> Result<BigInt, String> {
        right
            .integer()
            .ok_or_else(|| "an infinite integer is divided only by a standard integer".to_string())
    };
    let refuse = |e| scale.refuse(e);
    match op {
        Op::Add => Ok(from_natural(x.add(&y).map_err(refuse)?, scale)),
        Op::Sub => Ok(from_natural(x.sub(&y).map_err(refuse)?, scale)),
        Op::Mul => Ok(from_natural(x.mul(&y).map_err(refuse)?, scale)),
        Op::FloorDiv => {
            let k = standard_divisor()?;
            if k.is_zero() {
                return Err("Division by zero".to_string());
            }
            let t = Rational::new(BigInt::from_i64(1), k).expect("k ≠ 0");
            Ok(from_natural(x.scaled_floor(&t).map_err(refuse)?, scale))
        }
        Op::Mod => {
            let k = standard_divisor()?;
            if !k.is_positive() {
                return Err(
                    "an infinite integer's remainder is taken by a positive standard integer"
                        .to_string(),
                );
            }
            let residues = x
                .rem(&k)
                .map_err(refuse)?
                .map(|r| Branch(V::from_bigint(r.clone())));
            Ok(from_depends(residues, scale))
        }
        Op::Pow => match right.integer().and_then(|b| b.to_u64()) {
            Some(k) => Ok(from_natural(
                x.pow(k).map_err(|e| e.describe(&scale.name))?,
                scale,
            )),
            None => Err("an infinite integer is raised only to a natural power".to_string()),
        },
        Op::Div | Op::ExactDiv => {
            unreachable!("exact division of infinite integers goes through the hyperreals")
        }
    }
}

fn as_ordinal(n: &Num) -> Option<Ordinal> {
    match n {
        Num::Ord(o) => Some(o.clone()),
        Num::Rat(r) if r.is_integer() && !r.is_negative() => {
            Some(Ordinal::from_natural(r.to_bigint().expect("an integer")))
        }
        _ => None,
    }
}

fn ordinal_arith<V: TowerValue>(op: Op, a: &Num, b: &Num) -> Option<Result<V, String>> {
    let (x, y) = (as_ordinal(a)?, as_ordinal(b)?);
    Some(match op {
        Op::Add => Ok(from_ordinal(x.add(&y))),
        Op::Mul => Ok(from_ordinal(x.mul(&y))),
        Op::Pow => Ok(from_ordinal(x.pow(&y))),
        _ => Err(format!(
            "ordinals add, multiply and exponentiate; they do not {}",
            op.word()
        )),
    })
}

/// The relational operators the exact types answer.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Rel {
    Lt,
    Gt,
    LtEq,
    GtEq,
    Eq,
    NotEq,
}

impl Rel {
    fn holds(self, o: Ordering) -> bool {
        match self {
            Rel::Lt => o == Ordering::Less,
            Rel::Gt => o == Ordering::Greater,
            Rel::LtEq => o != Ordering::Greater,
            Rel::GtEq => o != Ordering::Less,
            Rel::Eq => o == Ordering::Equal,
            Rel::NotEq => o != Ordering::Equal,
        }
    }
}

/// Apply `rel` when either operand is an exact type; `None` when neither is. The answer is a
/// `Bool`, or a residue-dependent `Bool` when it depends on `⌈1/dt⌉`; a comparison no theorem
/// decides within the budget is a loud error.
pub fn relation<V: TowerValue>(
    rel: Rel,
    left: &V,
    right: &V,
    recurse: &dyn Fn(Rel, V, V) -> Result<V, String>,
) -> Option<Result<V, String>> {
    if !is_exact_value(left) && !is_exact_value(right) {
        return None;
    }
    if let Some(r) = lift(left, right, |a, b| recurse(rel, a, b)) {
        return Some(r);
    }
    let (Some(a), Some(b)) = (classify(left), classify(right)) else {
        if matches!(rel, Rel::Eq | Rel::NotEq) {
            return Some(Ok(V::boolean(rel == Rel::NotEq)));
        }
        return Some(Err(format!(
            "cannot compare {} and {}",
            left.type_name(),
            right.type_name()
        )));
    };
    if let Some(r) = several_relation(rel, &a, &b, left, right, recurse) {
        return Some(r);
    }
    if let Some(r) = germ_relation(rel, &a, &b, left, right, recurse) {
        return Some(r);
    }
    Some(relation_num(rel, a, b))
}

fn relation_num<V: TowerValue>(rel: Rel, a: Num, b: Num) -> Result<V, String> {
    same_scale(&a, &b)?;
    let answer = |o: Ordering| Ok(V::boolean(rel.holds(o)));
    if matches!(a, Num::Ord(_)) || matches!(b, Num::Ord(_)) {
        return match (as_ordinal(&a), as_ordinal(&b)) {
            (Some(x), Some(y)) => answer(x.cmp(&y)),
            _ => Err("an ordinal compares only with ordinals and naturals".to_string()),
        };
    }
    if let Some(scale) = scale_of(&a, &b) {
        if matches!(a, Num::Closed(..)) || matches!(b, Num::Closed(..)) {
            let x = to_closed_branches(&a, &scale.residues).expect("an operand of the real closure");
            let y = to_closed_branches(&b, &scale.residues).expect("an operand of the real closure");
            let out = x
                .zip_with(&y, |p, q| Branch(V::boolean(rel.holds(p.compare(q)))))
                .map_err(|e| scale.refuse(e))?;
            return Ok(from_depends(out, &scale));
        }
        let x = to_hyper_branches(&a, &scale.residues).expect("hyperreal operand");
        let y = to_hyper_branches(&b, &scale.residues).expect("hyperreal operand");
        let out = x
            .zip_with(&y, |p, q| Branch(V::boolean(rel.holds(p.cmp(q)))))
            .map_err(|e| scale.refuse(e))?;
        return Ok(from_depends(out, &scale));
    }
    if matches!(a, Num::Real(_)) || matches!(b, Num::Real(_)) {
        let (x, y) = (to_real(&a).expect("real"), to_real(&b).expect("real"));
        return x
            .compare(&y, DEFAULT_BUDGET)
            .map_err(|e| e.to_string())
            .and_then(answer);
    }
    match (to_alg(&a), to_alg(&b)) {
        (Some(x), Some(y)) => answer(x.cmp(&y)),
        _ => Err("cannot compare these values".to_string()),
    }
}

/// Structural equality for collections and hashing: exact forms by value, a general computable
/// real by the formula that built it; `None` when neither value is an exact type.
pub fn structurally_equal<V: TowerValue>(left: &V, right: &V) -> Option<bool> {
    Some(match (left.exact(), right.exact()) {
        (Some(ExactRef::Algebraic(a)), Some(ExactRef::Algebraic(b))) => a == b,
        (Some(ExactRef::Hyper(a)), Some(ExactRef::Hyper(b))) => a.value == b.value,
        (Some(ExactRef::Natural(a)), Some(ExactRef::Natural(b))) => a.value == b.value,
        (Some(ExactRef::Ordinal(a)), Some(ExactRef::Ordinal(b))) => a == b,
        (Some(ExactRef::Real(a)), Some(ExactRef::Real(b))) => {
            if a.is_exact_form() && b.is_exact_form() {
                a.compare(b, DEFAULT_BUDGET) == Ok(Ordering::Equal)
            } else {
                a.describe() == b.describe()
            }
        }
        (Some(ExactRef::Depends(a)), Some(ExactRef::Depends(b))) => a.value == b.value,
        (Some(ExactRef::Converging(a)), Some(ExactRef::Converging(b))) => {
            a.value().values_equal(b.value())
                && a.certificate() == b.certificate()
                && a.steps() == b.steps()
                && a.revisions() == b.revisions()
        }
        (None, None) => return None,
        _ => false,
    })
}

/// How an exact value prints; `None` for any other value.
pub fn display<V: TowerValue>(v: &V) -> Option<String> {
    Some(match v.exact()? {
        ExactRef::Algebraic(a) => a.to_string(),
        ExactRef::Real(x) => x.to_string(),
        ExactRef::Hyper(h) => h.value.render(&h.scale.name),
        ExactRef::Natural(n) => n.value.render_reciprocal(&n.scale.name),
        ExactRef::Ordinal(o) => o.to_string(),
        ExactRef::Depends(d) => d.value.render(&d.scale.generator_text(), |b| match residue_generator(&b.0) {
            Some(_) => format!("({})", b.0.display_string()),
            None => b.0.display_string(),
        }),
        ExactRef::Converging(c) => c.render(|v| v.display_string()),
    })
}

/// The standard part: a hyperreal's standard value, branch by branch for a residue-dependent
/// value; a standard value is its own. An infinite value has none.
pub fn standard_part<V: TowerValue>(v: &V) -> Result<V, String> {
    if v.is_standard_number() {
        return Ok(v.clone());
    }
    match v.exact() {
        Some(ExactRef::Hyper(h)) => match &h.value {
            HyperForm::Rational(r) => match r.standard_part() {
                Some(s) => Ok(from_algebraic(s)),
                None => Err(format!(
                    "{} is infinite and has no standard part",
                    r.render(&h.scale.name)
                )),
            },
            HyperForm::Puiseux(p) => {
                let value = Closed::Series(p.clone());
                match value.standard_part() {
                    Some(s) => Ok(from_algebraic(s)),
                    None => Err(format!(
                        "{} is infinite and has no standard part",
                        value.render(&h.scale.name)
                    )),
                }
            }
            HyperForm::Germ(g) => match g.standard_part().map_err(|e| e.to_string())? {
                Some(s) => Ok(from_exact_real(s)),
                None => Err(format!(
                    "{} is infinite and has no standard part",
                    g.render(&h.scale.name)
                )),
            },
            HyperForm::Multi(m) | HyperForm::Integer(m) => match m.standard_part() {
                Some(s) => Ok(from_algebraic(s)),
                None => Err(format!("{} is infinite and has no standard part", m.render())),
            },
            HyperForm::Nested(g) => match g.standard_part_at(None)? {
                Some(s) => Ok(from_number(s)),
                None => Err(format!("{} is infinite and has no standard part", g.render())),
            },
        },
        Some(ExactRef::Natural(n)) => Err(format!(
            "{} is infinite and has no standard part",
            n.value.render_reciprocal(&n.scale.name)
        )),
        Some(ExactRef::Depends(d)) => map_depends(d, |b| standard_part(&b)),
        Some(ExactRef::Converging(c)) => standard_part(c.value()).map(|s| carry_evidence(c, s)),
        Some(ExactRef::Algebraic(_)) | Some(ExactRef::Real(_)) => Ok(v.clone()),
        Some(ExactRef::Ordinal(_)) | None => Err(format!(
            "the standard part of a {} is undefined",
            v.type_name()
        )),
    }
}

/// How an integer part rounds: down, up, or to the nearest integer with ties away from zero (the
/// tower's `round`).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Rounding {
    Floor,
    Ceil,
    Nearest,
}

/// The integer part of an exact value under `mode`; `None` when `v` is not one (the tower handles
/// it). `recurse` is the builtin itself, for the standard values inside a dependence or a
/// provisional answer.
pub fn integer_part<V: TowerValue>(
    v: &V,
    mode: Rounding,
    recurse: &dyn Fn(V) -> Result<V, String>,
) -> Option<Result<V, String>> {
    Some(match v.exact()? {
        ExactRef::Natural(_) | ExactRef::Ordinal(_) => Ok(v.clone()),
        ExactRef::Depends(d) => map_depends(d, recurse),
        ExactRef::Converging(c) => recurse(c.value().clone()).map(|x| carry_evidence(c, x)),
        ExactRef::Algebraic(a) => Ok(V::from_bigint(algebraic_integer_part(a, mode))),
        ExactRef::Real(x) => real_integer_part(x, mode).map(V::from_bigint),
        ExactRef::Hyper(h) => hyper_integer_part(h, mode),
    })
}

fn half() -> Rational {
    Rational::from_ratio_i64(1, 2).expect("a nonzero denominator")
}

fn algebraic_integer_part(a: &Algebraic, mode: Rounding) -> BigInt {
    match mode {
        Rounding::Floor => a.floor(),
        Rounding::Ceil => a.ceil(),
        Rounding::Nearest => {
            let magnitude = if a.signum() < 0 { a.neg() } else { a.clone() };
            let m = magnitude.add(&Algebraic::from_rational(half())).floor();
            if a.signum() < 0 {
                m.negated()
            } else {
                m
            }
        }
    }
}

fn real_integer_part(x: &ExactReal, mode: Rounding) -> Result<BigInt, String> {
    let floor = |y: &ExactReal| y.floor(DEFAULT_BUDGET).map_err(|e| e.to_string());
    match mode {
        Rounding::Floor => floor(x),
        Rounding::Ceil => Ok(floor(&x.neg())?.negated()),
        Rounding::Nearest => {
            let negative = x
                .compare(&ExactReal::from_i64(0), DEFAULT_BUDGET)
                .map_err(|e| e.to_string())?
                == Ordering::Less;
            let magnitude = if negative { x.neg() } else { x.clone() };
            let m = floor(&magnitude.add(&ExactReal::from_rational(half())))?;
            Ok(if negative { m.negated() } else { m })
        }
    }
}

fn hyper_integer_part<V: TowerValue>(h: &HyperValue, mode: Rounding) -> Result<V, String> {
    let value = match &h.value {
        HyperForm::Rational(r) => r,
        HyperForm::Puiseux(p) => return closed_integer_part(&Closed::Series(p.clone()), mode, &h.scale.name),
        HyperForm::Germ(g) => return germ_integer_part(g, mode),
        HyperForm::Multi(m) => return multi_integer_part(m, mode),
        HyperForm::Integer(_) => return Ok(V::hyper(h.clone())),
        HyperForm::Nested(g) => return nested_integer_part(g, mode),
    };
    let ty = &h.scale.residues;
    let refuse = |e: crate::hypernatural::FloorError| e.describe(&h.scale.name);
    let natural = match mode {
        Rounding::Floor => Hypernatural::floor_of(value, ty).map_err(refuse)?,
        Rounding::Ceil => Hypernatural::ceil_of(value, ty).map_err(refuse)?,
        Rounding::Nearest => {
            let negative = value.signum() < 0;
            let magnitude = if negative { value.neg() } else { value.clone() };
            let m = Hypernatural::floor_of(&magnitude.add(&Hyperreal::from_rational(half())), ty)
                .map_err(refuse)?;
            if negative {
                m.neg()
            } else {
                m
            }
        }
    };
    Ok(from_natural(natural, &h.scale))
}

/// The integer part of a limited root of a hyperreal: the floor of its standard part, one less when
/// the standard part is an integer the value lies below. An infinite one has no integer part this
/// value model holds, its floor being no polynomial in `⌈1/dt⌉`.
fn closed_integer_part<V: TowerValue>(x: &Closed, mode: Rounding, name: &str) -> Result<V, String> {
    let floor_of = |x: &Closed| -> Result<BigInt, String> {
        let st = x.standard_part().ok_or_else(|| {
            format!(
                "the integer part of {} is no polynomial in ⌈1/{name}⌉, the infinite integers a program holds",
                x.render(name)
            )
        })?;
        let fl = st.floor();
        let whole = Closed::Field(Hyperreal::from_rational(Rational::from_bigint(fl.clone())));
        if x.compare(&whole) == Ordering::Less {
            Ok(fl.sub(&BigInt::from_i64(1)))
        } else {
            Ok(fl)
        }
    };
    let n = match mode {
        Rounding::Floor => floor_of(x)?,
        Rounding::Ceil => floor_of(&x.neg())?.negated(),
        Rounding::Nearest => {
            let negative = x.signum() < 0;
            let magnitude = if negative { x.neg() } else { x.clone() };
            let half = Closed::Field(Hyperreal::from_rational(half()));
            let m = floor_of(&magnitude.add(&half))?;
            if negative {
                m.negated()
            } else {
                m
            }
        }
    };
    Ok(V::from_bigint(n))
}

// ── integer parts of several infinitesimals ──────────────────────────────────────────────────

/// The integer part of a value of several infinitesimals. See [`polar_floor`].
fn multi_integer_part<V: TowerValue>(x: &Multi, mode: Rounding) -> Result<V, String> {
    several_integer_part(x, mode, &|m| multi_polar(m), &Multi::neg, &|m| {
        m.add(&Multi::Standard(Algebraic::from_rational(half())))
    }, &|m| m.signum())
}

/// The integer part of a germ of several infinitesimals. See [`polar_floor`].
fn nested_integer_part<V: TowerValue>(g: &Arc<NestedGerm>, mode: Rounding) -> Result<V, String> {
    let half = Arc::new(NestedGerm::constant(Number::from_rational(half()), &g.scale));
    let sign = |g: &Arc<NestedGerm>| g.sign().unwrap_or(0);
    several_integer_part(
        g,
        mode,
        &|g| nested_polar(g),
        &|g| Arc::new(NestedGerm::neg(g)),
        &|g| Arc::new(NestedGerm::add(g, &half)),
        &sign,
    )
}

/// The integer part under `mode` of a value whose floor [`polar_floor`] reads from its `polar` split:
/// the ceiling the negated floor of the negation, the nearest integer the floor of the magnitude plus
/// a half, its sign restored.
fn several_integer_part<V: TowerValue, X: Clone>(
    x: &X,
    mode: Rounding,
    polar: &dyn Fn(&X) -> Result<Polar, String>,
    neg: &dyn Fn(&X) -> X,
    plus_half: &dyn Fn(&X) -> X,
    sign: &dyn Fn(&X) -> i32,
) -> Result<V, String> {
    let negated = |n: Number| Number::arith(Op::Sub, Number::from_bigint(BigInt::from_i64(0)), n);
    let n = match mode {
        Rounding::Floor => polar_floor(polar(x)?)?,
        Rounding::Ceil => negated(polar_floor(polar(&neg(x))?)?)?,
        Rounding::Nearest => {
            let negative = sign(x) < 0;
            let magnitude = if negative { neg(x) } else { x.clone() };
            let m = polar_floor(polar(&plus_half(&magnitude))?)?;
            if negative {
                negated(m)?
            } else {
                m
            }
        }
    };
    Ok(from_number(n))
}

/// A value read in its smallest infinitesimal `ε`, over the larger ones: the coefficients of its terms
/// infinite in `ε`, its part constant in `ε`, and the sign of the rest — infinitesimal from every
/// larger infinitesimal's standpoint — read only when the floor needs it.
struct Polar {
    scale: Arc<Scale>,
    q: u32,
    /// The coefficient of `ε^(k/q)` for each `k < 0` with a nonzero one, a value of the larger
    /// infinitesimals.
    infinite: Vec<(i64, Number)>,
    constant: Number,
    rest: Box<dyn Fn() -> Result<i32, String>>,
    shown: String,
    generators: Vec<Arc<Scale>>,
}

fn multi_polar(m: &Multi) -> Result<Polar, String> {
    let scale = m.top().expect("a value of several infinitesimals has a smallest").clone();
    let expansion = crate::closure::AlgValue::at(m, &scale).expansion;
    let (floor, q) = (expansion.floor().min(0), expansion.ramification());
    let terms: Vec<Multi> = (floor..=0)
        .map(|k| expansion.coefficient(k).map_err(|e| e.to_string()))
        .collect::<Result<_, _>>()?;
    let mut den = vec![Multi::zero(); (-floor) as usize + 1];
    den[(-floor) as usize] = Multi::Standard(Algebraic::from_i64(1));
    let polar = Multi::make(&scale, q, PolyOver::from(terms.clone()), PolyOver::from(den));
    let rest = m.sub(&polar);
    Ok(Polar {
        scale: scale.clone(),
        q,
        infinite: (floor..0)
            .zip(&terms)
            .filter(|(_, c)| !c.is_zero())
            .map(|(k, c)| (k, from_multi(c.clone())))
            .collect(),
        constant: from_multi(terms.last().expect("order 0 is read").clone()),
        rest: Box::new(move || Ok(rest.signum())),
        shown: m.render(),
        generators: m.scales(),
    })
}

fn nested_polar(g: &Arc<NestedGerm>) -> Result<Polar, String> {
    let (floor, q) = (g.expansion.floor().min(0), g.expansion.ramification());
    let terms: Vec<Number> = (floor..=0)
        .map(|k| g.expansion.coefficient(k).map_err(|e| e.to_string()))
        .collect::<Result<_, _>>()?;
    let expansion = g.expansion.clone();
    let reach = crate::germ::SIGN_ORDERS * i64::from(q);
    Ok(Polar {
        scale: g.scale.clone(),
        q,
        infinite: (floor..0)
            .zip(&terms)
            .filter(|(_, c)| !matches!(c.standard_rational(), Some(r) if r.is_zero()))
            .map(|(k, c)| (k, c.clone()))
            .collect(),
        constant: terms.last().expect("order 0 is read").clone(),
        rest: Box::new(move || {
            for k in 1..=reach {
                let c = expansion.coefficient(k).map_err(|e| e.to_string())?;
                let s = crate::expansion::Coefficient::sign(&c).map_err(|e| e.to_string())?;
                if s != 0 {
                    return Ok(s);
                }
            }
            Err(crate::germ::GermError::Flat.to_string())
        }),
        shown: g.render(),
        generators: g.scales(),
    })
}

/// The floor of a value `x` of several infinitesimals, from its split in its smallest one, `ε`:
/// `x = P + a + ρ`, `P = Σ_{j≥1} c_j·(1/ε)^j` its part infinite in `ε`, `a` a value of the larger
/// infinitesimals and `ρ` infinitesimal from all of their standpoints.
///
/// The floor is an infinite integer a program holds — a polynomial in the reciprocals of the
/// infinitesimals with rational coefficients on each residue class of each — exactly when every `c_j`
/// is one of the larger infinitesimals' reciprocals: `1/(dt·dx)` is `⌈1/dt⌉·⌈1/dx⌉`. A coefficient
/// that is not, `dt` in `dt/dx`, leaves a fraction that no residue of `⌈1/ε⌉` decides, and so does a
/// root of `1/ε`. With `D` the coefficients' common denominator, on each class `h` of `⌈1/ε⌉` modulo `D`,
/// `P − R_h` is an integer for `R_h = Σ c_j·h^j`, a value of the larger infinitesimals, so
/// `⌊x⌋ = P − R_h + ⌊R_h + a + ρ⌋`: the same floor one infinitesimal up, `⌈R_h + a⌉ − 1` when `ρ` is
/// negative. The classes' answers join as one value ([`from_depends`]): an infinite integer of one
/// infinitesimal where they all are, otherwise a dependence on the coarsest residue whose branches
/// read the finer.
fn polar_floor(p: Polar) -> Result<Number, String> {
    let mut generators = p.generators.clone();
    generators.sort_by(|a, b| b.order(a).unwrap_or(Ordering::Equal));
    let names: Vec<String> = generators.iter().map(|g| g.generator_text()).collect();
    let held = match names.split_last() {
        Some((last, [])) => last.clone(),
        Some((last, init)) => format!("{} and {last}", init.join(", ")),
        None => String::new(),
    };
    let refuse = |why: String| {
        format!(
            "the integer part of {} is no polynomial in {held}, the infinite integers a program holds: {why}",
            p.shown
        )
    };
    let name = &p.scale.name;
    let mut powers: Vec<(u32, Number)> = Vec::new();
    let mut denominator = BigInt::from_i64(1);
    for (k, c) in &p.infinite {
        if k % i64::from(p.q) != 0 {
            return Err(refuse(format!("it holds a root of 1/{name}")));
        }
        let Some(d) = reciprocal_denominator(c) else {
            return Err(refuse(format!(
                "it multiplies a power of 1/{name} by {}, which is no polynomial in the reciprocals of the infinitesimals \
                 larger than {name} with rational coefficients",
                c.display_string()
            )));
        };
        denominator = big_lcm(&denominator, &d);
        powers.push(((-k / i64::from(p.q)) as u32, c.clone()));
    }
    let ty = p.scale.residues.clone();
    let classes = denominator
        .to_i64()
        .and_then(|d| u64::try_from(d).ok())
        .ok_or_else(|| ResidueError::TooFine { classes: denominator.clone() })
        .and_then(|d| crate::limit_value::bounded_lcm(ty.modulus(), d))
        .map_err(|e| refuse(e.describe(&p.scale.generator_text())))?;
    let reciprocal = from_hyper::<Number>(Hyperreal::from_reciprocal_powers(&[Rational::zero(), Rational::one()]), &p.scale);
    let add = |a: Number, b: Number| Number::arith(Op::Add, a, b);
    let mul = |a: Number, b: Number| Number::arith(Op::Mul, a, b);
    let mut infinite = Number::from_bigint(BigInt::from_i64(0));
    for (j, c) in &powers {
        let power = Number::arith(Op::Pow, reciprocal.clone(), Number::from_bigint(BigInt::from_i64(i64::from(*j))))?;
        infinite = add(infinite, mul(c.clone(), power)?)?;
    }
    let mut rest: Option<i32> = None;
    let mut raw = Vec::with_capacity(classes as usize);
    for h in 0..classes {
        if !ty.admits(h) {
            raw.push(None);
            continue;
        }
        let mut r_h = Number::from_bigint(BigInt::from_i64(0));
        for (j, c) in &powers {
            let at = Rational::from_i64(h as i64).pow(*j as i32).expect("a natural power");
            r_h = add(r_h, mul(c.clone(), Number::from_rational(at))?)?;
        }
        let c = add(r_h.clone(), p.constant.clone())?;
        let below = floor_number(&c)?;
        let above = Number::arith(
            Op::Sub,
            negate(floor_number(&negate(c)?)?)?,
            Number::from_bigint(BigInt::from_i64(1)),
        )?;
        let inner = if below.values_equal(&above) {
            below
        } else {
            let sign = match rest {
                Some(s) => s,
                None => *rest.insert((p.rest)()?),
            };
            if sign < 0 {
                above
            } else {
                below
            }
        };
        let whole = integral_on(Number::arith(Op::Sub, infinite.clone(), r_h)?, &p.scale, &ty, h, classes)?;
        raw.push(Some(Branch(add(whole, inner)?)));
    }
    let joined = Depends::from_branches(ty, classes, raw).expect("the classes are the type's own");
    Ok(from_depends(joined, &p.scale))
}

fn big_lcm(a: &BigInt, b: &BigInt) -> BigInt {
    let g = a.gcd(b);
    a.div_rem(&g).expect("a nonzero divisor").0.mul(b).abs()
}

/// `whole`, a polynomial in the reciprocals that is an integer on the class `h` modulo `m` of `scale`'s
/// generator, as the integer it is there: one of one infinitesimal on that class's own scale, whose facts
/// make it one; one of several is one by its scales already ([`from_multi`]).
fn integral_on(whole: Number, scale: &Arc<Scale>, ty: &ResidueType, h: u64, m: u64) -> Result<Number, String> {
    let Some(ExactRef::Hyper(x)) = whole.exact() else {
        return Ok(whole);
    };
    match &x.value {
        HyperForm::Rational(r) if x.scale.same_infinitesimal(scale) => {
            let class = Arc::new(scale.with_residues(ty.and(&ResidueType::congruent(h, m)).map_err(|e| scale.refuse(e))?));
            let natural = r
                .as_reciprocal_powers()
                .and_then(|p| Hypernatural::from_polynomial(Poly::from_coeffs(p), &class.residues))
                .expect("the part of a floor infinite in its smallest infinitesimal is an integer on its class");
            Ok(from_natural(natural, &class))
        }
        _ => Ok(whole),
    }
}

fn negate(n: Number) -> Result<Number, String> {
    Number::arith(Op::Sub, Number::from_bigint(BigInt::from_i64(0)), n)
}

/// The common denominator of a polynomial in the reciprocals of infinitesimals with rational
/// coefficients — `1/(2·dt) + 1/3` has `6` — or `None` for a number that is no such polynomial.
fn reciprocal_denominator(n: &Number) -> Option<BigInt> {
    if let Some(r) = n.standard_rational() {
        return Some(r.denominator().clone());
    }
    match n.exact()? {
        ExactRef::Natural(m) => {
            let mut d = BigInt::from_i64(1);
            for (_, poly) in m.value.depends().branches() {
                for c in poly.coeffs() {
                    d = big_lcm(&d, c.denominator());
                }
            }
            Some(d)
        }
        ExactRef::Hyper(h) => match &h.value {
            HyperForm::Rational(r) => Some(
                r.as_reciprocal_powers()?
                    .iter()
                    .fold(BigInt::from_i64(1), |d, c| big_lcm(&d, c.denominator())),
            ),
            HyperForm::Multi(m) | HyperForm::Integer(m) => {
                let polar = multi_polar(m).ok()?;
                if polar.infinite.iter().any(|(k, _)| k % i64::from(polar.q) != 0) || (polar.rest)().ok()? != 0 {
                    return None;
                }
                polar
                    .infinite
                    .iter()
                    .map(|(_, c)| c)
                    .chain(std::iter::once(&polar.constant))
                    .try_fold(BigInt::from_i64(1), |d, c| Some(big_lcm(&d, &reciprocal_denominator(c)?)))
            }
            _ => None,
        },
        _ => None,
    }
}

/// The floor of a number, in base's own value model.
fn floor_number(x: &Number) -> Result<Number, String> {
    if let Some(r) = x.standard_rational() {
        return Ok(Number::from_bigint(r.floor()));
    }
    integer_part(x, Rounding::Floor, &|v| floor_number(&v))
        .unwrap_or_else(|| Err(format!("cannot take the integer part of {}", x.display_string())))
}

/// The integer part of a germ: the floor of its standard part, one less when the standard part
/// is an integer the germ approaches from below.
fn germ_integer_part<V: TowerValue>(g: &Germ, mode: Rounding) -> Result<V, String> {
    let text = |e: crate::germ::GermError| e.to_string();
    let floor_of = |g: &Germ| -> Result<BigInt, String> {
        let st = g.standard_part().map_err(text)?.ok_or_else(|| {
            "the integer part of a value with a pole in the infinitesimal past a polynomial in its reciprocal is not computed".to_string()
        })?;
        let fl = st.floor(DEFAULT_BUDGET).map_err(|e| e.to_string())?;
        let whole = ExactReal::from_rational(Rational::from_bigint(fl.clone()));
        let on_integer = st.compare(&whole, DEFAULT_BUDGET).map_err(|e| e.to_string())? == Ordering::Equal;
        if on_integer && g.sub(&Germ::constant(&whole)).signum().map_err(text)? < 0 {
            Ok(fl.sub(&BigInt::from_i64(1)))
        } else {
            Ok(fl)
        }
    };
    let n = match mode {
        Rounding::Floor => floor_of(g)?,
        Rounding::Ceil => floor_of(&g.neg())?.negated(),
        Rounding::Nearest => {
            let negative = g.signum().map_err(text)? < 0;
            let magnitude = if negative { g.neg() } else { g.clone() };
            let half = Germ::constant(&ExactReal::from_rational(half()));
            let m = floor_of(&magnitude.add(&half))?;
            if negative {
                m.negated()
            } else {
                m
            }
        }
    };
    Ok(V::from_bigint(n))
}

/// `x ≈ 0`: zero or an infinitesimal.
pub fn is_infinitesimal<V: TowerValue>(v: &V) -> Result<V, String> {
    match v.exact() {
        Some(ExactRef::Hyper(h)) => match &h.value {
            HyperForm::Rational(r) => Ok(V::boolean(r.is_infinitesimal())),
            HyperForm::Puiseux(p) => Ok(V::boolean(Closed::Series(p.clone()).is_infinitesimal())),
            HyperForm::Germ(g) => match g.standard_part().map_err(|e| e.to_string())? {
                None => Ok(V::boolean(false)),
                Some(s) => Ok(V::boolean(
                    s.compare(&ExactReal::from_i64(0), DEFAULT_BUDGET)
                        .map_err(|e| e.to_string())?
                        == Ordering::Equal,
                )),
            },
            HyperForm::Multi(m) | HyperForm::Integer(m) => Ok(V::boolean(m.is_infinitesimal())),
            HyperForm::Nested(g) => Ok(V::boolean(matches!(
                g.standard_part_at(None)?,
                Some(s) if s.standard_rational().is_some_and(|r| r.is_zero())
            ))),
        },
        Some(ExactRef::Natural(_)) => Ok(V::boolean(false)),
        Some(ExactRef::Depends(d)) => map_depends(d, |b| is_infinitesimal(&b)),
        _ => match classify(v) {
            Some(Num::Rat(r)) => Ok(V::boolean(r.is_zero())),
            Some(Num::Alg(a)) => Ok(V::boolean(a.is_zero())),
            Some(Num::Real(x)) => Ok(V::boolean(x.is_exactly_zero())),
            _ => Err(format!("a {} is not a number", v.type_name())),
        },
    }
}

/// Bounded by a standard number.
pub fn is_limited<V: TowerValue>(v: &V) -> Result<V, String> {
    match v.exact() {
        Some(ExactRef::Hyper(h)) => match &h.value {
            HyperForm::Rational(r) => Ok(V::boolean(r.is_limited())),
            HyperForm::Puiseux(p) => Ok(V::boolean(Closed::Series(p.clone()).is_limited())),
            HyperForm::Germ(g) => Ok(V::boolean(
                g.standard_part().map_err(|e| e.to_string())?.is_some(),
            )),
            HyperForm::Multi(m) | HyperForm::Integer(m) => Ok(V::boolean(m.is_limited())),
            HyperForm::Nested(g) => Ok(V::boolean(g.standard_part_at(None)?.is_some())),
        },
        Some(ExactRef::Natural(n)) => Ok(from_depends(
            n.value.is_infinite().map(|inf| Branch(V::boolean(!inf))),
            &n.scale,
        )),
        Some(ExactRef::Depends(d)) => map_depends(d, |b| is_limited(&b)),
        _ => match classify(v) {
            Some(Num::Rat(_)) | Some(Num::Alg(_)) | Some(Num::Real(_)) => Ok(V::boolean(true)),
            _ => Err(format!("a {} is not a number", v.type_name())),
        },
    }
}

// ── relative to an infinitesimal ──────────────────────────────────────────────────────────────

/// What a value is from the standpoint of an infinitesimal `at`, where every value of `at` and of the
/// infinitesimals larger than it is an ordinary number: itself when it involves no smaller one, the
/// value it is infinitely close to there when it is limited from that standpoint, and none when it is
/// infinite from it.
enum Relative<V> {
    Ordinary,
    Close(V),
    Infinite,
}

/// The infinitesimal `relative to` names: the infinitesimal itself.
fn standpoint<V: TowerValue>(at: &V) -> Result<Arc<Scale>, String> {
    infinitesimal_scale(at)
        .ok_or_else(|| format!("`relative to` names an infinitesimal itself, not {}", at.display_string()))
}

fn read_relative<V: TowerValue>(v: &V, at: &Arc<Scale>) -> Result<Relative<V>, String> {
    let ordered = |s: &Arc<Scale>| -> Result<Ordering, String> {
        s.order(at).ok_or_else(|| {
            format!(
                "cannot read a value of {} relative to {}, whose order the program does not state; declare one much smaller than the other",
                s.name, at.name
            )
        })
    };
    let Some(n) = classify(v) else {
        return Err(format!("a {} is not a number", v.type_name()));
    };
    if let Num::Multi(m) = &n {
        for s in m.scales() {
            ordered(&s)?;
        }
        return Ok(match m.standard_part_at(Some(at)) {
            None => Relative::Infinite,
            Some(c) if c == *m => Relative::Ordinary,
            Some(c) => Relative::Close(from_multi(c)),
        });
    }
    if let Num::Nested(g) = &n {
        for s in g.scales() {
            ordered(&s)?;
        }
        if g.scale.order(at) != Some(Ordering::Less) {
            return Ok(Relative::Ordinary);
        }
        return Ok(match g.standard_part_at(Some(at))? {
            None => Relative::Infinite,
            Some(c) => Relative::Close(from_number(c)),
        });
    }
    let Some(scale) = scale_of(&n, &n) else {
        return match n {
            Num::Ord(_) => Err(format!("the standard part of a {} is undefined", v.type_name())),
            _ => Ok(Relative::Ordinary),
        };
    };
    if ordered(&scale)? != Ordering::Less {
        return Ok(Relative::Ordinary);
    }
    let limited = is_limited(v)?;
    if limited.values_equal(&V::boolean(false)) {
        return Ok(Relative::Infinite);
    }
    if let Some(why) = undecided_branch(&limited) {
        return Err(why);
    }
    standard_part(v).map(Relative::Close)
}

/// The standard part relative to the infinitesimal `at`: what `v` is infinitely close to among the
/// values of `at` and the infinitesimals larger than it, every smaller infinitesimal read at zero — the
/// inner limit with `at` held fixed. `the standard part of dt + dx relative to dt` is `dt`.
pub fn standard_part_relative<V: TowerValue>(v: &V, at: &V) -> Result<V, String> {
    match v.exact() {
        Some(ExactRef::Depends(d)) => return map_depends(d, |b| standard_part_relative(&b, at)),
        Some(ExactRef::Converging(c)) => {
            return standard_part_relative(c.value(), at).map(|s| carry_evidence(c, s));
        }
        _ => {}
    }
    let scale = standpoint(at)?;
    match read_relative(v, &scale)? {
        Relative::Ordinary => Ok(v.clone()),
        Relative::Close(s) => Ok(s),
        Relative::Infinite => Err(format!(
            "{} is infinite relative to {} and has no standard part relative to it",
            v.display_string(),
            scale.name
        )),
    }
}

/// Zero, or smaller than every positive value of `at` and of the infinitesimals larger than it.
pub fn is_infinitesimal_relative<V: TowerValue>(v: &V, at: &V) -> Result<V, String> {
    match v.exact() {
        Some(ExactRef::Depends(d)) => return map_depends(d, |b| is_infinitesimal_relative(&b, at)),
        Some(ExactRef::Converging(c)) => {
            return is_infinitesimal_relative(c.value(), at).map(|s| carry_evidence(c, s));
        }
        _ => {}
    }
    let scale = standpoint(at)?;
    Ok(V::boolean(match read_relative(v, &scale)? {
        Relative::Ordinary => is_standard_zero(v),
        Relative::Close(s) => is_standard_zero(&s),
        Relative::Infinite => false,
    }))
}

/// Bounded by a value of `at` and of the infinitesimals larger than it.
pub fn is_limited_relative<V: TowerValue>(v: &V, at: &V) -> Result<V, String> {
    match v.exact() {
        Some(ExactRef::Depends(d)) => return map_depends(d, |b| is_limited_relative(&b, at)),
        Some(ExactRef::Converging(c)) => {
            return is_limited_relative(c.value(), at).map(|s| carry_evidence(c, s));
        }
        _ => {}
    }
    let scale = standpoint(at)?;
    Ok(V::boolean(!matches!(read_relative(v, &scale)?, Relative::Infinite)))
}

/// Whether a value is the number zero.
fn is_standard_zero<V: TowerValue>(v: &V) -> bool {
    v.standard_rational().is_some_and(|r| r.is_zero())
}

/// A function of the reals the exact types take: the square root, the exponential, the natural
/// logarithm.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum RealFn {
    Sqrt,
    Exp,
    Ln,
}

impl RealFn {
    fn noun(self) -> &'static str {
        match self {
            RealFn::Sqrt => "square root",
            RealFn::Exp => "exponential",
            RealFn::Ln => "natural logarithm",
        }
    }
}

/// `f` of `v`, exactly. A standard number goes in as the rational it denotes (a float as its dyadic
/// rational), an algebraic number or a computable real as itself, and the answer is held in its
/// smallest exact form: `sqrt(4)` is `2`, `sqrt(2)` is `√2`, `exp(0)` is `1`, `ln(e)` is `1`. The
/// square root of a hyperreal or an infinite integer is its root in the real closure
/// ([`crate::puiseux`]): `sqrt(dt)` is `√dt`. Every other function of a value of the infinitesimal is
/// the germ of it ([`Germ`]): `exp(dt)` is `1 + dt + O(dt^2)`, `ln(1 + dt)` is
/// `dt - (1/2)·dt^2 + O(dt^3)`, and the root of a germ is a germ. What is no germ is refused by name:
/// the exponential of an infinite value, beyond every power of `dt`, and the logarithm of a positive
/// infinitesimal or an infinite value, which carries `ln(dt)`. A residue-dependent value is mapped
/// branch by branch and a provisional one keeps its evidence; a function of an ordinal has no exact
/// form.
pub fn real_fn<V: TowerValue>(f: RealFn, v: &V) -> Result<V, String> {
    match v.exact() {
        Some(ExactRef::Depends(d)) => return map_depends(d, |b| real_fn(f, &b)),
        Some(ExactRef::Converging(c)) => {
            return real_fn(f, c.value()).map(|x| carry_evidence(c, x));
        }
        _ => {}
    }
    let x = match classify(v) {
        Some(Num::Rat(r)) => ExactReal::from_rational(r),
        Some(Num::Alg(a)) => ExactReal::from_algebraic(a),
        Some(Num::Real(x)) => x,
        Some(n @ (Num::Hyper(..) | Num::Nat(..) | Num::Closed(..))) if f == RealFn::Sqrt => {
            let scale = scale_of(&n, &n).expect("a hyperreal has its infinitesimal");
            let branches = to_closed_branches(&n, &scale.residues).expect("a value of the real closure");
            let err = RefCell::new(None);
            let out = branches.map(|c| capture(&err, c.root(2).map(|r| from_closed(r, &scale))));
            return match err.into_inner() {
                Some(e) => Err(e),
                None => Ok(from_depends(out, &scale)),
            };
        }
        Some(Num::Germ(g, scale)) => return germ_fn(f, &g, v, &scale).map(|g| from_germ(g, &scale)),
        Some(Num::Multi(m)) => {
            if f == RealFn::Sqrt {
                return m.root(2).map(from_multi);
            }
            let scale = m.top().expect("a value of several infinitesimals has a smallest").clone();
            let g = Arc::new(NestedGerm::exact(&m, &scale));
            return nested_fn(f, &g, &v.display_string()).map(from_nested);
        }
        Some(Num::Nested(g)) => return nested_fn(f, &g, &v.display_string()).map(from_nested),
        Some(n @ (Num::Hyper(..) | Num::Nat(..) | Num::Closed(..))) => {
            let scale = scale_of(&n, &n).expect("a hyperreal has its infinitesimal");
            let branches = to_closed_branches(&n, &scale.residues).expect("a value of the real closure");
            let err = RefCell::new(None);
            let out = branches.map(|c| {
                capture(&err, germ_fn(f, &closed_germ(c), v, &scale).map(|g| from_germ(g, &scale)))
            });
            return match err.into_inner() {
                Some(e) => Err(e),
                None => Ok(from_depends(out, &scale)),
            };
        }
        Some(Num::Ord(_)) => {
            return Err(format!(
                "the {} of {} has no exact form",
                f.noun(),
                v.display_string()
            ))
        }
        None => return Err(format!("a {} is not a number", v.type_name())),
    };
    let y = match f {
        RealFn::Sqrt => x.sqrt(),
        RealFn::Exp => Ok(x.exp()),
        RealFn::Ln => x.log(),
    };
    y.map(from_exact_real).map_err(|e| e.to_string())
}

/// `f` of a germ of several infinitesimals; what has no germ refused in the words `shown` prints.
fn nested_fn(f: RealFn, g: &Arc<NestedGerm>, shown: &str) -> Result<NestedGerm, String> {
    match f {
        RealFn::Sqrt => NestedGerm::root(g, 2),
        RealFn::Exp => NestedGerm::exp(g, shown),
        RealFn::Ln => NestedGerm::ln(g, shown),
    }
}

/// `f` of a germ, the germ of `v`; what has no germ refused in the words of `v` and the program's
/// infinitesimal.
fn germ_fn<V: TowerValue>(f: RealFn, g: &Germ, v: &V, scale: &Scale) -> Result<Germ, String> {
    use crate::germ::GermError;
    let out = match f {
        RealFn::Sqrt => g.root(2),
        RealFn::Exp => g.exp(),
        RealFn::Ln => g.ln(),
    };
    out.map_err(|e| match e {
        GermError::BeyondEveryPower => format!(
            "the exponential of {} is beyond every power of {}",
            v.display_string(),
            scale.name
        ),
        GermError::CarriesLog { infinite } => format!(
            "the logarithm of {} carries ln({}{})",
            v.display_string(),
            if infinite { "1/" } else { "" },
            scale.name
        ),
        e => e.to_string(),
    })
}

/// `base ** exponent` for an exponent that is an exact number — what `**` and `pow` are when their
/// exponent is one: a fraction `p/q` takes the real `q`-th root and raises it to `p` (`2 ** (1/2)` is
/// `√2`, `dt ** (1/2)` is `√dt`, an even root of a negative number refused), and any other exponent is
/// the language's own `**`, a float on either side the float power. A residue-dependent or provisional
/// operand is followed branch by branch.
pub fn exact_power<V: ValueAlgebra>(base: &V, exponent: &V) -> Result<V, String> {
    if let Some(r) = lift(base, exponent, |a, b| exact_power(&a, &b)) {
        return r;
    }
    let Some((p, q)) = fractional_exponent(exponent) else {
        return V::power(base.clone(), exponent.clone());
    };
    if is_exact_value(base) {
        let recurse = |op: Op, a: V, b: V| -> Result<V, String> {
            match op {
                Op::Pow => exact_power(&a, &b),
                Op::Add => V::add(a, b),
                Op::Sub => V::subtract(a, b),
                Op::Mul => V::multiply(a, b),
                Op::Div | Op::ExactDiv => V::exact_divide(a, b),
                Op::Mod => V::modulo(a, b),
                Op::FloorDiv => Err("an exact power floors nothing".to_string()),
            }
        };
        return arith(Op::Pow, base, exponent, &recurse).expect("an exact base is the tower's");
    }
    match base.exact_rational() {
        Some(r) => Algebraic::from_rational(r)
            .nth_root(q)
            .ok_or_else(|| negative_root(q))?
            .pow(p)
            .map(from_algebraic)
            .ok_or_else(|| "zero cannot be raised to a negative power".to_string()),
        None => V::power(base.clone(), exponent.clone()),
    }
}

/// π, exactly.
pub fn pi<V: TowerValue>() -> V {
    from_exact_real(ExactReal::pi())
}

/// e, exactly.
pub fn euler<V: TowerValue>() -> V {
    from_exact_real(ExactReal::e())
}

/// ω, the first infinite ordinal.
pub fn omega<V: TowerValue>() -> V {
    from_ordinal(Ordinal::omega())
}

/// The program's infinitesimal: `Let <name> be an infinitesimal …`, its reciprocal's residues
/// modulo `modulus` limited to `allowed` (the parser has already intersected the stated facts),
/// or the contradiction refused when nothing is allowed.
pub fn new_infinitesimal<V: TowerValue>(name: &str, modulus: u64, allowed: &[u64]) -> Result<V, String> {
    let residues = ResidueType::from_allowed(modulus.max(1), allowed)
        .map_err(|e| e.describe(&format!("1/{name}")))?;
    Ok(V::hyper(HyperValue {
        value: HyperForm::Rational(Hyperreal::dt()),
        scale: Arc::new(Scale::new(name, residues)),
    }))
}

/// `Let <name> be an infinitesimal much smaller than <larger> [and much larger than <smaller>] …`: an
/// infinitesimal below `larger` and above `smaller`, each an infinitesimal itself or nothing, with its
/// reciprocal's residues as [`new_infinitesimal`] reads them. Refused when a bound is no infinitesimal,
/// when the two bounds are not already ordered, and when the name is one an infinitesimal it would be
/// ordered with already has.
pub fn new_ordered_infinitesimal<V: TowerValue>(
    name: &str,
    larger: &V,
    smaller: &V,
    modulus: u64,
    allowed: &[u64],
) -> Result<V, String> {
    let bound = |v: &V, relation: &str| -> Result<Option<Arc<Scale>>, String> {
        if v.is_nothing() {
            return Ok(None);
        }
        infinitesimal_scale(v).map(Some).ok_or_else(|| {
            format!(
                "an infinitesimal is declared {relation} another infinitesimal itself, not than {}",
                v.display_string()
            )
        })
    };
    let larger = bound(larger, "much smaller than")?;
    let smaller = bound(smaller, "much larger than")?;
    let residues = ResidueType::from_allowed(modulus.max(1), allowed)
        .map_err(|e| e.describe(&format!("1/{name}")))?;
    let scale = Scale::ordered(name, residues, larger, smaller)?;
    Ok(V::hyper(HyperValue {
        value: HyperForm::Rational(Hyperreal::dt()),
        scale: Arc::new(scale),
    }))
}

/// The infinitesimal a value is, when it is an infinitesimal itself.
fn infinitesimal_scale<V: TowerValue>(v: &V) -> Option<Arc<Scale>> {
    match v.exact()? {
        ExactRef::Hyper(h) if h.value == HyperForm::Rational(Hyperreal::dt()) => Some(h.scale.clone()),
        _ => None,
    }
}

/// The infinite natural `⌈1/dt⌉` generated by an infinitesimal value.
pub fn generator_of<V: TowerValue>(v: &V) -> Result<V, String> {
    match v.exact() {
        Some(ExactRef::Hyper(h)) if h.value == HyperForm::Rational(Hyperreal::dt()) => {
            Ok(V::natural(NaturalValue {
                value: Hypernatural::generator(&h.scale.residues),
                scale: h.scale.clone(),
            }))
        }
        _ => Err(format!(
            "the infinite generator is taken of the infinitesimal itself, not of {}",
            v.display_string()
        )),
    }
}

/// A limit rule by its English name.
pub fn limit_rule(name: &str) -> Result<LimitRule, String> {
    Ok(match name {
        "the standard part" | "standard part" => LimitRule::StandardPart,
        "the limit" | "limit" => LimitRule::Limit,
        "the limit superior" | "limit superior" => LimitRule::LimitSuperior,
        "the limit inferior" | "limit inferior" => LimitRule::LimitInferior,
        "the Cesàro mean" | "the Cesaro mean" | "Cesàro mean" | "Cesaro mean" => LimitRule::CesaroMean,
        other => return Err(format!("unknown limit rule: {other}")),
    })
}

/// Resolve a residue-dependent value under a limit rule; a value that does not depend on the
/// residue is its own limit under every rule. A value that depends on the residues of several
/// generators resolves each branch's finer dependence first: the residues of different generators
/// are independent, so the rule over every pair of classes is the rule over the coarser generator's
/// classes of the rule over the finer one's.
pub fn apply_limit<V: TowerValue>(v: &V, rule: LimitRule) -> Result<V, String> {
    let Some(d) = depends_of(v) else {
        return Ok(v.clone());
    };
    if d.value.branches().any(|(_, b)| residue_generator(&b.0).is_some()) {
        let inner = map_depends(d, |b| apply_limit(&b, rule)).map_err(|e| match rule {
            LimitRule::Limit | LimitRule::StandardPart => {
                format!("no limit: the value is {}", display(v).expect("a dependence displays"))
            }
            _ => e,
        })?;
        return apply_limit(&inner, rule);
    }
    let as_alg = d.value.map(|b| match classify(&b.0) {
        Some(Num::Rat(r)) => Some(Algebraic::from_rational(r)),
        Some(Num::Alg(a)) => Some(a),
        _ => None,
    });
    let all_numeric = as_alg.branches().all(|(_, a)| a.is_some());
    if !all_numeric {
        return match (rule, d.value.single()) {
            (_, Some(b)) => Ok(b.0.clone()),
            (LimitRule::Limit | LimitRule::StandardPart, None) => Err(format!(
                "no limit: the value is {}",
                display(v).expect("a dependence displays")
            )),
            _ => Err("only a numeric value has a limit superior, inferior or mean".to_string()),
        };
    }
    let algebraic = as_alg.map(|a| a.clone().expect("checked numeric"));
    algebraic
        .apply_with(rule, &d.scale.generator_text())
        .map(from_algebraic)
}

/// A provisional answer: the current guess after `steps` cases with `revisions` changes. A guess
/// that is already an answer joins this evidence to its own.
pub fn provisional<V: TowerValue>(value: V, steps: u64, revisions: u64) -> V {
    carry_evidence(&Converging::provisional((), steps, revisions), value)
}

/// Why a value cannot decide a branch — a residue-dependent answer, or a provisional one no proof
/// settled — or `None` for any other value. Every tier refuses such a branch with this sentence.
pub fn undecided_branch<V: TowerValue>(v: &V) -> Option<String> {
    match v.exact()? {
        ExactRef::Depends(_) => {
            let mut generators = Vec::new();
            generators_read(v, &mut generators);
            let listed = |each: &dyn Fn(&Scale) -> String| {
                let words: Vec<String> = generators.iter().map(|g| each(g)).collect();
                match words.split_last() {
                    Some((last, [])) => last.clone(),
                    Some((last, init)) => format!("{} and {last}", init.join(", ")),
                    None => unreachable!("a dependence reads a generator"),
                }
            };
            Some(format!(
                "this condition depends on the residue{} of {}: it is {}; declare what is known about {} or take a limit",
                if generators.len() > 1 { "s" } else { "" },
                listed(&|g| g.generator_text()),
                display(v).expect("a dependence displays"),
                listed(&|g| format!("1/{}", g.name)),
            ))
        }
        ExactRef::Converging(c) if !c.is_settled() => Some(format!(
            "a provisional answer cannot decide a condition: {}",
            display(v).expect("a provisional answer displays")
        )),
        _ => None,
    }
}

/// `not` lifted over residue branches and through provisional values; `None` for any other value.
pub fn not<V: TowerValue>(
    v: &V,
    recurse: &dyn Fn(V) -> Result<V, String>,
) -> Option<Result<V, String>> {
    match v.exact()? {
        ExactRef::Depends(d) => Some(map_depends(d, recurse)),
        ExactRef::Converging(c) => Some(recurse(c.value().clone()).map(|x| carry_evidence(c, x))),
        _ => None,
    }
}

// ── transport ─────────────────────────────────────────────────────────────────────────────────

/// Whether a value of the exact types can travel as data — to a task, through a channel, over the
/// wire: every value but one holding a real built from a function a program defines, in itself, in a
/// germ, in a branch of a residue-dependent value or as a provisional answer. A value model's own
/// lists are its own to walk.
pub fn transmissible<V: TowerValue>(v: &V) -> bool {
    match v.exact() {
        Some(ExactRef::Real(x)) => x.is_transmissible(),
        Some(ExactRef::Hyper(h)) => match &h.value {
            HyperForm::Germ(g) => g.is_transmissible(),
            HyperForm::Nested(g) => g.is_transmissible(),
            HyperForm::Rational(_) | HyperForm::Puiseux(_) | HyperForm::Multi(_) | HyperForm::Integer(_) => true,
        },
        Some(ExactRef::Depends(d)) => d.value.branches().all(|(_, b)| transmissible(&b.0)),
        Some(ExactRef::Converging(c)) => transmissible(c.value()),
        Some(ExactRef::Algebraic(_) | ExactRef::Natural(_) | ExactRef::Ordinal(_)) | None => true,
    }
}

/// An algebraic number (`0`), computable real (`1`) or ordinal (`2`) as its canonical bytes; `None`
/// for any other value, and for a real built from a function a program defines, which stays with the
/// program.
pub fn exact_bytes<V: TowerValue>(v: &V) -> Option<(u8, Vec<u8>)> {
    Some(match v.exact()? {
        ExactRef::Algebraic(a) => (0, a.to_bytes()),
        ExactRef::Real(x) if x.is_transmissible() => (1, x.to_bytes()),
        ExactRef::Ordinal(o) => (2, o.to_bytes()),
        _ => return None,
    })
}

/// The value [`exact_bytes`] wrote; `None` for a forged or non-canonical encoding.
pub fn from_exact_bytes<V: TowerValue>(kind: u8, bytes: &[u8]) -> Option<V> {
    let v: V = match kind {
        0 => from_algebraic(Algebraic::from_bytes(bytes)?),
        1 => from_exact_real(ExactReal::from_bytes(bytes)?),
        2 => from_ordinal(Ordinal::from_bytes(bytes)?),
        _ => return None,
    };
    (exact_bytes(&v)? == (kind, bytes.to_vec())).then_some(v)
}

/// The infinitesimal's name and its declaration's bytes ([`Scale::to_bytes`]): its reciprocal's
/// residue facts, and where it stands among the others.
pub fn scale_parts(scale: &Scale) -> (String, Vec<u8>) {
    (scale.name.clone(), scale.to_bytes())
}

/// The scale [`scale_parts`] wrote.
pub fn scale_from_parts(name: &str, bytes: &[u8]) -> Option<Arc<Scale>> {
    Scale::from_bytes(name, bytes)
}

impl Scale {
    /// The declaration's canonical bytes: the residue type of the reciprocal, and for an infinitesimal
    /// declared much smaller or much larger than another, a `1` and each of those two in turn — a `0`
    /// for none, or a `1`, its name and its own bytes. An infinitesimal declared on its own writes its
    /// residue type alone. A residue class's copy writes the declaration it refines.
    pub fn to_bytes(&self) -> Vec<u8> {
        let mut out = Vec::new();
        self.write_declaration(&mut out);
        out
    }

    fn write_declaration(&self, out: &mut Vec<u8>) {
        let scale = self.declaration();
        scale.residues.write(out);
        if scale.much_smaller_than.is_none() && scale.much_larger_than.is_none() {
            return;
        }
        out.push(1);
        for bound in [&scale.much_smaller_than, &scale.much_larger_than] {
            match bound {
                None => out.push(0),
                Some(b) => {
                    out.push(1);
                    crate::exact_codec::write_len(b.name.len(), out);
                    out.extend_from_slice(b.name.as_bytes());
                    let bytes = b.to_bytes();
                    crate::exact_codec::write_len(bytes.len(), out);
                    out.extend_from_slice(&bytes);
                }
            }
        }
    }

    /// The infinitesimal [`Scale::to_bytes`] wrote under `name`; `None` for a forged or non-canonical
    /// encoding, or a declaration its bounds refuse.
    pub fn from_bytes(name: &str, bytes: &[u8]) -> Option<Arc<Scale>> {
        Scale::read_declaration(name, bytes, 0)
    }

    fn read_declaration(name: &str, bytes: &[u8], depth: usize) -> Option<Arc<Scale>> {
        use crate::exact_codec::{read_byte, read_len, MAX_WIRE_DEPTH, MAX_WIRE_LEN};
        if depth > MAX_WIRE_DEPTH {
            return None;
        }
        let mut pos = 0;
        let residues = ResidueType::read(bytes, &mut pos)?;
        let scale = if pos == bytes.len() {
            Scale::new(name, residues)
        } else {
            if read_byte(bytes, &mut pos)? != 1 {
                return None;
            }
            let mut bounds = Vec::with_capacity(2);
            for _ in 0..2 {
                bounds.push(match read_byte(bytes, &mut pos)? {
                    0 => None,
                    1 => {
                        let n = read_len(bytes, &mut pos, MAX_WIRE_LEN)?;
                        let bound_name = std::str::from_utf8(bytes.get(pos..pos.checked_add(n)?)?).ok()?.to_string();
                        pos += n;
                        let n = read_len(bytes, &mut pos, MAX_WIRE_LEN)?;
                        let inner = bytes.get(pos..pos.checked_add(n)?)?;
                        pos += n;
                        Some(Scale::read_declaration(&bound_name, inner, depth + 1)?)
                    }
                    _ => return None,
                });
            }
            let smaller = bounds.pop().expect("two bounds");
            let larger = bounds.pop().expect("two bounds");
            if larger.is_none() && smaller.is_none() {
                return None;
            }
            Scale::ordered(name, residues, larger, smaller).ok()?
        };
        (pos == bytes.len() && scale.to_bytes() == bytes).then(|| Arc::new(scale))
    }
}

/// A hyperreal (`0`), infinite integer (`1`), germ (`2`), root of a hyperreal (`3`), exact value of
/// several infinitesimals (`4`), germ of several (`5`) or infinite integer of several (`6`) as its
/// scale and canonical bytes — the scale of
/// a value of several its smallest infinitesimal, the bytes naming every one it involves; `None` for any
/// other value, and for a germ holding a real built from a function a program defines.
pub fn scaled_bytes<V: TowerValue>(v: &V) -> Option<(u8, String, Vec<u8>, Vec<u8>)> {
    Some(match v.exact()? {
        ExactRef::Hyper(h) => {
            let (name, residues) = scale_parts(&h.scale);
            match &h.value {
                HyperForm::Rational(r) => (0, name, residues, r.to_bytes()),
                HyperForm::Puiseux(p) => (3, name, residues, p.to_bytes()),
                HyperForm::Germ(g) if g.is_transmissible() => (2, name, residues, g.to_bytes()),
                HyperForm::Germ(_) => return None,
                HyperForm::Multi(m) => (4, name, residues, m.to_bytes()),
                HyperForm::Integer(m) => (6, name, residues, m.to_bytes()),
                HyperForm::Nested(g) if g.is_transmissible() => (5, name, residues, g.to_bytes()),
                HyperForm::Nested(_) => return None,
            }
        }
        ExactRef::Natural(n) => {
            let (name, residues) = scale_parts(&n.scale);
            (1, name, residues, n.value.to_bytes())
        }
        _ => return None,
    })
}

/// The value [`scaled_bytes`] wrote; `None` for a forged or non-canonical encoding.
pub fn from_scaled_bytes<V: TowerValue>(kind: u8, name: &str, residues: &[u8], bytes: &[u8]) -> Option<V> {
    let scale = scale_from_parts(name, residues)?;
    let v: V = match kind {
        0 => from_hyper(Hyperreal::from_bytes(bytes)?, &scale),
        1 => from_natural(Hypernatural::from_bytes(bytes)?, &scale),
        2 => from_germ(Germ::from_bytes(bytes)?, &scale),
        3 => from_closed(Closed::Series(Puiseux::from_bytes(bytes)?), &scale),
        4 => from_multi(Multi::from_bytes(bytes)?),
        5 => from_nested(NestedGerm::from_bytes(bytes)?),
        6 => from_multi(Multi::from_bytes(bytes)?),
        _ => return None,
    };
    let canonical = scaled_bytes(&v)?;
    (canonical == (kind, name.to_string(), residues.to_vec(), bytes.to_vec())).then_some(v)
}

/// A residue-dependent value rebuilt from its scale, modulus and per-class values.
pub fn depends_from_parts<V: TowerValue>(
    name: &str,
    residues: &[u8],
    modulus: u64,
    branches: Vec<Option<V>>,
) -> Option<V> {
    let scale = scale_from_parts(name, residues)?;
    let raw = branches.into_iter().map(|b| b.map(Branch)).collect();
    let value = Depends::from_branches(scale.residues.clone(), modulus, raw)?;
    let built: V = from_depends(value.clone(), &scale);
    match depends_of(&built) {
        Some(d) if d.value == value => Some(built),
        _ => None,
    }
}

#[cfg(test)]
#[path = "../../logicaffeine_tests/unit/logicaffeine_base/tower/tests.rs"]
pub(crate) mod tests;