Paper §4.2, Step 3: absorbing the chain constant into the base

Paper: R-324 — §4.2 Step 3, the K^t absorption

exists_r324Step3_nestedChain_le delivers the nested-chain bound in the form (Cλ)^{2 Σ k_i} · K^t, with one factor of the elementary eight-dimensional constant K per removed interval. The shape the rest of §4.2 consumes — R324Step23ConfigReduction, and behind it the paper's own (Cλ)^{2m-2k} bookkeeping — carries no separate constant: every constant lives in the base of the power.

The two agree because each removed interval has at least one pair, so t ≤ Σ k_i, and one factor of max K 1 per removed site pays for one factor of K per removed interval. This is the same absorption r324RemovalStepConstant_le performs for the §4.1 iteration.

theorem Anderson4D.r324Step3_card_le_sum {t : ℕ} {ks : ℕ → ℕ} (hk : ∀ i < t, 1 ≤ ks i) : t ≤ ∑ i ∈ Finset.range t, ks i

Each removed interval contributes at least one to the site count, so the number of reductions never exceeds the total number of pairs removed.

theorem Anderson4D.r324Step3_absorb_chainConstant {C lam K : ℝ} {t : ℕ} {ks : ℕ → ℕ} (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hK : 0 ≤ K) (hk : ∀ i < t, 1 ≤ ks i) : (C * lam) ^ (2 * ∑ i ∈ Finset.range t, ks i) * K ^ t ≤ (C * max K 1 * lam) ^ (2 * ∑ i ∈ Finset.range t, ks i)

The chain constant is absorbed into the base.

(Cλ)^{2Σk_i}·K^t ≤ ((C·max K 1)·λ)^{2Σk_i}: one factor of max K 1 per removed site more than pays for one factor of K per removed interval.

theorem Anderson4D.r324Step3_chain_le_absorbed {C lam K M : ℝ} {t : ℕ} {ks : ℕ → ℕ} (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hK : 0 ≤ K) (hM : 0 ≤ M) (hk : ∀ i < t, 1 ≤ ks i) {E0 : ℝ} (hchain : E0 ≤ (C * lam) ^ (2 * ∑ i ∈ Finset.range t, ks i) * K ^ t * M) : E0 ≤ (C * max K 1 * lam) ^ (2 * ∑ i ∈ Finset.range t, ks i) * M

Step 3, in the constant-free shape §4.2 consumes.

The nested-chain bound with the elementary constant absorbed, ready to be read as the (Cλ)^{…} bookkeeping of R324Step23ConfigReduction.