Native One and Two Row Relative Poisson Transfer
Abstract
Native marked departure counts and their relative Poisson comparison.
Theorem 1.1 (Uniform native relative count estimate).
Proof. Machine-checked in Lean as D5/S3/Estimation/TimeArrow/ActualMarkedCountPoissonRelative.actual_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 = 2M lambda transitions 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.