Geometric & Compositional Ergodicity

Tools

`geometric_convergence`

Check if a process converges geometrically. Accepts either a sequence of observed values or a known contraction rate. Returns whether convergence is geometric (ratio < 1), the contraction rate r, expe...

`lyapunov_stability`

Construct and verify a Lyapunov function for a discrete dynamical system. Checks whether V decreases along every trajectory defined by the transition structure. Returns whether the system is Lyapunov ...

`envelope_convergence`

Check envelope convergence for a pipeline or iterative process. Verifies that upper and lower bounds are contracting toward each other and the value stays within the envelope. Returns convergence rate...

`compositional_ergodicity`

Check if composing two ergodic processes preserves ergodicity. Given contraction rates r_a and r_b, the composed rate is r_a * r_b. Returns composed contraction rate, whether the composition is ergodi...

`harris_recurrence`

Check Harris recurrence for a Markov chain. Determines irreducibility, positive recurrence, computes the stationary distribution (if it exists), and estimates mixing time. LEDGER section 10.

`thm_continuous_harris`

Foster-Lyapunov drift witness synthesis for continuous-state kernels over Polish spaces, extending beyond Fin (maxQueue + 1) types. Provides kernel structure, drift conditions, witness synthesis, and ...

`thm_geometric_ergodicity_discrete`

For a countable certified kernel with quantitative geometric envelope at an atom, the TV distance from any initial state to the stationary distribution decays geometrically: `TV(P^n(x, ·), π) ≤ M(x) ·...

`thm_geometric_ergodicity_rate`

The contraction rate `r` is bounded by `1 - stepEpsilon · smallSetEpsilon`, explicitly computable from the kernel certificate data. [LEDGER: THM-GEOMETRIC-ERGODICITY-RATE]

`thm_mixing_time_bound`

The ε-mixing time satisfies `t_mix(ε) ≤ (1/(1-r)) · log(M(x)/ε)`. For any target tolerance, there exists a finite step count at which TV distance drops below it. [LEDGER: THM-MIXING-TIME-BOUND]

`thm_continuous_ergodicity_lift`

For a ContinuousStateKernel with a discrete sub-lattice embedding, the discrete geometric rate lifts to the continuous kernel. Polish-space kernels inherit convergence rates from their discrete skelet...

`thm_parallel_ergodicity`

For two geometrically ergodic kernels `K₁(r₁)` and `K₂(r₂)`, the product kernel `K₁ ⊗ K₂` is geometrically ergodic with rate `r ≤ max(r₁, r₂)`. The slower stage dominates in parallel composition. [LED...

`thm_sequential_ergodicity`

For `K₂ ∘ K₁` (sequential composition), the composite is geometrically ergodic with rate `r ≤ r₁ · r₂`. Rates multiply under sequential composition — faster convergence than either stage alone. [LEDGE...

`thm_pipeline_mixing_bound`

An n-stage pipeline with per-stage rates has bounded mixing time. For sequential composition, `t_mix(ε) ≤ Σᵢ (1/(1-rᵢ)) · log(Mᵢ/ε)`. The pipeline converges to equilibrium in finite time. [LEDGER: THM...

`thm_pipeline_certificate`

Given per-stage `GeometricErgodicWitness` certificates, construct a pipeline-level certificate automatically. Per-stage stability certificates compose into pipeline-level certificates. [LEDGER: THM-PI...

`thm_ergodicity_monotone_in_stages`

Adding a geometrically ergodic stage to a sequential pipeline cannot worsen the per-step contraction rate. Since 0 < r_new < 1, the product rate is strictly smaller. [LEDGER: THM-ERGODICITY-MONOTONE-I...

`thm_syntactic_lyapunov_affine`

For an affine drift program with positive drift gap (serviceRate > arrivalRate), V(x) = x is a valid Lyapunov function. The drift gap equals serviceRate - arrivalRate, which is the spectral gap of the...

`thm_syntactic_small_set`

The set {x : x ≤ ventThreshold} is a valid small set for the affine kernel: finite, non-empty (contains state 0), bounded by maxState. The small-set fraction (ventThreshold+1)/(maxState+1) bounds the ...

`thm_syntactic_witness_sound`

The synthesized GeometricErgodicityRate (with stepEpsilon = driftGap/maxState, smallSetEpsilon = smallSetFraction) has a contraction rate r = 1 - ε₁·ε₂ that is provably in (0,1). The certificate match...

`thm_syntactic_witness_complete_affine`

For any affine drift program with positive drift gap, synthesis always succeeds: stepEpsilon > 0, smallSetFraction ∈ (0,1), so a GeometricErgodicityRate can always be constructed. Completeness for the...

`thm_syntactic_pipeline_lift`

Per-stage synthesized witnesses compose via THM-PIPELINE-CERTIFICATE into pipeline-level certificates automatically. The composite rate r₁·r₂ is sub-unit and strictly less than either individual rate....

`thm_nonlinear_lyapunov_quadratic`

For V(x) = x², the effective drift gap at state x is gap·(2x - gap), which grows linearly with x. Strictly positive for x > gap, and strictly exceeds the affine drift gap. Handles fluid backlog and th...

`thm_nonlinear_lyapunov_power`

V(x) = x^p for p ≥ 1 satisfies Foster drift: (x - gap)^p ≤ x^p for x ≥ gap. Monotonicity in the exponent: higher p gives larger effective drift gaps for states far from the small set. [LEDGER: THM-NON...

`thm_nonlinear_small_set_valid`

The level set {x ≤ T} from the affine program is also valid for nonlinear V(x) = x^p: finite, non-empty, bounded by maxState. [LEDGER: THM-NONLINEAR-SMALL-SET-VALID]

`thm_nonlinear_witness_sound`

The synthesized rate from nonlinear V inherits the affine synthesis parameters: stepEpsilon > 0, smallSetFraction ∈ (0,1). Nonlinear case can only improve the rate. [LEDGER: THM-NONLINEAR-WITNESS-SOUN...

`thm_nonlinear_dominates_affine`

Nonlinear V(x) = x² gives a tighter (smaller) contraction rate than affine V(x) = x: the quadratic drift term gap·(2x-gap) > gap for all x > gap. Larger effective spectral gap → faster convergence. [L...

`thm_adaptive_gradient_decomposition`

The gradient of service slack across network nodes defines valid drift weights: wᵢ = sᵢ/Σsⱼ ∈ [0,1], Σwᵢ = 1. All weights non-negative, normalized to sum to 1. [LEDGER: THM-ADAPTIVE-GRADIENT-DECOMPOSI...

`thm_adaptive_bottleneck_detection`

The minimum-slack node is the bottleneck: it is positive (stable) and lower-bounds all per-node slacks. [LEDGER: THM-ADAPTIVE-BOTTLENECK-DETECTION]

`thm_adaptive_reserve_coverage`

The gradient-weighted drift reserve = (Σsᵢ²)/(Σsᵢ) covers the drift gap. By QM-AM inequality, this exceeds the average slack and thus the minimum slack. [LEDGER: THM-ADAPTIVE-RESERVE-COVERAGE]

`thm_adaptive_decomposition_sound`

The gradient decomposition satisfies all AdaptiveCeilingDriftSynthesis obligations: non-negative normalized weights, positive total slack, positive bottleneck. [LEDGER: THM-ADAPTIVE-DECOMPOSITION-SOUN...

`thm_adaptive_dominates_uniform`

Gradient weights dominate uniform weights by Cauchy-Schwarz: n·Σsᵢ² ≥ (Σsᵢ)², so (Σsᵢ²)/(Σsᵢ) ≥ (Σsᵢ)/n = avg(sᵢ) = uniform reserve. [LEDGER: THM-ADAPTIVE-DOMINATES-UNIFORM]

`thm_envelope_contraction`

The throughputEnvelopeApprox ladder contracts: residual(n+1) = ρ · residual(n) where ρ = maxIncomingRoutingMass. The residual strictly decreases each step. [LEDGER: THM-ENVELOPE-CONTRACTION]

`thm_envelope_geometric_convergence`

The envelope ladder converges geometrically: \ [LEDGER: THM-ENVELOPE-GEOMETRIC-CONVERGENCE]

`thm_envelope_mixing_time`

For target accuracy ε > 0, the ladder reaches ε-accuracy in finite steps. The envelope-ladder analog of mixing_time_bound from GeometricErgodicity.lean. [LEDGER: THM-ENVELOPE-MIXING-TIME]

`thm_envelope_spectral_connection`

The contraction rate ρ bounds the spectral radius of the routing matrix P. The envelope iteration is the power method on the traffic equations. [LEDGER: THM-ENVELOPE-SPECTRAL-CONNECTION]

`thm_envelope_certificate_at_n`

At any step n where the envelope is below the service rate, the stability certificate is valid — early stopping is sound. As n grows, service slack increases monotonically, and eventually certificatio...