"""Lean-compatible total Euclidean division, including negative/zero divisors.
For b != 0 the remainder is in [0,abs(b)); for b=0 the quotient is 0.
Julia div/% truncate toward zero and cannot be substituted for this interface.
"""
function ediv(a::Integer,b::Integer)
    a=BigInt(a); b=BigInt(b)
    b == 0 ? big(0) : sign(b)*fld(a,abs(b))
end
function emod(a::Integer,b::Integer)
    a=BigInt(a); b=BigInt(b)
    b == 0 ? a : mod(a,abs(b))
end
ledger_step(A::Integer,B::Integer,d::Integer) = ediv(BigInt(A)*BigInt(d),B)
ledger_remainder(A::Integer,B::Integer,d::Integer) = emod(BigInt(A)*BigInt(d),B)

function F(d::Integer)
    d >= 0 || throw(DomainError(d,"canonical F has natural-number domain"))
    fld(Q*BigInt(d),S)
end
function rho(d::Integer)
    d >= 0 || throw(DomainError(d,"canonical rho has natural-number domain"))
    mod(Q*BigInt(d),S)
end
function iterate_state(d::Integer,n::Integer)
    n >= 0 || throw(DomainError(n,"iteration depth must be nonnegative"))
    d >= 0 || throw(DomainError(d,"canonical state must be nonnegative"))
    x=BigInt(d)
    for _ in 1:n; x=F(x); end
    x
end
function extinction_thresholds(n::Integer)
    n >= 0 || throw(DomainError(n,"depth must be nonnegative"))
    ts=BigInt[1]
    for _ in 1:n; push!(ts,cld(S*last(ts),Q)); end
    ts
end

"""Terminal state and remainder vector in FORWARD order; no source restrictions on A or B."""
function encode(A::Integer,B::Integer,n::Integer,d::Integer)
    n >= 0 || throw(DomainError(n,"ledger length must be nonnegative"))
    A=BigInt(A); B=BigInt(B); x=BigInt(d); rs=BigInt[]
    for _ in 1:n
        push!(rs,ledger_remainder(A,B,x))
        x=ledger_step(A,B,x)
    end
    (terminal=x,remainders=rs)
end

"""Total Lean recovery function; consumes the forward-ordered list from the right.
For untrusted records use decode_checked, which validates every reverse step.
"""
function recover(A::Integer,B::Integer,t::Integer,rs::AbstractVector{<:Integer})
    A=BigInt(A);B=BigInt(B);x=BigInt(t)
    for r in Iterators.reverse(rs); x=ediv(B*x+BigInt(r),A); end
    x
end
function admissible(A::Integer,B::Integer,t::Integer,rs::AbstractVector{<:Integer})
    A=BigInt(A);B=BigInt(B);x=BigInt(t)
    for r0 in Iterators.reverse(rs)
        r=BigInt(r0); y=B*x+r
        0 <= r < B && emod(y,A) == 0 || return false
        x=ediv(y,A)
    end
    true
end
function decode_checked(A::Integer,B::Integer,t::Integer,rs::AbstractVector{<:Integer})
    A != 0 || throw(DomainError(A,"unique decoding requires A != 0"))
    B > 0 || throw(DomainError(B,"canonical remainder bounds require B > 0"))
    admissible(A,B,t,rs) || throw(ArgumentError("inadmissible ordered ledger"))
    recover(A,B,t,rs)
end

"""V(r::rs)=A^length(rs)*r+B*V(rs), exactly the Lean recursive polynomial."""
function ledger_value(A::Integer,B::Integer,rs::AbstractVector{<:Integer})
    A=BigInt(A);B=BigInt(B);v=big(0);power=big(1)
    for r in Iterators.reverse(rs)
        v=power*BigInt(r)+B*v
        power *= A
    end
    v
end
function seed_from_remainder(r::Integer)
    0 <= r < S && iseven(r) || throw(DomainError(r,"canonical remainder must be even and in [0,S)"))
    mod(MODULAR_INVERSE*div(BigInt(r),2),PERIOD)
end

# This is the scalar external coordinate interface from Interface.lean.
# No SRSD implementation, transport, carry API, or extension is introduced.
function scalar_encode_total(h::Union{Integer,Rational},y::Union{Integer,Rational})
    h=rational(h);y=rational(y)
    e=h == 0 ? big(0) : floor_rat(y/h)
    (integer=e,residual=y-h*e)
end
function scalar_encode(h::Union{Integer,Rational},y::Union{Integer,Rational})
    h=rational(h);y=rational(y)
    h > 0 || throw(DomainError(h,"canonical scalar interface requires h > 0"))
    scalar_encode_total(h,y)
end
scalar_decode(h::Union{Integer,Rational},e::Integer,r::Union{Integer,Rational}) = rational(h)*BigInt(e)+rational(r)
quantize(h::Union{Integer,Rational},y::Union{Integer,Rational}) = rational(h)*scalar_encode(h,y).integer
function rational_grid_step(h::Union{Integer,Rational},y::Union{Integer,Rational},r::Rat=q)
    quantize(h,r*rational(y))
end

"""On the certified domain only, compute the exact real-lambda grid successor.
The finite real-floor theorem justifies use of F; q is not substituted globally.
"""
function certified_lambda_grid_step(h::Union{Integer,Rational},y::Union{Integer,Rational})
    h=rational(h); y=rational(y)
    h > 0 || throw(DomainError(h,"grid scale must be positive"))
    d=y/h
    denominator(d) == 1 || throw(DomainError(y,"input is not on the retained grid"))
    0 <= numerator(d) < DOMAIN_SIZE || throw(DomainError(d,"outside certified domain"))
    h*F(numerator(d))
end