Strict Address Monotonicity

Abstract

A fixed point makes frozen escape probability strictly increase with positive address count.

Theorem 1.1 (A fixed point gives strict monotonicity in positive address count).

$$\forall Y,[\mathrm{Fintype}Y][\mathrm{Nonempty}Y],\forall f:Y\to Y,2\le \mathrm{card}\left(Y\right)\Rightarrow 0<\mathrm{card}\left(\mathrm{Fix}\left(f\right)\right)\Rightarrow \mathrm{StrictMonoOn}\left((A\mapsto \mathrm{escapeProbability}\left(\mathrm{Fin}\left(A\right),f\right)),\mathrm{Ici}\left(1\right)\right).$$

Proof. Machine-checked in Lean as D5/S0/Asymptotics/EscapeProbability/StrictAddressMonotonicity.escape_probability_strictMonoOn_of_has_fixed_point (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a finite nonempty output type Y with at least two elements, if f has at least one fixed point, then its frozen escape probability is strictly increasing as the positive address count grows.

The proof applies the public frozen closed form at consecutive address counts. A strict auxiliary ratio comparison uses the positive fixed-point count, and pinned Mathlib’s strictMonoOn_of_lt_succ promotes the successor inequality to strict monotonicity on Ici 1.

References

• Truth anchor: D5/S0/Asymptotics/EscapeProbability/StrictAddressMonotonicity.escape_probability_strictMonoOn_of_has_fixed_point
• Dependency: D5/S0/Asymptotics/EscapeProbability/PoissonDomainLimit
• Dependency: D5/S0/Asymptotics/EscapeProbabilityMonotone