Realizable Escape Regimes

Abstract

Fixed finite output systems admit only the full-escape large-address regime.

Theorem 1.1 (The fixed-output escape regimes reduce to full escape).

$$\forall Y,[\mathrm{Fintype}Y][\mathrm{Nonempty}Y],\forall f:Y\to Y,n=\mathrm{card}\left(Y\right),k=\mathrm{card}\left(\mathrm{Fix}\left(f\right)\right),\left(\begin{array}{r}\left(k=0\Rightarrow \forall A\in \mathbb{N},\mathrm{escapeProbability}\left(\mathrm{Fin}\left(A\right),f\right)=1\right)\\ \wedge \mathrm{MonotoneOn}\left((A\mapsto \mathrm{escapeProbability}\left(\mathrm{Fin}\left(A\right),f\right)),\mathrm{Ici}\left(1\right)\right)\\ \wedge \left(\left(n\ge 2\wedge k>0\right)\Rightarrow \mathrm{StrictMonoOn}\left((A\mapsto \mathrm{escapeProbability}\left(\mathrm{Fin}\left(A\right),f\right)),\mathrm{Ici}\left(1\right)\right)\right)\\ \wedge \mathrm{escapeProbability}\left(\mathrm{Fin}\left(1\right),f\right)=1-\frac{k}{n}\\ \wedge \left(n\ge 2\Rightarrow \underset{A\to \infty }{\lim }\mathrm{escapeProbability}\left(\mathrm{Fin}\left(A\right),f\right)=1\right)\\ \wedge k\le n\\ \wedge \left(n\ge 2\Rightarrow \left(\begin{array}{r}\forall A\in \mathbb{N},0\le kA{n}^{-A}\le A{n}^{1-A}\le A{2}^{1-A}\\ \wedge \underset{A\to \infty }{\lim }kA{n}^{-A}=0\\ \wedge \forall \lambda \in \mathbb{R},\lambda >0\Rightarrow \neg \left(\underset{A\to \infty }{\lim }kA{n}^{-A}=\lambda \right)\end{array}\right)\right)\\ \wedge \left(n\ge 2\Rightarrow \left(\forall c\in \mathbb{R},0<c<1\Rightarrow \exists A_0\in \mathbb{N},\forall A\in \mathbb{N},A_0\le A\Rightarrow k\ne c{n}^A\right)\right)\end{array}\right).$$

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

Source. Repository-derived.

Commentary.

Let Y be a finite nonempty output alphabet, let f map Y to itself, write n for the size of Y and k for the number of fixed points. If k is zero, every address count has escape probability one. On positive address counts the probability is nondecreasing, and at one address it is one minus k divided by n. When n is at least two, the probability is strictly increasing if k is positive and tends to one as the address count grows.

The same theorem records the unconditional model constraint k at most n. When n is at least two, the scaled weight k A n to the minus A lies between zero and the two stated geometric envelopes, tends to zero, and therefore cannot tend to a positive lambda. Under that same size condition, every density c strictly between zero and one has a finite threshold beyond which k cannot equal c n to the A.

The proof applies the repository’s exact closed-form, monotonicity, strict-monotonicity, fixed-output limit, geometric-decay, and positive-density exclusion theorems. Pinned Mathlib and Loogle contain no theorem combining these clauses; Mathlib’s Fintype.card_subtype_le supplies the structural count bound. The conjunction preserves every mathematical clause of the named corollary, including its positive-address guard.

References

• Truth anchor: D5/S0/Asymptotics/EscapeProbability/EscapeRegimeCorollary.escape_probability_realizable_regimes
• Dependency: D5/S0/Asymptotics/DensePhaseUnrealizable
• Dependency: D5/S0/Asymptotics/EscapeProbability/FixedOutputLimit
• Dependency: D5/S0/Asymptotics/EscapeProbability/PoissonDomainLimit
• Dependency: D5/S0/Asymptotics/EscapeProbability/StrictAddressMonotonicity
• Dependency: D5/S0/Asymptotics/EscapeProbabilityMonotone
• Dependency: D5/S0/Asymptotics/PoissonWeightDecay