lemmaroutine

Fixed point with factorial convergence

Correction fixed point

E_*

is unique; iterates converge factorially

fixes iteration count

k_*

for the residual bounds

Lemma·lem:hier-fixed-point·§4.1 Correction with a fixed column multiplier

Statement (paper)

For every fixed column multiplier

0\leq g\leq1

, there is a unique strictly forward nonnegative solution of

E_*(x,y)=fQ((C+E_*C)(x,y)/f)g(y).

For the recurrence in Equation ,

0\leq E_i\leq E_*

, and for every

k\geq0

\max_{x,y}\frac{E_*(x,y)-E_k(x,y)}f \leq e^{1/\theta_1}\frac{(L_Q/\theta_1)^k}{k!}.

In particular

k_*

can be chosen as a fixed integer so that the right side of Equation at

k=k_*

is at most

q^{-1}/32

, uniformly in

C,f,V

, and

g

In plain English

For each fixed column multiplier

0\leq g\leq1

, the equation

E_*=fQ((C+E_*C)/f)g

has a unique strictly forward nonnegative solution

E_*

. The recurrence iterates satisfy

0\leq E_i\leq E_*

, and

\max(E_*-E_k)/f\leq e^{1/\theta_1}(L_Q/\theta_1)^k/k!

, so a fixed

k_*

makes this at most

q^{-1}/32

uniformly in

C,f,V,g

Why it's here

This lemma shows that the iterative correction converges to a well-defined limit

E_*

at a factorial rate, with no contraction assumption. Uniformity in

C,f,V,g

lets later results, such as the residual bounds, use one fixed iteration count

k_*

. The proof combines forward ordering for existence and uniqueness, a row-support size bound, an entry bound, and a binomial count over the row supports for the factorial decay.

Classified routine:

A Picard-type iteration argument for a strictly forward (triangular, nilpotent-like) system: forward ordering gives existence and uniqueness, and Lipschitz bounds over ordered supports give the k!-rate, in the spirit of Volterra/Picard iteration estimates. It is a technical step in the correction scheme rather than the paper's central new idea.

Uses

Nothing else in the paper

Used by

lemResidual matrix D is bounded and dominating

Inside the proof

claimFixed point exists uniquely by forward orderingclaimResidual nonnegative with bounded row supportclaimEntry bound via increasing support sequencesclaimFactorial decay of iteration differences

Sources

PaperOpen

Section: §4.1 Correction with a fixed column multiplier
Page: —
Label: lem:hier-fixed-point
Line: sections/hierarchy.tex:82

Leannot aligned

Phase 2 aligns this node to a Lean declaration.