Honest finite assembly for the fixed-class inner sum

This file supplies the finite-sum layer between the local copy estimate in SingleScaleBridge and the parity bookkeeping in paper (5.87)--(5.92). The carrier is the paper's labeled-copy carrier

Σ l : HeppLeaf t, Fin (leafMultiplicity mu l).

Conditioning on copies already used by a partial permutation is represented by deleting a finite set from each (N,X) fiber. The resulting one- and two-variable sums are proved to be sub-sums of the unrestricted copy sums; no independence or product-separability of the two edge kernels is assumed.

The last section isolates the purely numerical parity ledger: one parity can lose at most twenty gains, the two parity exceptional sets have union of cardinality at most forty, and geometric-mean interpolation changes the gain exponent from 1/8 to 1/16.

Labeled copies and conditioned local choices

@[reducible, inline]

abbrev Anderson4D.XYCluster.HeppLabeledCopy {t : PlaneTree} (mu : t.Multiplicities) : Type

The distinct copies of all leaves. This is the codomain of a labeled arrangement in the factorial ledger.

Equations

• Anderson4D.XYCluster.HeppLabeledCopy mu = ((l : Anderson4D.HeppLeaf t) × Fin (Anderson4D.leafMultiplicity mu l))

def Anderson4D.XYCluster.labeledCopyPoint {t : PlaneTree} {mu : t.Multiplicities} (z : HeppLeaf t → Fin 4 → ℤ) (c : HeppLabeledCopy mu) : Fin 4 → ℤ

The lattice point carried by a labeled copy.

Equations

• Anderson4D.XYCluster.labeledCopyPoint z c = z c.fst

def Anderson4D.XYCluster.labeledCopiesAtNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) : Finset (HeppLabeledCopy mu)

All labeled copies whose leaf lies in the fixed (N,X) fiber a.

Equations

• Anderson4D.XYCluster.labeledCopiesAtNX Nm mu a = {c : Anderson4D.XYCluster.HeppLabeledCopy mu | Anderson4D.singleScaleSigma1 Nm mu c.fst = a}

def Anderson4D.XYCluster.conditionedCopiesAtNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (used : Finset (HeppLabeledCopy mu)) (a : NXClass) : Finset (HeppLabeledCopy mu)

Copies in a fixed fiber which have not occurred in the already exposed part of a labeled permutation.

Equations

• Anderson4D.XYCluster.conditionedCopiesAtNX Nm mu used a = Anderson4D.XYCluster.labeledCopiesAtNX Nm mu a \ used

theorem Anderson4D.XYCluster.conditionedCopiesAtNX_subset {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (used : Finset (HeppLabeledCopy mu)) (a : NXClass) : conditionedCopiesAtNX Nm mu used a ⊆ labeledCopiesAtNX Nm mu a

theorem Anderson4D.XYCluster.mem_labeledCopiesAtNX_iff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (a : NXClass) (c : HeppLabeledCopy mu) : c ∈ labeledCopiesAtNX Nm mu a ↔ singleScaleSigma1 Nm mu c.fst = a

theorem Anderson4D.XYCluster.mem_conditionedCopiesAtNX_iff {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (used : Finset (HeppLabeledCopy mu)) (a : NXClass) (c : HeppLabeledCopy mu) : c ∈ conditionedCopiesAtNX Nm mu used a ↔ singleScaleSigma1 Nm mu c.fst = a ∧ c ∉ used

Link to the factorial-ledger arrangement carrier

def Anderson4D.XYCluster.arrangementUsedCopies {t : PlaneTree} {mu : t.Multiplicities} {M : ℕ} (σ : Fin M ≃ HeppLabeledCopy mu) (J : Finset (Fin M)) : Finset (HeppLabeledCopy mu)

Copies occupying a finite set of positions in a labeled arrangement.

Equations

• Anderson4D.XYCluster.arrangementUsedCopies σ J = Finset.image (⇑σ) J

theorem Anderson4D.XYCluster.arrangement_copy_not_mem_used {t : PlaneTree} {mu : t.Multiplicities} {M : ℕ} (σ : Fin M ≃ HeppLabeledCopy mu) (J : Finset (Fin M)) {j : Fin M} (hj : j ∉ J) : σ j ∉ arrangementUsedCopies σ J

theorem Anderson4D.XYCluster.arrangement_copy_mem_conditionedNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {M : ℕ} (σ : Fin M ≃ HeppLabeledCopy mu) (J : Finset (Fin M)) {j : Fin M} (hj : j ∉ J) (a : NXClass) (ha : singleScaleSigma1 Nm mu (σ j).fst = a) : σ j ∈ conditionedCopiesAtNX Nm mu (arrangementUsedCopies σ J) a

A position not yet exposed by the backward summation is one of the conditioned local choices in its fixed (N,X) class.

theorem Anderson4D.XYCluster.arrangement_inducedWord_valid {t : PlaneTree} (mu : t.Multiplicities) {M : ℕ} (σ : Fin M ≃ HeppLabeledCopy mu) : inducedWord (leafMultiplicity mu) σ ∈ validWords (leafMultiplicity mu)

The induced leaf word of every labeled arrangement is an admissible word in the factorial ledger. This records that the local carrier above does not introduce a different notion of "valid word".

theorem Anderson4D.XYCluster.arrangement_pair_mem_conditionedNX {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) {M : ℕ} (σ : Fin M ≃ HeppLabeledCopy mu) (J : Finset (Fin M)) {j k : Fin M} (hj : j ∉ J) (hk : k ∉ J) (hjk : j ≠ k) (a b : NXClass) (ha : singleScaleSigma1 Nm mu (σ j).fst = a) (hb : singleScaleSigma1 Nm mu (σ k).fst = b) : σ j ∈ conditionedCopiesAtNX Nm mu (arrangementUsedCopies σ J) a ∧ σ k ∈ conditionedCopiesAtNX Nm mu (insert (σ j) (arrangementUsedCopies σ J)) b

Two distinct, not-yet-exposed positions give a legal conditioned pair: the second choice sees both the previously used positions and the first new copy. This is the exact local selection made in a labeled permutation.

theorem Anderson4D.XYCluster.sum_labeledCopiesAtNX_eq_nxCopyWeightedSum {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (a : NXClass) (f : (Fin 4 → ℤ) → ℝ) : ∑ c ∈ labeledCopiesAtNX Nm mu a, f (labeledCopyPoint z c) = nxCopyWeightedSum Nm mu z a f

A sum over all labeled copies in a fiber is exactly the multiplicity weighted leaf sum used by nxCopyWeightedSum.

theorem Anderson4D.XYCluster.sum_conditionedCopiesAtNX_le_nxCopyWeightedSum {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (used : Finset (HeppLabeledCopy mu)) (a : NXClass) (f : (Fin 4 → ℤ) → ℝ) (hf : ∀ c ∈ labeledCopiesAtNX Nm mu a, 0 ≤ f (labeledCopyPoint z c)) : ∑ c ∈ conditionedCopiesAtNX Nm mu used a, f (labeledCopyPoint z c) ≤ nxCopyWeightedSum Nm mu z a f

Dropping already-used copies only decreases a nonnegative local sum.

A conditioned two-variable block

noncomputable def Anderson4D.XYCluster.conditionedNXPairSum {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) {a b : NXClass} (ha : a ∈ nxCarrier Nm mu) (hb : b ∈ nxCarrier Nm mu) (used : Finset (HeppLabeledCopy mu)) (skipA skipB : Bool) (u : Fin 4 → ℤ) : ℝ

The honest conditional local sum for two consecutive positions of a labeled permutation. The second copy is selected after inserting the first one into used, so the two positions can never reuse the same labeled copy. The first copy may nevertheless have the same underlying leaf as the second when the incoming edge is skipped, exactly as in Proposition 5.10.

Equations

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

theorem Anderson4D.XYCluster.conditionedNXPairSum_le_nxCoupledCopyPairSum {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) {a b : NXClass} (ha : a ∈ nxCarrier Nm mu) (hb : b ∈ nxCarrier Nm mu) (used : Finset (HeppLabeledCopy mu)) (skipA skipB : Bool) (u : Fin 4 → ℤ) : conditionedNXPairSum ht hroot Nm mu z hz R ha hb used skipA skipB u ≤ nxCoupledCopyPairSum ht hroot Nm mu z hz R ha hb skipA skipB u

Forgetting both the used-copy condition and the inequality between the two labeled copies enlarges the conditional block to the unrestricted copy-level sum from SingleScaleBridge.

A conditioned one-variable block

noncomputable def Anderson4D.XYCluster.conditionedNXSingleSum {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) (used : Finset (HeppLabeledCopy mu)) (skipped : Bool) (u : Fin 4 → ℤ) : ℝ

The honest conditional local sum for a position that cannot be paired in the chosen parity.

Equations

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

noncomputable def Anderson4D.XYCluster.paperDyadicSingleRoughTarget {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℝ) (a : NXClass) (skipped : Bool) : ℝ

The exact dyadic right-hand factor in the one-variable estimate (5.92), before a universal comparison constant.

Equations

• Anderson4D.XYCluster.paperDyadicSingleRoughTarget Nm mu R a skipped = ↑a.2 * Anderson4D.XYCluster.paperDyadicY Nm mu a * if skipped = true then R⁻¹ ^ 2 else (↑a.1)⁻¹ ^ 2

theorem Anderson4D.XYCluster.paperDyadicSingleRoughTarget_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℝ) (a : NXClass) (skipped : Bool) : 0 ≤ paperDyadicSingleRoughTarget Nm mu R a skipped

theorem Anderson4D.XYCluster.conditionedNXSingleSum_le_sixteen_mul_target {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) {a : NXClass} (ha : a ∈ nxCarrier Nm mu) (used : Finset (HeppLabeledCopy mu)) (skipped : Bool) (u : Fin 4 → ℤ) : conditionedNXSingleSum ht hroot Nm mu z hz R ha used skipped u ≤ 16 * paperDyadicSingleRoughTarget Nm mu R a skipped

Copy-level, conditioned version of the one-variable rough estimate (5.92). The explicit constant 16 audits the two copies-to-points loss, the dyadic cardinality loss, and the use of the separation scale N/2.

The rough two-variable block (5.90)

noncomputable def Anderson4D.XYCluster.paperDyadicPairRoughTarget {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℝ) (a b : NXClass) (skipA skipB : Bool) : ℝ

The dyadic target in (5.90) is the product of its two one-variable (5.92) factors.

Equations

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

theorem Anderson4D.XYCluster.paperDyadicPairRoughTarget_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℝ) (a b : NXClass) (skipA skipB : Bool) : 0 ≤ paperDyadicPairRoughTarget Nm mu R a b skipA skipB

theorem Anderson4D.XYCluster.conditionedNXPairSum_le_256_mul_roughTarget {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) {a b : NXClass} (ha : a ∈ nxCarrier Nm mu) (hb : b ∈ nxCarrier Nm mu) (used : Finset (HeppLabeledCopy mu)) (skipA skipB : Bool) (u : Fin 4 → ℤ) : conditionedNXPairSum ht hroot Nm mu z hz R ha hb used skipA skipB u ≤ 256 * paperDyadicPairRoughTarget Nm mu R a b skipA skipB

Conditioned copy-level form of the rough pair estimate (5.90). It is obtained by two honest one-variable eliminations, hence the audited constant 16² = 256.

Backward elimination of a whole parity

structure Anderson4D.XYCluster.NXPairBlock {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Type

Two consecutive positions eliminated together. skipLeft refers to the edge from the already fixed point into left; skipRight refers to the edge between the two positions.

• left : ActiveNXClass Nm mu
• right : ActiveNXClass Nm mu
• skipLeft : Bool
• skipRight : Bool

noncomputable def Anderson4D.XYCluster.nxPairBlockTarget {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (p : NXPairBlock Nm mu) : ℝ

The exact paper dyadic target attached to a paired elimination block.

Equations

• Anderson4D.XYCluster.nxPairBlockTarget Nm mu p = Anderson4D.XYCluster.paperDyadicPairTarget Nm mu (↑p.left) (↑p.right) p.skipLeft p.skipRight

theorem Anderson4D.XYCluster.nxPairBlockTarget_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (p : NXPairBlock Nm mu) : 0 ≤ nxPairBlockTarget Nm mu p

noncomputable def Anderson4D.XYCluster.conditionedNXPairChainSum {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) : List (NXPairBlock Nm mu) → Finset (HeppLabeledCopy mu) → (Fin 4 → ℤ) → ℝ

The actual nested finite sum obtained by eliminating consecutive pairs from left to right. used is threaded through the recursion, so choices in different blocks are also distinct. The endpoint of a block becomes the fixed preceding point for the next block; this is the finite Fubini step behind the paper's instruction to sum in decreasing position order.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.conditionedNXPairChainSum ht hroot Nm mu z hz R [] x✝¹ x✝ = 1

theorem Anderson4D.XYCluster.conditionedNXPairChainSum_nonneg {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (ps : List (NXPairBlock Nm mu)) (used : Finset (HeppLabeledCopy mu)) (u : Fin 4 → ℤ) : 0 ≤ conditionedNXPairChainSum ht hroot Nm mu z hz R ps used u

theorem Anderson4D.XYCluster.conditionedNXPairChainSum_le_targetProduct : ∃ (C : ℝ), 0 < C ∧ ∀ {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℕ), accumulatedScale Nm mu t.rootV ≤ R → ∀ (ps : List (NXPairBlock Nm mu)) (used : Finset (HeppLabeledCopy mu)) (u : Fin 4 → ℤ), conditionedNXPairChainSum ht hroot Nm mu z hz (↑R) ps used u ≤ (List.map (fun (p : NXPairBlock Nm mu) => C * nxPairBlockTarget Nm mu p) ps).prod

One-parity fixed-class assembly. The sum is over honest distinct labeled-copy choices and is nested in the elimination order. Every local bound is the uniform copy-level (5.91) theorem; induction, rather than an assumed factorization, yields the product of dyadic targets.

One- and two-variable blocks in the same parity

inductive Anderson4D.XYCluster.NXParityBlock {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) : Type

The elimination schedule for one parity. Interior positions occur in pair blocks; parity endpoints and the split around the minimal-scale position occur in single blocks.

• single {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (a : ActiveNXClass Nm mu) (skipped : Bool) : NXParityBlock Nm mu
• pair {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (p : NXPairBlock Nm mu) : NXParityBlock Nm mu
• roughPair {t : PlaneTree} {Nm : t.HeppMarking} {mu : t.Multiplicities} (p : NXPairBlock Nm mu) : NXParityBlock Nm mu

noncomputable def Anderson4D.XYCluster.nxParityBlockTarget {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℝ) : NXParityBlock Nm mu → ℝ

Local target for a mixed one-parity schedule.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.nxParityBlockTarget Nm mu R (Anderson4D.XYCluster.NXParityBlock.single a skipped) = Anderson4D.XYCluster.paperDyadicSingleRoughTarget Nm mu R (↑a) skipped
• Anderson4D.XYCluster.nxParityBlockTarget Nm mu R (Anderson4D.XYCluster.NXParityBlock.pair p) = Anderson4D.XYCluster.nxPairBlockTarget Nm mu p

theorem Anderson4D.XYCluster.nxParityBlockTarget_nonneg {t : PlaneTree} (Nm : t.HeppMarking) (mu : t.Multiplicities) (R : ℝ) (p : NXParityBlock Nm mu) : 0 ≤ nxParityBlockTarget Nm mu R p

noncomputable def Anderson4D.XYCluster.conditionedNXParityChainSum {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) : List (NXParityBlock Nm mu) → Finset (HeppLabeledCopy mu) → (Fin 4 → ℤ) → ℝ

Honest nested sum for an arbitrary schedule of single and paired eliminations. As above, the used-copy set is threaded through every choice.

Equations

• One or more equations did not get rendered due to their size.
• Anderson4D.XYCluster.conditionedNXParityChainSum ht hroot Nm mu z hz R [] x✝¹ x✝ = 1

theorem Anderson4D.XYCluster.conditionedNXParityChainSum_nonneg {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℝ) (ps : List (NXParityBlock Nm mu)) (used : Finset (HeppLabeledCopy mu)) (u : Fin 4 → ℤ) : 0 ≤ conditionedNXParityChainSum ht hroot Nm mu z hz R ps used u

theorem Anderson4D.XYCluster.conditionedNXParityChainSum_le_targetProduct : ∃ (C : ℝ), 256 ≤ C ∧ ∀ {t : PlaneTree} (ht : t.isValid = true) (hroot : t.rootV ∈ t.BranchNodes) (Nm : t.HeppMarking) (mu : t.Multiplicities) (z : HeppLeaf t → Fin 4 → ℤ) (hz : IsSeparatedEmbedding Nm z) (R : ℕ), accumulatedScale Nm mu t.rootV ≤ R → ∀ (ps : List (NXParityBlock Nm mu)) (used : Finset (HeppLabeledCopy mu)) (u : Fin 4 → ℤ), conditionedNXParityChainSum ht hroot Nm mu z hz (↑R) ps used u ≤ (List.map (fun (p : NXParityBlock Nm mu) => C * nxParityBlockTarget Nm mu (↑R) p) ps).prod

Mixed one-parity assembly. This is the paper-facing finite elimination theorem for a fixed class sequence: it allows the at most four one-variable boundary blocks (5.92) and all two-variable blocks (5.91) in one nested sum. The universal constant is outside every schedule and every conditioning set.

The twenty/forty-exception parity ledger

structure Anderson4D.XYCluster.ParityExceptionLedger (κ : Type u_1) (ι : Type u_2) [DecidableEq ι] : Type (max u_1 u_2)

A conservative explicit certificate for the gains spoiled by the rough and one-variable local estimates in one parity. Six interior operations may touch three neighboring gains each and one boundary operation may touch two, which is the paper's 6 · 3 + 1 · 2 = 20 audit.

• interiorOps : Finset κ
• boundaryOps : Finset κ
• affected : κ → Finset ι
• interior_card : self.interiorOps.card ≤ 6
• boundary_card : self.boundaryOps.card ≤ 1
• affected_interior (k : κ) : k ∈ self.interiorOps → (self.affected k).card ≤ 3
• affected_boundary (k : κ) : k ∈ self.boundaryOps → (self.affected k).card ≤ 2

def Anderson4D.XYCluster.ParityExceptionLedger.exceptions {κ : Type u_1} {ι : Type u_2} [DecidableEq ι] (d : ParityExceptionLedger κ ι) : Finset ι

All gains discarded by the certified exceptional local operations.

Equations

• d.exceptions = d.interiorOps.biUnion d.affected ∪ d.boundaryOps.biUnion d.affected

theorem Anderson4D.XYCluster.ParityExceptionLedger.card_exceptions_le_twenty {κ : Type u_1} {ι : Type u_2} [DecidableEq ι] (d : ParityExceptionLedger κ ι) : d.exceptions.card ≤ 20

One parity discards at most twenty gains, with the constant obtained from the explicit local-operation ledger rather than assumed as a field.

theorem Anderson4D.XYCluster.two_parity_exception_union_card_le_forty {ι : Type u_1} [DecidableEq ι] (evenExceptional oddExceptional : Finset ι) (he : evenExceptional.card ≤ 20) (ho : oddExceptional.card ≤ 20) : (evenExceptional ∪ oddExceptional).card ≤ 40

Combining the even and odd exceptional ledgers loses at most forty gain indices.

Interpolation changes 1/8 to 1/16

noncomputable def Anderson4D.XYCluster.ratioGain (θ r : ℝ) : ℝ

A generic ratio gain, used only for the interpolation identity.

Equations

• Anderson4D.XYCluster.ratioGain θ r = min 1 (r ^ θ)

theorem Anderson4D.XYCluster.ratioGain_nonneg (θ : ℝ) {r : ℝ} (hr : 0 ≤ r) : 0 ≤ ratioGain θ r

theorem Anderson4D.XYCluster.sqrt_ratioGain_eighth {r : ℝ} (hr : 0 ≤ r) : √(ratioGain (1 / 8) r) = ratioGain (1 / 16) r

Pointwise interpolation identity underlying the sentence after (5.87): the square root of a 1/8 gain is the corresponding 1/16 gain.

theorem Anderson4D.XYCluster.sqrt_prod_ratioGain_eighth {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (ratio : ι → ℝ) (hratio : ∀ i ∈ s, 0 ≤ ratio i) : √(∏ i ∈ s, ratioGain (1 / 8) (ratio i)) = ∏ i ∈ s, ratioGain (1 / 16) (ratio i)

Square root commutes with the retained finite product of 1/8 gains, turning every retained factor into exponent 1/16.

theorem Anderson4D.XYCluster.parity_retained_union {ι : Type u_1} [DecidableEq ι] (blocks even odd evenExceptional oddExceptional : Finset ι) (hparts : even ∪ odd = blocks) (hdisj : Disjoint even odd) (he : evenExceptional ⊆ even) (ho : oddExceptional ⊆ odd) : even \ evenExceptional ∪ odd \ oddExceptional = blocks \ (evenExceptional ∪ oddExceptional)

The retained even and odd index sets join to the complement of the union of their exceptions.

theorem Anderson4D.XYCluster.sqrt_even_mul_odd_gain_eq_sixteenth {ι : Type u_1} [DecidableEq ι] (blocks even odd evenExceptional oddExceptional : Finset ι) (hparts : even ∪ odd = blocks) (hdisj : Disjoint even odd) (he : evenExceptional ⊆ even) (ho : oddExceptional ⊆ odd) (ratio : ι → ℝ) (hratio : ∀ i ∈ blocks, 0 ≤ ratio i) : √((∏ i ∈ even \ evenExceptional, ratioGain (1 / 8) (ratio i)) * ∏ i ∈ odd \ oddExceptional, ratioGain (1 / 8) (ratio i)) = ∏ i ∈ blocks \ (evenExceptional ∪ oddExceptional), ratioGain (1 / 16) (ratio i)

Exact product form of even/odd interpolation after deleting their two exceptional sets. Together with the following geometric-mean lemma this is the formal content of the paper's transition from at most twenty exceptions per parity to at most forty exceptions and exponent 1/16.

theorem Anderson4D.XYCluster.le_geometricMean_of_le_both {x a b : ℝ} (hx : 0 ≤ x) (ha : 0 ≤ a) (_hb : 0 ≤ b) (hxa : x ≤ a) (hxb : x ≤ b) : x ≤ √(a * b)

If a nonnegative quantity satisfies the even and odd estimates, it is bounded by their geometric mean. This lemma performs the interpolation rather than assuming it as an opaque global summation step.

Remaining statement-boundary obligations for the literal (5.87)

The analytic and finite-Fubini parts are closed above. The following position-level bookkeeping is intentionally not hidden in a hypothesis here:

• construct, from Fin m, the split at the minimal-scale position and the even/odd NXParityBlock schedules, proving at most four single blocks;
• select at most three skipped-edge blocks as roughPair and prove that their explicit (N/R)² factors give (N_root/R)^(min (2s) 3);
• map those single/rough blocks to a concrete ParityExceptionLedger, and discharge its 6 interior plus 1 boundary operation bounds;
• compare the heterogeneous single/roughPair targets with the common refined target in (5.87), paying the explicit Y^(1/2) and Ξ⁻¹ losses, proving that at most twenty such factors occur and absorbing the resulting m^20 into a universal exponential;
• supply the mirrored elimination theorem on the left of the minimal-scale anchor (or an equivalent reversal argument), including the reversed ratio gain, the shared used set, and the anchor/cross-side distinct-copy bookkeeping;
• identify the arrangement sum after fixing the (N,X) word with the corresponding conditioned chain, then reinsert R^(2s) and the factorial ledger at the statement boundary.

Thus no theorem in this file is named as Proposition 5.10 or as (5.87) itself; the declarations above are the strict, reusable middle layer needed to close that final position-level assembly.