The within-half successive removal, carrying an outer factor #
Paper: R-324 — §4.2 Step 2(5) — removal inside (4.18), outer factor carried
Paper §4.2, Step 2(5): "we successively sum over the primitive pairings
κ_i (i ≥ 1) and remove each I_i, gaining a factor Cλ and
introducing new inputs H, exactly as in §4.1."
The §4.1 removal is already available at the level of one half as
R324WithinHalfResidualPrefix.residualValue_eq_afterHead and its list
iteration exists_terminal_residualValue_eq_of_provider. What Step 2
needs on top of §4.1 is that the removal takes place inside the
2m+4-fold integral (4.18): while the left half's blocks are integrated
out, the whole right half, the cross-copy covariances, and the four
endpoint characters are simply there, untouched.
This module supplies exactly that. The point that makes it work is structural, not analytic:
Definition 3.1's fully paired subintervals contain no singles. The cross-copy covariance factors are indexed by the singles. Hence every factor of (4.18) outside the current half's block is constant in the block's coordinates and passes through the block integral as a scalar.
Concretely R324OuterReadsOnly S Outer says the outer factor reads the
half's tuple only at the vertices of S; when S avoids the current
schedule block, r324Outer_reconstruct_split_eq shows the outer factor is
literally constant along the block coordinates, and the one-head
transition of R324WithinHalfResidualStep carries it through unchanged.
Outer factors that avoid the removed blocks #
Outer reads the within-half internal tuple only at the vertices of
S. In (4.18) the relevant S is the set of singles of the half's
pairing: those carry the cross-copy covariances, and nothing else in the
other half, in the endpoint characters, or in the cross factors looks at
this half's internal coordinates.
Equations
- Anderson4D.R324OuterReadsOnly S Outer = ∀ (u u' : Fin m → Anderson4D.T4), (∀ i ∈ S, u i = u' i) → Outer u = Outer u'
Instances For
A constant outer factor reads nothing.
Outside the current block the reconstruction does not see the block
coordinates. A vertex not in head.2 is either still active after the
absorb — in which case the split reads it from the post tuple — or was
already deleted, in which case both reconstructions return the junk value
0. Either way the value is independent of the block tuple t.
Forward form of the previous lemma: outside the current block the pre-step reconstruction already agrees with the post-step reconstruction of the split tuple.
The outer factor is constant along the block coordinates. This is the whole content of "the rest of (4.18) is untouched by the removal".
The residual value with an outer factor #
The complete residual value of one half, multiplied by an outer factor
that reads only surviving vertices. With Outer = 1 this is the
proved residualValue, complexified.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One removal of §4.1, performed inside (4.18).
The exact one-head transition of R324WithinHalfResidualStep, with an
arbitrary outer factor riding along. The outer factor is not integrated
and not estimated: by r324Outer_reconstruct_split_eq it is a scalar for
the block integral, so it commutes with the collapse.
Iteration through the whole schedule #
The paper removes all the fully paired subintervals of the half, one
after another. This is the same structural list recursion as the
proved exists_terminal_residualValue_eq_of_provider, now preserving
the outer factor at every step.
The evidence for one outer-carrying removal. base is the proved
Fubini/collapse evidence — the outer factor plays no part in it — avoid
is the structural fact that the removed block contains no vertex the outer
factor reads, and fullOuter is the joint integrability of the product
actually integrated.
- base : res.R324WithinHalfResidualStepReady head tail hremaining x y
- fullOuter : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => ↑(res.residualIntegrand ρ ε x y (res.reconstruct w)) * Outer (res.reconstruct w)) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)
Instances For
One packaged outer-carrying removal preserves the value.
Uniform provider of the outer-carrying step evidence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A proof-relevant exact trace through every remaining schedule block, carrying the outer factor.
- terminal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {S : Finset (Fin m)} {Outer : (Fin m → T4) → ℂ} {x y : T4} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (hremaining : res.remaining = []) : R324OuterIterationReady S Outer x y res
- step {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} {S : Finset (Fin m)} {Outer : (Fin m → T4) → ℂ} {x y : T4} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (ready : res.R324OuterStepReady head tail hremaining S Outer x y) (next : R324OuterIterationReady S Outer x y (res.afterHead head tail hremaining)) : R324OuterIterationReady S Outer x y res
Instances For
A uniform provider constructs the complete trace.
All the removals of one half, performed inside (4.18).
Iterating a ready trace reaches a genuine empty suffix — every fully paired subinterval of the half has been removed — and the residual value with its outer factor is preserved exactly. This is paper §4.2 Step 2(5) for one half: absolute values have not been taken, and the right half, the cross covariances, and the endpoint characters have not been touched.
Consumer-facing list iteration from one uniform provider.
Bridging an ambient outer factor to the proved certified trace #
R324WithinHalfResidualIntegrability already iterates the removal with an
outer factor — but one presented as a function of the terminal surviving
coordinates (lamEps_pow_integral_mul_terminalOuter_eq_terminal). In
(4.18) the outer factor is not given in that form: it is a function of the
ambient half tuple, namely the other half times the cross-copy covariances
times the endpoint characters.
The two presentations agree exactly when the outer factor avoids every
removed block, which is the structural fact R324OuterAvoidsSchedule
below — true for (4.18) because Definition 3.1's subintervals are fully
paired and the cross covariances are indexed by the singles.
No block of the analytic schedule meets S. For (4.18), with S the
singles of the half's pairing, this holds because every schedule block is
fully paired.
Equations
- Anderson4D.R324WithinHalfResidualPrefix.R324OuterAvoidsSchedule pairing S = ∀ step ∈ Anderson4D.r322AnalyticSchedule pairing, ∀ i ∈ S, i ∉ step.2
Instances For
The singles avoid every removed block.
Definition 3.1's fully paired subintervals contain no fixed point of the
pairing (IsFullyPairedOn asserts κ i ≠ i on the block). The outer
factor of (4.18) depends on this half only through the cross-copy
covariances, which are indexed by the singles; hence it never reads a
coordinate that a removal integrates out. This is the hypothesis that
makes the whole "remove inside the integral" step legitimate.
Any subset of the singles also avoids every removed block.
The ambient outer factor is the terminal outer factor.
Along any certified analytic trace, an outer factor reading only vertices
that no removed block contains takes the same value on the current tuple
and on its terminal projection. Consequently
fun w => Outer (trace.terminalPrefix.reconstruct w) is the
terminal-coordinate presentation required by
lamEps_pow_integral_mul_terminalOuter_eq_terminal.
All the removals of one half, inside (4.18), with the ambient outer factor.
This is paper §4.2 Step 2(5) for one half in the form Step 2 actually
needs: the value integrated is the half's residual integrand times the
ambient outer factor — the other half, the cross covariances, the
endpoint characters — and the conclusion is the same product on the
terminal carrier, where every fully paired subinterval of the half has
been removed and each removal has been replaced by the input H of
(4.13). No absolute value has been taken (Step 2(f)).
Step 2(5) for one half, under the paper's own hypothesis.
Specialization of the previous theorem in which the only requirement on the
outer factor is that it read this half's tuple at the singles — which is
exactly what the cross-copy covariances of (4.18) do, the other half and
the four endpoint characters not looking at this half's internal
coordinates at all. The block-avoidance side condition is then automatic
(r324OuterAvoidsSchedule_singles).