Primitive analytic bounds for the residual R-324 blocks

Paper §4.2 Step 3 successively reduces the nested residual blocks left after the two within-copy reductions. ResidualCollapse.lean proves that every such sparse block is fully paired and relatively primitive. This file connects those certificates to the actual Proposition 4.1 estimate:

• a sparse block is increasingly reindexed by Fin B.card;
• its restricted pairing is full and primitive after this reindexing;
• its cardinality is even, giving the canonical order q = B.card / 2;
• the resulting pairing belongs to primitiveFullPairings q;
• for nonnegative dominating inputs, its concrete ordinary and inserted integral terms satisfy the pointwise (4.3)--(4.4) majorants.

The final theorem is a term-level analytic bound obtained from the proved proposition41; it is not an R-324 output predicate and does not assume either branch of (3.24).

Increasing transport of a sparse paired block

def Anderson4D.orderedBlockPairing {n k : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B) (e : Fin k ≃o ↥B) : PartialPairing (Fin k)

Restrict a pairing to a closed sparse block and transport it along an increasing enumeration of that block.

Equations

• Anderson4D.orderedBlockPairing κ B hB e = (Anderson4D.PartialPairing.congr e.symm.toEquiv) (κ.restrictTo ⋯)

@[simp]

theorem Anderson4D.orderedBlockPairing_apply {n k : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B) (e : Fin k ≃o ↥B) (i : Fin k) : ↑(e ((orderedBlockPairing κ B hB e) i)) = κ ↑(e i)

theorem Anderson4D.orderedBlockPairing_isFull {n k : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B) (e : Fin k ≃o ↥B) : (orderedBlockPairing κ B hB e).IsFull

Closure and absence of fixed points are preserved by the increasing reindexing.

theorem Anderson4D.orderedBlockPairing_isPrimitive {n k : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B) (hprim : IsRelPrimitiveOn κ B) (e : Fin k ≃o ↥B) : IsPrimitive (orderedBlockPairing κ B hB e)

Relative primitivity on the sparse carrier becomes ordinary paper primitivity after increasing reindexing.

theorem Anderson4D.residualBlock_card_even {n : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B) : Even B.card

A fully paired sparse block has even cardinality.

def Anderson4D.residualBlockOrder {n : ℕ} (B : Finset (Fin n)) : ℕ

The perturbative order carried by a residual block.

Equations

• Anderson4D.residualBlockOrder B = B.card / 2

def Anderson4D.residualPrimitiveBlockOrderIso {n : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B) : Fin (2 * residualBlockOrder B) ≃o ↥B

Canonical increasing enumeration of an even residual block.

Equations

• Anderson4D.residualPrimitiveBlockOrderIso κ B hB = B.orderIsoOfFin ⋯

def Anderson4D.residualPrimitiveBlockPairing {n : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B) : PartialPairing (Fin (2 * residualBlockOrder B))

The canonical standard-index pairing carried by a residual block.

Equations

• Anderson4D.residualPrimitiveBlockPairing κ B hB = Anderson4D.orderedBlockPairing κ B hB (Anderson4D.residualPrimitiveBlockOrderIso κ B hB)

theorem Anderson4D.residualPrimitiveBlockPairing_mem {n : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B) (hprim : IsRelPrimitiveOn κ B) : residualPrimitiveBlockPairing κ B hB ∈ primitiveFullPairings (residualBlockOrder B)

A certified residual block is a genuine member of the primitive-pairing sum in Proposition 4.1 at its exact half-cardinality order.

Disjointness and the exact order ledger

theorem Anderson4D.mem_finsetUnionList_iff {α : Type u_1} [DecidableEq α] {x : α} (blocks : List (Finset α)) : x ∈ finsetUnionList blocks ↔ ∃ B ∈ blocks, x ∈ B

Membership in the union of a list of finite blocks.

theorem Anderson4D.residualIntervalTrace_disjoint_nestedResidualShells {n : ℕ} (active : Finset (Fin n)) (previous : Fin n × Fin n) (rest : List (Fin n × Fin n)) (hpair : List.Pairwise LaterCrossCutIntervalContains (previous :: rest)) (B : Finset (Fin n)) : B ∈ nestedResidualShells active previous rest → Disjoint (residualIntervalTrace active previous) B

The current trace is disjoint from every subsequent shell and from the final exterior.

theorem Anderson4D.nestedResidualShells_pairwise_disjoint {n : ℕ} (active : Finset (Fin n)) (previous : Fin n × Fin n) (rest : List (Fin n × Fin n)) (hpair : List.Pairwise LaterCrossCutIntervalContains (previous :: rest)) : List.Pairwise Disjoint (nestedResidualShells active previous rest)

Successive shells and the exterior of a nested interval chain are pairwise disjoint.

theorem Anderson4D.residualCollapseBlocks_pairwise_disjoint {n : ℕ} (active : Finset (Fin n)) (chain : List (Fin n × Fin n)) (hpair : List.Pairwise LaterCrossCutIntervalContains chain) : List.Pairwise Disjoint (residualCollapseBlocks active chain)

The trace/shell/exterior decomposition associated with a nested chain is pairwise disjoint.

theorem Anderson4D.card_finsetUnionList_eq_sum_card {α : Type u_1} [DecidableEq α] (blocks : List (Finset α)) (hdisjoint : List.Pairwise Disjoint blocks) : (finsetUnionList blocks).card = (List.map Finset.card blocks).sum

Pairwise-disjoint finite blocks have additive cardinality under finsetUnionList.

theorem Anderson4D.sum_card_momentResidualCollapseBlocks {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : (List.map Finset.card (momentResidualCollapseBlocks κp κm π)).sum = (momentResidualActive κp κm).card

Exact cardinality ledger for the concrete R-324 collapse blocks.

theorem Anderson4D.two_mul_sum_residualBlockOrder_eq_sum_card {n : ℕ} (blocks : List (Finset (Fin n))) (heven : List.Forall (fun (B : Finset (Fin n)) => Even B.card) blocks) : 2 * (List.map residualBlockOrder blocks).sum = (List.map Finset.card blocks).sum

For a list of even blocks, twice the sum of their half-cardinality orders is the sum of their cardinalities.

theorem Anderson4D.two_mul_sum_momentResidualBlockOrders {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) : 2 * (List.map residualBlockOrder (momentResidualCollapseBlocks κp κm π)).sum = (momentResidualActive κp κm).card

Exact perturbative-order ledger for the concrete residual collapse: the block orders add to half the number of residual variables.

Concrete primitive-pairing terms

noncomputable def Anderson4D.primitivePairingKernelTerm (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (κ : PartialPairing (Fin (2 * n))) (z w : T4) : ℝ

One ordinary primitive-pairing summand, including its exact coupling.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Anderson4D.primitivePairingKernelInsertedTerm (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (κ : PartialPairing (Fin (2 * n))) (z w : T4) : ℝ

One inserted primitive-pairing summand, including its exact coupling.

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.primitivePairingKernelTerm_nonneg (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)) (z : T4), 0 ≤ G j z) (κ : PartialPairing (Fin (2 * n))) (z w : T4) : 0 ≤ primitivePairingKernelTerm ρ lam ε n hn G κ z w

theorem Anderson4D.primitivePairingKernelInsertedTerm_nonneg (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)) (z : T4), 0 ≤ G j z) (κ : PartialPairing (Fin (2 * n))) (z w : T4) : 0 ≤ primitivePairingKernelInsertedTerm ρ lam ε n hn G κ z w

theorem Anderson4D.primitivePairingKernelTerm_le_kernel (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)) (z : T4), 0 ≤ G j z) (κ : PartialPairing (Fin (2 * n))) (hκ : κ ∈ primitiveFullPairings n) (z w : T4) : primitivePairingKernelTerm ρ lam ε n hn G κ z w ≤ primitiveKernel ρ lam ε n hn G z w

A nonnegative concrete primitive term is bounded by the complete primitive sum containing it.

theorem Anderson4D.primitivePairingKernelInsertedTerm_le_kernel (ρ : SmoothCutoff) (lam ε : ℝ) (n : ℕ) (hn : 1 ≤ n) (G : Fin (2 * n - 1) → T4 → ℝ) (hG : ∀ (j : Fin (2 * n - 1)) (z : T4), 0 ≤ G j z) (κ : PartialPairing (Fin (2 * n))) (hκ : κ ∈ primitiveFullPairings n) (z w : T4) : primitivePairingKernelInsertedTerm ρ lam ε n hn G κ z w ≤ primitiveKernelInserted ρ lam ε n hn G z w

Inserted counterpart of primitivePairingKernelTerm_le_kernel.

Proposition 4.1 applied to every certified residual block

theorem Anderson4D.exists_residualPrimitiveBlockPairing_term_bounds (ρ : SmoothCutoff) : ∃ (orderConstant : ℝ) (supportConstant : ℝ) (C : ℝ), 0 < orderConstant ∧ 0 < supportConstant ∧ 0 < C ∧ ∀ {n : ℕ} (κ : PartialPairing (Fin n)) (B : Finset (Fin n)) (hB : IsFullyPairedOn κ B), IsRelPrimitiveOn κ B → ∀ (lam ε : ℝ) (G : Fin (2 * residualBlockOrder B - 1) → T4 → ℝ) (hreg : PrimitiveEstimateRegime (residualBlockOrder B) lam ε orderConstant supportConstant C), IsAdmissiblePrimitiveInput (residualBlockOrder B) G → (∀ (j : Fin (2 * residualBlockOrder B - 1)) (z : T4), 0 ≤ G j z) → ∀ (z : T4), |primitivePairingKernelTerm ρ lam ε (residualBlockOrder B) ⋯ G (residualPrimitiveBlockPairing κ B hB) z 0| ≤ primitiveKernelMajorant C lam ε supportConstant (residualBlockOrder B) z ∧ |primitivePairingKernelInsertedTerm ρ lam ε (residualBlockOrder B) ⋯ G (residualPrimitiveBlockPairing κ B hB) z 0| ≤ primitiveInsertedMajorant C lam ε supportConstant (residualBlockOrder B) z

Every certified nonempty residual primitive block satisfies the actual ordinary and inserted Proposition 4.1 bounds, for its canonical transported pairing.

The constants are chosen once by the proved proposition41, before the ambient carrier, the block, the perturbative parameters, and the input kernels. The extra nonnegativity assumption is exactly the dominating |G_j| branch used after taking absolute values in (4.19)--(4.20).

Specialization to the canonical R-324 block list

theorem Anderson4D.momentResidualCollapseBlock_isFullyPairedOn_of_mem {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentResidualCollapseBlocks κp κm π) : IsFullyPairedOn (momentCombinedPairing κp κm π) B

Extract the closure certificate for a particular block in the canonical R-324 residual decomposition.

theorem Anderson4D.momentResidualCollapseBlock_isRelPrimitiveOn_of_mem {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hB : B ∈ momentResidualCollapseBlocks κp κm π) : IsRelPrimitiveOn (momentCombinedPairing κp κm π) B

Extract the relative-primitivity certificate for a particular block in the canonical R-324 residual decomposition.

theorem Anderson4D.exists_momentResidualCollapseBlock_term_bounds (ρ : SmoothCutoff) : ∃ (orderConstant : ℝ) (supportConstant : ℝ) (C : ℝ), 0 < orderConstant ∧ 0 < supportConstant ∧ 0 < C ∧ ∀ {m : ℕ} (κp κm : PartialPairing (Fin m)) (π : ↥κp.singles ≃ ↥κm.singles) (B : Finset (Fin (2 * m))) (hmem : B ∈ momentResidualCollapseBlocks κp κm π), have hB := ⋯; ∀ (lam ε : ℝ) (G : Fin (2 * residualBlockOrder B - 1) → T4 → ℝ) (hreg : PrimitiveEstimateRegime (residualBlockOrder B) lam ε orderConstant supportConstant C), IsAdmissiblePrimitiveInput (residualBlockOrder B) G → (∀ (j : Fin (2 * residualBlockOrder B - 1)) (z : T4), 0 ≤ G j z) → ∀ (z : T4), |primitivePairingKernelTerm ρ lam ε (residualBlockOrder B) ⋯ G (residualPrimitiveBlockPairing (momentCombinedPairing κp κm π) B hB) z 0| ≤ primitiveKernelMajorant C lam ε supportConstant (residualBlockOrder B) z ∧ |primitivePairingKernelInsertedTerm ρ lam ε (residualBlockOrder B) ⋯ G (residualPrimitiveBlockPairing (momentCombinedPairing κp κm π) B hB) z 0| ≤ primitiveInsertedMajorant C lam ε supportConstant (residualBlockOrder B) z

Every concrete block in momentResidualCollapseBlocks has the ordinary and inserted Proposition 4.1 term bounds after its canonical increasing reindexing.

This is the direct analytic consumer of the coverage/fullness/primitivity theorems in ResidualCollapse.lean. In particular, no MomentFiberReductionData or desired density domination is assumed.