claimroutine

Fixed point exists uniquely by forward ordering

Fixed point exists uniquely by forward ordering, with

E_i\le E_*

existence and monotone bound for the convergence estimate

Claim·§4.1 Correction with a fixed column multiplier·inside lemFixed point with factorial convergence

Statement (paper)

For every fixed column multiplier

0\leq g\leq1

, there is a unique strictly forward nonnegative solution

E_*

of Equation , without any contraction hypothesis. Moreover, for the recurrence in Equation ,

E_i\leq E_*

for all

i

, so the differences

E_*-E_k

are nonnegative.

In plain English

For any fixed column multiplier

0\leq g\leq1

, the fixed-point equation for

E_*

has exactly one strictly forward nonnegative solution, with no contraction assumption needed. The iterates

E_i

from the recurrence stay below it, so

E_*-E_k\geq0

for every

k

Why it's here

Because the equation is strictly forward, each entry of

E_*

is determined by entries earlier in the forward order, so the solution can be built and shown unique by ordering rather than by a contraction argument. The bound

E_i\leq E_*

makes the differences

E_*-E_k

nonnegative, which the later factorial convergence estimate and the residual claims need.

Classified routine:

Standard argument for strictly triangular (nilpotent) linear systems: entries are solved one at a time in the forward order, which gives existence and uniqueness, and monotone induction gives E_i ≤ E_* for the nonnegative iteration.

Uses

Nothing else in the paper

Used by

claimResidual nonnegative with bounded row support

Sources

PaperOpen

Section: §4.1 Correction with a fixed column multiplier
Page: —
Label: —
Line: sections/hierarchy.tex:103

Leannot aligned

Phase 2 aligns this node to a Lean declaration.