Paper §4.2, Steps 2--4 closed onto the frozen deterministic moment #
Paper: R-324 — §4.2 Steps 2(a)–(f) at one interval configuration
The (Cλ)^{2n} scaling of the integrated (4.4) majorant #
Step 2(a): the frozen moment as a sum over full pairings of [1,2m] #
The (4.18) term attached to a full pairing κ' of [1, 2m]: the
value of the 2m+4-fold integral at the unique contraction triple
(κ₊, κ₋, π) glued by momentCombinedPairing into κ'.
Equations
- Anderson4D.r324Step2FullTerm ρ ε m α β κ = Anderson4D.deterministicMomentContractionTerm ρ ε m α β ((Anderson4D.momentContractionEquivFullPairing m).symm κ)
Instances For
Step 2(a) in the abstract form of r324Step2_wick_regroup: a sum of
contraction terms is a sum over full pairings of [1, 2m].
Step 2(a), on the frozen moment. By Wick the (κ₊, κ₋, π) sum
defining deterministicMomentPairingSum is the sum over full pairings
κ' of [1, 2m].
Step 2(c) and 2(f): fix the positions, then take absolute values #
The set of full pairings whose Definition 3.1 interval configuration
is c. cfg is the Step 2(b) datum: the positions of the fully paired
subintervals extracted inside [1, m] and inside [m+1, 2m].
Equations
Instances For
The contribution of one fixed positional configuration to the frozen deterministic moment. No absolute value has been taken inside it: this is exactly the quantity (4.18) that Steps 2(d)–(e) and Step 3 reduce, and only the outer sum over configurations is estimated in modulus (Step 2(f)).
Equations
- Anderson4D.r324Step2ConfigSum ρ lam ε m α β cfg c = ↑(Anderson4D.lamEps lam ε) ^ (2 * m) * ∑ κ ∈ Anderson4D.r324Step2ConfigFibre cfg c, Anderson4D.r324Step2FullTerm ρ ε m α β κ
Instances For
Step 2(c) and 2(f), assembled. "We may fix the positions of
these subintervals at O(C^m) cost", and only after the removals do
we take absolute values. The positional count is the proved
card_intervalConfigs_two_mul_le, so the cost is 16^m.
Step 2(d)–(e): the successive removal, instantiated at [1, 2m] #
The paper removes the fully paired subintervals extracted inside [1, m]
and, independently, those extracted inside [m+1, 2m]. Definition 3.1's
subintervals never straddle the cut, so on a surviving chain slot of
Ĩ₀ = [1, 2m] \ ∪ I_i the two families simply concatenate.
The §4.1 iteration at the doubled carrier. One application of
exists_r324ReducedInput_admissible per surviving slot of Ĩ₀, fed with
the subintervals removed on that slot from either half. The surviving
inputs are the admissible H's of (4.13) and the gained factors multiply
to (Cλ)^{#removed} by Finset.prod_pow_eq_pow_sum.
Steps 2(d)–3: what the removal leaves, at one fixed configuration #
After the removals only a primitive pairing κ₀ on 2k sites survives,
carrying the new inputs H of (4.13); Step 3 integrates the four external
legs, reduces the nested chain by the elementary eight-dimensional
integral, and applies (4.4) one last time — leaving the single integral
∫ |J̃_{2k,prim}| of the surviving primitive kernel.
The one input Steps 2–3 take from the §4.1 iteration, at one fixed
positional configuration, in exactly the form R324Step1Reduction records
it for Step 1: V is the configuration's contribution to (4.18), the
schedules IsL, IsR are the fully paired subintervals removed inside
[1, m] and inside [m+1, 2m], they delete 2m - 2k sites in total, and
after the removal V is dominated by the gained factor times the integral
of the surviving primitive kernel J̃_{2k,prim} built from the H's.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Steps 2(d)–3 at one configuration, closed. The surviving inputs
are admissible (the doubled-carrier iteration), so Proposition 4.1 applies
to the surviving primitive pairing and (4.4) bounds the last integral by
the inserted majorant. Together with the (Cλ)^{2m-2k} gained by the
removals this is the per-configuration form of (4.19)–(4.20).
Steps 2--3 in the per-configuration shape the paper produces #
R324Step23Reduction (R324PaperStep23.lean) records the output of
Steps 2--3 with a single surviving order k. That is not what the
paper's Step 2 produces: the positional count fixes the interval
configuration first, and the surviving primitive pairing κ₀ — hence
its order k — depends on the configuration. This section restates the
hypothesis in that shape and shows that the paper's own arithmetic is
insensitive to the dependence: each configuration's bound
(Cλ)^{2m-2k} · ∫ J̃_{k,prim} ≤ (Cλ)^{2m-2k} · (Cλ)^{2k} · D/|log ε|
collapses to the k-free number (Cλ)^{2m} · D/|log ε|, so the
positional 16^m multiplies a single uniform bound exactly as in
Step 2(c).
The output of Steps 2(d)--3, per interval configuration.
cfg is the Step 2(b) datum assigning to each full pairing of [1,2m]
the positions of its Definition 3.1 fully paired subintervals inside
[1,m] and inside [m+1,2m]. For each configuration c the successive
removal deletes 2m - 2k sites, gains (Cλ)^{2m-2k}, and leaves the
single integral of the surviving primitive inserted kernel — with k
allowed to depend on c.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Steps 2 and 3 of §4.2, complete, in the per-configuration shape.
Same conclusion as exists_r324Step23_bound — the paper's
|E|P̂_m(α,β)|²| ≤ (Cλ)^{2m}|log ε|⁻¹ = λ_ε² · C (Cλ)^{2m-2},
i.e. (3.24) with 1 on the right — but consuming the honest
configuration-indexed output of the removal instead of a single global
surviving order. The proof is the paper's: bound each configuration by
the k-free number (Cλ)^{2m} D/|log ε| via (4.4), then pay the
positional count 16^m once.
The per-configuration hypothesis is exactly what
exists_r324Step23_fibre_bound produces once the physical bridge
supplies R324Step23FibreRemoval at each configuration: the fibre bound
already delivers the shape (Cλ)^{2m-2k} · ∫ J̃_{k,prim} with k
depending on the configuration.