Arbitrary Length Relative Poisson Transfer

Abstract

Native marked departure counts and their relative Poisson comparison.

Theorem 1.1 (Actual forward independent pairs).

$$\forall M,q,s,k:Nat,0<M\Rightarrow \forall r:Real,\forall S:\mathrm{Support}(M,q),\forall m:\mathrm{Fin}(k)\to \mathrm{Fin}(M),\mathrm{injective}(m)\Rightarrow \forall zp,zm:\mathrm{Fin}(k)\to Complex,\mathrm{actualPairPGF}(r,S,m,zp,zm,s)={1+\mathrm{driftA}(r,S,m,zp,zm)}^s$$

Proof. Machine-checked in Lean as D5/S3/Estimation/TimeArrow/ArbitraryMarkedCountPoissonRelative.actual_marked_pair_pgf (✓ std3). ∎

Source. Repository-derived.

Commentary.

For M>0, arbitrary real r, any native support, any distinct marks and arbitrary complex tilts, the sum of complete independent-pair history masses times their count monomial is exactly (1+driftA)^s. This identity includes s=0 and zero tilts. Each factor retains the actual stationary adjacent-pair kernel.

Theorem 1.2 (Uniform native relative count estimate).

$$\forall kappa,Czero:Real,0<kappa<1\wedge 1\le Czero\Rightarrow \exists A:Real,\exists Mzero:Nat,\exists etazero:Real,0<A\wedge 1\le Mzero\wedge 0<etazero\wedge \forall M,q,s,k:Nat,\forall r:Real,Mzero\le M\wedge 1\le q<M\wedge 0<r\le 1-kappa\wedge \mathrm{compensation}(M,q,r)\le 1-kappa\wedge 1\le \frac{s}{2M}\wedge \frac{\frac{s}{2M}}{M}\le etazero\wedge (k=1\vee k=2)\Rightarrow \forall S:\mathrm{Support}(M,q),\forall m:\mathrm{Fin}(k)\to \mathrm{Fin}(M),\mathrm{injective}(m)\Rightarrow \forall n^{+},n^{-}:\mathrm{Fin}(k)\to Nat,(\forall j:\mathrm{Fin}(k),{n^{+}}_j\le Czero\frac{s}{2M}\wedge {n^{-}}_j\le Czero\frac{s}{2M})\Rightarrow \forall e:\mathrm{Experiment}(),|\frac{P(M,q,s,r,S,m,n^{+},n^{-},e)}{Q(M,q,s,r,S,m,n^{+},n^{-})}-1|\le \frac{A{\frac{s}{2M}}^{k+1}}{M}$$

Proof. Machine-checked in Lean as D5/S3/Estimation/TimeArrow/ArbitraryMarkedCountPoissonRelative.arbitrary_marked_count_poisson_relative (✓ std3). ∎

Source. Repository-derived.

Commentary.

The constants A, Mzero and etazero depend only on kappa and Czero. There are k = 1 or k = 2 distinct marked positive states m(j). S is a native support of cardinality q. The native compensation is c = rq/(M-q), with natural difference in the denominator. The experiment e ranges over the native pair and uniform-start path experiments.

In the displayed formula P is the sum of native history masses over all histories of T = s transitions at the real scale lambda = s/(2M) for which every marked positive and negative destination-parity count equals the prescribed natural count. Counts of zero are included. Each pair history has mass equal to the product of (2M)^(-1) transition(x,y); a path history has mass (2M)^(-1) times the product of its consecutive transition factors. The transition is (1+b(x) chi(y))/(2M), where chi is the destination parity.

Q is the product, over marked states and both destination parities, of exp(-mu) mu^n/n!. The means are muplus(j) = lambda(1+b(m(j)))/2 and muminus(j) = lambda(1-b(m(j)))/2. The profile b is r on the positive support, -c on its positive complement, and zero on negative states. P and Q use the same support and marked rows; no independent path-row model is used.

Positive radii (n+1)/mu extract both native and Poisson count coefficients from their generating functions on a product torus. The pair and path exponential estimates bound the integrated coefficient difference. A factorial estimate, including n = 0, gives the relative normalization.

References

• Truth anchor: D5/S3/Estimation/TimeArrow/ArbitraryMarkedCountPoissonRelative.actual_marked_pair_pgf
• Truth anchor: D5/S3/Estimation/TimeArrow/ArbitraryMarkedCountPoissonRelative.arbitrary_marked_count_poisson_relative
• Dependency: D5/S3/Estimation/TimeArrow/ActualMarkedPathPgfPoissonEnvelope
• Dependency: D5/S3/Estimation/TimeArrow/MarkedPoissonCoefficient