Integrability carried through an R-324 within-half residual trace #
The exact residual transition needs integrability of the weighted local section almost everywhere in the post-head coordinates. Full current integrability supplies precisely that statement after the genuine head/post split.
It is important not to replace this by unweighted local integrability almost everywhere in the local endpoint parameter. The map from a post tuple to the predecessor-minus-successor point may be constant or otherwise degenerate (in particular when there are no post coordinates), so such an a.e. statement cannot in general be pulled back. The weighted formulation also handles a zero outer factor without dividing by it.
No global moment estimate is stored here. The state below contains only:
- the actual scale of every named edge;
- the corresponding off-diagonal edge certificate; and
- full integrability of the current physical residual integrand.
Integrability supplied by a slotwise edge certificate #
theorem
Anderson4D.R324WithinHalfEdgeCertificate.integrable_stepClosedIntegrand_section
{ρ : SmoothCutoff}
{ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{ctx : R324WithinHalfStepContext pairing}
{scale : Fin (m + 1) → ℝ}
(hcert : R324WithinHalfEdgeCertificate ctx.state scale)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2)))
(z w : T4)
:
MeasureTheory.Integrable
(fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges
(primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ z w v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)
Every closed primitive summand in one actual within-half head has an integrable internal section, pointwise in its two displayed endpoints.
theorem
Anderson4D.R324WithinHalfEdgeCertificate.eventually_integrable_stepClosedIntegrand_section
{ρ : SmoothCutoff}
{ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{ctx : R324WithinHalfStepContext pairing}
{scale : Fin (m + 1) → ℝ}
(hcert : R324WithinHalfEdgeCertificate ctx.state scale)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
:
∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))),
MeasureTheory.Integrable
(fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges
(primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ p.1 p.2 v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure)
Uniform-in-pairing endpoint form used by the local-collapse Fubini identity. The preceding theorem is pointwise, so the a.e. packaging costs nothing.
theorem
Anderson4D.R324WithinHalfStepContext.rawLocalSpatialIntegral_mul_complexOuter_eq_absorb_of_weighted
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(ctx : R324WithinHalfStepContext pairing)
(ρ : SmoothCutoff)
(lam ε : ℝ)
(u : T4)
(outer : ℂ)
(hweighted :
MeasureTheory.Integrable
(fun (t : Fin (2 * residualBlockOrder ctx.step.2) → T4) => ↑(ctx.rawLocalIntegrand ρ ε u t) * outer)
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure))
(hinternal :
∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder ctx.step.2))),
MeasureTheory.Integrable
(fun (v : Fin (2 * residualBlockOrder ctx.step.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder ctx.step.2) (↑κB) ctx.internalEdges
(primitiveAssemble (residualBlockOrder ctx.step.2) ⋯ p.1 p.2 v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2 - 2)) => paperMeasure))
:
(↑(lamEps lam ε) ^ (2 * residualBlockOrder ctx.step.2) * ∫ (t : Fin (2 * residualBlockOrder ctx.step.2) → T4), ↑(ctx.rawLocalIntegrand ρ ε u t) * outer ∂MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder ctx.step.2)) => paperMeasure) = ↑((ctx.absorb ρ lam ε).edges (r324WithinHalfPredecessorSlot ctx.state ctx.step) u) * outer
A weighted complex local section is sufficient for the exact processed collapse. On the zero-weight set both sides vanish; off that set, complex scalar cancellation recovers the real unweighted integrability premise of the existing local theorem.
Full residual integrability and one-step advance #
structure
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfResidualAnalyticState
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(x y : T4)
:
Physical analytic state carried at one literal within-half suffix.
- certificate : R324WithinHalfEdgeCertificate res.state self.scale
- full : MeasureTheory.Integrable (fun (w : res.SurvivingCoordinate → T4) => ↑(res.residualIntegrand ρ ε x y (res.reconstruct w))) (MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure)
Instances For
structure
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfResidualInternalReady
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(head : R322ExtractionStep m)
(tail : List (R322ExtractionStep m))
(hremaining : res.remaining = head :: tail)
:
Endpoint-independent analytic evidence for one within-half transition.
There is deliberately no full residual integrability and no unweighted
standard field here. The former belongs to the actual scalar integral
being transported, while the latter is recovered only off the zero set of
its genuine outer weight.
- internal : ∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))), MeasureTheory.Integrable (fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) => detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB) (res.headContext head tail hremaining).internalEdges (primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 w)) (MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure)
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.eventually_integrable_weightedHeadLocal_mul_postOuter_of_integrable
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(head : R322ExtractionStep m)
(tail : List (R322ExtractionStep m))
(hremaining : res.remaining = head :: tail)
(x y : T4)
(postOuter : ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ)
(hfull :
MeasureTheory.Integrable
(fun (w : res.SurvivingCoordinate → T4) =>
↑(res.residualIntegrand ρ ε x y (res.reconstruct w)) * postOuter ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) w).2)
(MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))
:
∀ᵐ (v :
(res.afterHead head tail hremaining).SurvivingCoordinate →
T4) ∂MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure, MeasureTheory.Integrable
(fun (t : Fin (2 * residualBlockOrder head.2) → T4) =>
↑((res.headContext head tail hremaining).rawLocalIntegrand ρ ε
(res.headPredecessorPoint head tail hremaining x y v - res.headSuccessorPoint head tail hremaining x y v)
t) * (↑(res.headOuterFactor head tail hremaining ρ ε x y v) * postOuter v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure)
Full integrability with an arbitrary post-coordinate outer function gives the exact weighted local sections at almost every post-head tuple.
The local weight is the product of the actual physical outer factor and the carried post-coordinate factor; neither is cancelled.
theorem
Anderson4D.R324WithinHalfResidualPrefix.eventually_integrable_weightedHeadLocal_of_integrable
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(head : R322ExtractionStep m)
(tail : List (R322ExtractionStep m))
(hremaining : res.remaining = head :: tail)
(x y : T4)
(hfull :
MeasureTheory.Integrable
(fun (w : res.SurvivingCoordinate → T4) => ↑(res.residualIntegrand ρ ε x y (res.reconstruct w)))
(MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))
:
∀ᵐ (v :
(res.afterHead head tail hremaining).SurvivingCoordinate →
T4) ∂MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure, MeasureTheory.Integrable
(fun (t : Fin (2 * residualBlockOrder head.2) → T4) =>
↑((res.headContext head tail hremaining).rawLocalIntegrand ρ ε
(res.headPredecessorPoint head tail hremaining x y v - res.headSuccessorPoint head tail hremaining x y v)
t) * ↑(res.headOuterFactor head tail hremaining ρ ε x y v))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2)) => paperMeasure)
Unweighted-current specialization of the preceding weighted-section theorem. This is useful for the optional scalar analytic-state corollary.
theorem
Anderson4D.R324WithinHalfResidualPrefix.lamEps_pow_integral_residual_mul_postOuter_eq_afterHead_of_weighted
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(head : R322ExtractionStep m)
(tail : List (R322ExtractionStep m))
(hremaining : res.remaining = head :: tail)
(x y : T4)
(postOuter : ((res.afterHead head tail hremaining).SurvivingCoordinate → T4) → ℂ)
(hfull :
MeasureTheory.Integrable
(fun (w : res.SurvivingCoordinate → T4) =>
↑(res.residualIntegrand ρ ε x y (res.reconstruct w)) * postOuter ((res.splitSurvivingPiMeasurableEquiv head tail hremaining) w).2)
(MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))
(hinternal :
∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))),
MeasureTheory.Integrable
(fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB)
(res.headContext head tail hremaining).internalEdges
(primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 w))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure))
:
(↑(lamEps lam ε) ^ (2 * res.remainingOrder) * ∫ (w : res.SurvivingCoordinate → T4), ↑(res.residualIntegrand ρ ε x y (res.reconstruct w)) * postOuter
((res.splitSurvivingPiMeasurableEquiv head tail hremaining)
w).2 ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ↑(lamEps lam ε) ^ (2 * (res.afterHead head tail hremaining).remainingOrder) * ∫ (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4), ↑((res.afterHead head tail hremaining).residualIntegrand ρ ε x y
((res.afterHead head tail hremaining).reconstruct v)) * postOuter
v ∂MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure
One exact head transition with an arbitrary post-coordinate complex outer factor, using only full weighted current integrability and the endpoint-independent internal certificate.
Its premise uses weighted current integrability instead of unweighted local integrability at every post tuple.
theorem
Anderson4D.R324WithinHalfResidualPrefix.integrable_residualIntegrand_afterHead
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(head : R322ExtractionStep m)
(tail : List (R322ExtractionStep m))
(hremaining : res.remaining = head :: tail)
(x y : T4)
(hfull :
MeasureTheory.Integrable
(fun (w : res.SurvivingCoordinate → T4) => ↑(res.residualIntegrand ρ ε x y (res.reconstruct w)))
(MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure))
(hinternal :
∀ᵐ (p : T4 × T4) ∂paperMeasure.prod paperMeasure, ∀ (κB : ↥(primitiveFullPairings (residualBlockOrder head.2))),
MeasureTheory.Integrable
(fun (w : Fin (2 * residualBlockOrder head.2 - 2) → T4) =>
detJclosedIntegrandWith ρ ε (2 * residualBlockOrder head.2) (↑κB)
(res.headContext head tail hremaining).internalEdges
(primitiveAssemble (residualBlockOrder head.2) ⋯ p.1 p.2 w))
(MeasureTheory.Measure.pi fun (x : Fin (2 * residualBlockOrder head.2 - 2)) => paperMeasure))
:
MeasureTheory.Integrable
(fun (v : (res.afterHead head tail hremaining).SurvivingCoordinate → T4) =>
↑((res.afterHead head tail hremaining).residualIntegrand ρ ε x y
((res.afterHead head tail hremaining).reconstruct v)))
(MeasureTheory.Measure.pi fun (x : (res.afterHead head tail hremaining).SurvivingCoordinate) => paperMeasure)
Full residual integrability is preserved by one literal head collapse.
The proof transports the current integrand through the actual measure-preserving head/post split, integrates the head section, and uses the already proved exact one-section transition.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfResidualAnalyticState.internalReady
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{res : R324WithinHalfResidualPrefix ρ lam ε pairing}
{x y : T4}
(state : res.R324WithinHalfResidualAnalyticState x y)
(head : R322ExtractionStep m)
(tail : List (R322ExtractionStep m))
(hremaining : res.remaining = head :: tail)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
:
res.R324WithinHalfResidualInternalReady head tail hremaining
Build the honest weighted ready evidence at one certified analytic state.
def
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfResidualAnalyticState.advance
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{res : R324WithinHalfResidualPrefix ρ lam ε pairing}
{x y : T4}
(state : res.R324WithinHalfResidualAnalyticState x y)
(head : R322ExtractionStep m)
(tail : List (R322ExtractionStep m))
(hremaining : res.remaining = head :: tail)
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(nextScale : Fin (m + 1) → ℝ)
(nextCertificate : R324WithinHalfEdgeCertificate (res.afterHead head tail hremaining).state nextScale)
:
(res.afterHead head tail hremaining).R324WithinHalfResidualAnalyticState x y
Advance a certified analytic state through one actual schedule head. The caller supplies only the genuine next edge certificate, normally produced by the local Proposition 4.1 certificate transport.
Equations
Instances For
Endpoint-independent certified analytic trace #
inductive
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
:
A data-valued analytic trace through the literal within-half suffix.
At a nonterminal node the trace stores exactly the internal Fubini evidence needed for the local primitive collapse and the certificate of the new edge state. Full weighted integrability is intentionally not stored: it depends on the endpoints and on the terminal outer functional, and is supplied to the exact iteration theorem below.
- terminal {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (scale : Fin (m + 1) → ℝ) (hremaining : res.remaining = []) (certificate : R324WithinHalfEdgeCertificate res.state scale) : res.R324WithinHalfCertifiedAnalyticTrace scale
- step {ρ : SmoothCutoff} {lam ε : ℝ} {m : ℕ} {pairing : PartialPairing (Fin m)} (res : R324WithinHalfResidualPrefix ρ lam ε pairing) (head : R322ExtractionStep m) (tail : List (R322ExtractionStep m)) (hremaining : res.remaining = head :: tail) (scale : Fin (m + 1) → ℝ) (internal : res.R324WithinHalfResidualInternalReady head tail hremaining) (nextScale : Fin (m + 1) → ℝ) (nextCertificate : R324WithinHalfEdgeCertificate (res.afterHead head tail hremaining).state nextScale) (next : (res.afterHead head tail hremaining).R324WithinHalfCertifiedAnalyticTrace nextScale) : res.R324WithinHalfCertifiedAnalyticTrace scale
Instances For
@[irreducible]
def
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.of_localBlockProvider
{ρ : SmoothCutoff}
{C lam ε K : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
(hε : 0 < ε)
(hε1 : ε ≤ 1)
(provider : R324WithinHalfLocalBlockProvider ρ C lam ε K pairing)
(res : R324WithinHalfResidualPrefix ρ lam ε pairing)
(scale : Fin (m + 1) → ℝ)
(certificate : R324WithinHalfEdgeCertificate res.state scale)
:
res.R324WithinHalfCertifiedAnalyticTrace scale
Structural recursion on the literal suffix turns the quantitative local provider into the endpoint-independent analytic trace.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminalPrefix
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{res : R324WithinHalfResidualPrefix ρ lam ε pairing}
{scale : Fin (m + 1) → ℝ}
(trace : res.R324WithinHalfCertifiedAnalyticTrace scale)
:
R324WithinHalfResidualPrefix ρ lam ε pairing
The literal terminal residual prefix reached by a certified trace.
Equations
- (Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminal res scale hremaining certificate).terminalPrefix = res
- (Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.step res head tail hremaining scale internal nextScale nextCertificate next).terminalPrefix = next.terminalPrefix
Instances For
def
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminalProjection
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{res : R324WithinHalfResidualPrefix ρ lam ε pairing}
{scale : Fin (m + 1) → ℝ}
(trace : res.R324WithinHalfCertifiedAnalyticTrace scale)
:
(res.SurvivingCoordinate → T4) → trace.terminalPrefix.SurvivingCoordinate → T4
Restrict a current surviving tuple through every genuine head/post split until it lies on the actual terminal carrier.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.WeightedIntegrableAlong
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{res : R324WithinHalfResidualPrefix ρ lam ε pairing}
{scale : Fin (m + 1) → ℝ}
(x y : T4)
(trace : res.R324WithinHalfCertifiedAnalyticTrace scale)
(outer : (trace.terminalPrefix.SurvivingCoordinate → T4) → ℂ)
:
Full weighted integrability at precisely the nonterminal scalar integrals traversed by the trace.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminalPrefix_remaining_eq_nil
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{res : R324WithinHalfResidualPrefix ρ lam ε pairing}
{scale : Fin (m + 1) → ℝ}
(trace : res.R324WithinHalfCertifiedAnalyticTrace scale)
:
The terminal prefix has the literal empty suffix.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.terminalPrefix_processed_eq_schedule
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{res : R324WithinHalfResidualPrefix ρ lam ε pairing}
{scale : Fin (m + 1) → ℝ}
(trace : res.R324WithinHalfCertifiedAnalyticTrace scale)
:
The terminal prefix has processed the complete analytic schedule.
theorem
Anderson4D.R324WithinHalfResidualPrefix.R324WithinHalfCertifiedAnalyticTrace.lamEps_pow_integral_mul_terminalOuter_eq_terminal
{ρ : SmoothCutoff}
{lam ε : ℝ}
{m : ℕ}
{pairing : PartialPairing (Fin m)}
{res : R324WithinHalfResidualPrefix ρ lam ε pairing}
{scale : Fin (m + 1) → ℝ}
(x y : T4)
(trace : res.R324WithinHalfCertifiedAnalyticTrace scale)
(outer : (trace.terminalPrefix.SurvivingCoordinate → T4) → ℂ)
(hweighted : WeightedIntegrableAlong x y trace outer)
:
(↑(lamEps lam ε) ^ (2 * res.remainingOrder) * ∫ (v : res.SurvivingCoordinate → T4), ↑(res.residualIntegrand ρ ε x y (res.reconstruct v)) * outer
(trace.terminalProjection v) ∂MeasureTheory.Measure.pi fun (x : res.SurvivingCoordinate) => paperMeasure) = ∫ (v : trace.terminalPrefix.SurvivingCoordinate → T4), ↑(trace.terminalPrefix.residualIntegrand ρ ε x y (trace.terminalPrefix.reconstruct v)) * outer v ∂MeasureTheory.Measure.pi fun (x : trace.terminalPrefix.SurvivingCoordinate) => paperMeasure
Exact weighted iteration through every certified head in the literal suffix.