Analytic iteration closure for R-322

Paper Section 4.1 replaces different chain edges by collapsed kernels carrying different normalization constants. A common normalization would raise the largest such constant to the number of surviving chain edges and would destroy the exact perturbative-order ledger. This file therefore first proves the heterogeneous scaling identity: one scale factor is extracted from each chain edge, and no scale is counted twice.

The resulting Proposition 4.1 interface is the terminal analytic operation in the successive interval reduction. The actual selector/Fubini routing is kept separate from this normalization ledger.

Heterogeneous scaling of primitive chain inputs

theorem Anderson4D.primitiveChainProduct_family_mul (n : ℕ) (hn : 1 ≤ n) (A : Fin (2 * n - 1) → ℝ) (G : Fin (2 * n - 1) → T4 → ℝ) (x : Fin (2 * n) → T4) : primitiveChainProduct n hn (fun (j : Fin (2 * n - 1)) (z : T4) => A j * G j z) x = (∏ j : Fin (2 * n - 1), A j) * primitiveChainProduct n hn G x

Multiplying the j-th primitive-chain input by its own scalar A j extracts exactly the product of the edge scalars.

theorem Anderson4D.primitiveIntegrand_family_mul (ρ : SmoothCutoff) (ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (A : Fin (2 * n - 1) → ℝ) (G : Fin (2 * n - 1) → T4 → ℝ) (κ : PartialPairing (Fin (2 * n))) (x : Fin (2 * n) → T4) : primitiveIntegrand ρ ε n hn (fun (j : Fin (2 * n - 1)) (z : T4) => A j * G j z) κ x = (∏ j : Fin (2 * n - 1), A j) * primitiveIntegrand ρ ε n hn G κ x

Heterogeneous edge scaling at the primitive-integrand level.

theorem Anderson4D.primitiveKernel_family_mul (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (A : Fin (2 * n - 1) → ℝ) (G : Fin (2 * n - 1) → T4 → ℝ) (z w : T4) : primitiveKernel ρ lam ε n hn (fun (j : Fin (2 * n - 1)) (u : T4) => A j * G j u) z w = (∏ j : Fin (2 * n - 1), A j) * primitiveKernel ρ lam ε n hn G z w

Heterogeneous edge scaling at the two-endpoint primitive-kernel level.

Exact edgewise normalization

theorem Anderson4D.mul_normalizedOffDiagonalRepresentative_eq {C : ℝ} (hC : 0 < C) (f : T4 → ℝ) {z : T4} (hz : z ≠ 0) : C * normalizedOffDiagonalRepresentative C f z = f z

Off the diagonal, an input is exactly its positive normalization constant times its normalized representative.

theorem Anderson4D.primitiveKernel_eq_prod_mul_normalizedFamily (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 2 ≤ n) (C : Fin (2 * n - 1) → ℝ) (hC : ∀ (j : Fin (2 * n - 1)), 0 < C j) (G : Fin (2 * n - 1) → T4 → ℝ) (z w : T4) : primitiveKernel ρ lam ε n ⋯ G z w = (∏ j : Fin (2 * n - 1), C j) * primitiveKernel ρ lam ε n ⋯ (fun (j : Fin (2 * n - 1)) => normalizedOffDiagonalRepresentative (C j) (G j)) z w

At primitive order at least two, an arbitrary positive normalization constant can be extracted independently from every chain edge.

The order restriction is exactly the one needed for the null-diagonal congruence: at order one there are no internal variables, so the endpoint diagonal must instead be handled by the explicit order-one theorem.

Terminal Proposition 4.1 with exact edge scales

theorem Anderson4D.primitiveKernelDiff_le_prod_edgeScales_mul_majorant (ρ : SmoothCutoff) {lam ε supportConstant primitiveConstant : ℝ} {n : ℕ} (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (Cedge : Fin (2 * n - 1) → ℝ) (hCedge : ∀ (j : Fin (2 * n - 1)), 0 < Cedge j) (hmem : ∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) (hbound : ∀ (j : Fin (2 * n - 1)) (z : T4), z ≠ 0 → |G j z| ≤ Cedge j * invSqKer z) (hprop : ∀ (H : Fin (2 * n - 1) → T4 → ℝ), IsAdmissiblePrimitiveInput n H → MemEClassT4 (primitiveKernelDiff ρ lam ε n ⋯ H) ∧ MemEClassT4 (primitiveKernelInsertedDiff ρ lam ε n ⋯ H) ∧ PrimitiveKernelBounds ρ lam ε n ⋯ H supportConstant primitiveConstant) (z : T4) : |primitiveKernelDiff ρ lam ε n ⋯ G z| ≤ (∏ j : Fin (2 * n - 1), Cedge j) * primitiveKernelMajorant primitiveConstant lam ε supportConstant n z

Proposition 4.1 applied after edgewise normalization.

Each surviving generalized chain edge contributes its own factor Cedge j exactly once. This is the terminal estimate needed after all proper primitive blocks in paper (4.13) have been removed.

theorem Anderson4D.exists_primitiveKernelDiff_le_prod_edgeScales_mul_majorant_at_truncation (ρ : SmoothCutoff) : ∃ (supportConstant : ℝ) (primitiveConstant : ℝ), 0 < supportConstant ∧ 0 < primitiveConstant ∧ ∀ (lam ε : ℝ) (n : ℕ) (hn : 2 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (Cedge : Fin (2 * n - 1) → ℝ), 0 < lam → 0 < ε → ε ≤ 1 → n ≤ truncOrder ε → (∀ (j : Fin (2 * n - 1)), 0 < Cedge j) → (∀ (j : Fin (2 * n - 1)), MemEClassT4 (G j)) → (∀ (j : Fin (2 * n - 1)) (z : T4), z ≠ 0 → |G j z| ≤ Cedge j * invSqKer z) → ∀ (z : T4), |primitiveKernelDiff ρ lam ε n ⋯ G z| ≤ (∏ j : Fin (2 * n - 1), Cedge j) * primitiveKernelMajorant primitiveConstant lam ε supportConstant n z

Direct truncation-range specialization of the preceding terminal estimate to the proved Proposition 4.1.

Exact perturbative ledger for collapsed edge histories

def Anderson4D.r322CollapsedEdgeScale (base K C lam : ℝ) (orders : List ℕ) : ℝ

Scale carried by one surviving chain edge after the primitive blocks in orders have successively been collapsed into that edge.

Equations

• Anderson4D.r322CollapsedEdgeScale base K C lam orders = base * K ^ orders.length * (C * lam) ^ (2 * orders.sum)

theorem Anderson4D.prod_r322CollapsedEdgeScale {ι : Type u_1} [Fintype ι] (base : ι → ℝ) (K C lam : ℝ) (orders : ι → List ℕ) : ∏ i : ι, r322CollapsedEdgeScale (base i) K C lam (orders i) = ((∏ i : ι, base i) * K ^ ∑ i : ι, (orders i).length) * (C * lam) ^ (2 * ∑ i : ι, (orders i).sum)

Multiplying all surviving edge scales counts each base edge and each removed primitive block exactly once.

theorem Anderson4D.pow_mul_primitiveKernelMajorant_eq_order_add (C lam ε supportConstant : ℝ) (removedOrder terminalOrder : ℕ) (z : T4) : (C * lam) ^ (2 * removedOrder) * primitiveKernelMajorant C lam ε supportConstant terminalOrder z = primitiveKernelMajorant C lam ε supportConstant (removedOrder + terminalOrder) z

A removed-order power combines exactly with the order power already present in the Proposition 4.1 majorant.

theorem Anderson4D.prod_r322CollapsedEdgeScale_mul_terminalMajorant {ι : Type u_1} [Fintype ι] (base : ι → ℝ) (K C lam ε supportConstant : ℝ) (orders : ι → List ℕ) (terminalOrder : ℕ) (z : T4) : (∏ i : ι, r322CollapsedEdgeScale (base i) K C lam (orders i)) * primitiveKernelMajorant C lam ε supportConstant terminalOrder z = ((∏ i : ι, base i) * K ^ ∑ i : ι, (orders i).length) * primitiveKernelMajorant C lam ε supportConstant (∑ i : ι, (orders i).sum + terminalOrder) z

Terminal ledger after all proper blocks have been routed into the surviving generalized chain edges. Apart from the base Green constants and one universal collapse constant per proper block, the perturbative powers combine to the sum of removed and terminal primitive orders.