LocalizationActualBackground

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: the actual-carrier background of the localization split

Source displays in ABK26:

• e.homs.defs together with the two sentences, which say that each diagonal block of bfAhom_m is a scalar matrix;
• e.recurrence.P.def, P = bfAhom_{m-h}^{-1/2}(e'; e);
• e.def.w, the two correctors w_{D,e}^{(K)} in H^1_0(cu_K) and w_{N,e'}^{(K)} in H^1(cu_K);
• e.Pz.def and e.Fz.def;
• the X_z display, whose affine background is

  bfAhom_{m-h}^{-1/2} ( e' + grad w_{D,e}^{(K)};
  e  + grad w_{N,e'}^{(K)} + shom_{m-h}^{-1} h e' );
  

PrincipalResponsePz.lean already carries P_z (principalPz) and F_z (principalFz) as functions of the two correctors. This module puts them on the doubled-field carrier the localization selection/gluing layer consumes, and derives -- never assumes -- the membership facts that layer left as caller propositions.

What is proved

• linearH1OfDomain / potentialFieldOn_const -- a constant field is the gradient of x |-> p . x, hence lies in Lpot(U).
• principalLoadField, with potentialFieldOn_smul and solenoidalFieldOn_smul -- the splitting question: bfAhom_{m-h}^{-1/2} acts as a positive real scalar on each leg separately, and both Chapter-1 field spaces are closed under a real scalar, so L^2_{pot,0} x Lsolo and Lpot x Lsol are each mapped into themselves. See "The bfAhom splitting question" below.
• localizationFz -- e.Fz.def on the DoubledField d carrier, per-sample omega explicit.
• localizationBackground -- the affine background of the X_z display on the same carrier, and localizationBackground_eq_constantDoubledField_principalPz_add_localizationFz, which is the identity P_z + bfF_z behind.
• solenoidalZeroNormalTraceFieldOn_neumannFluxField -- derived: the flux leg grad w_N + shom^{-1} h e' lies in Lsolo(cu_K). This is the second half of the manuscript's "Since." clause, and it is exactly the weak Neumann formulation of e.def.w read through the mean-zero gauge.
• isDoubledMuAdmissible_localizationBackground -- the actual-source hG, derived: the background lies in P + L^2_{pot,0}(cu_K) x Lsolo(cu_K).
• memVectorL2_localizationFz_potential / ..._flux -- the actual-source hFpot/hFflux, derived on every subcube.
• isDoubledAmbientField_localizationFz -- bfF_z in Lpot x Lsol on a localization cell, derived; this is the hF of LocalizationSelectionVariation.lean.

The bfAhom splitting question, resolved

The manuscript's clause names the two memberships grad w_D in L^2_{pot,0}(cu_K) and grad w_N + shom^{-1} h e' in Lsolo(cu_K) for the unnormalized pair, and then asserts the membership of the glued field in P + L^2_{pot,0}(cu_K) x Lsolo(cu_K) for the pair after applying bfAhom_{m-h}^{-1/2}. The step needs bfAhom_{m-h}^{-1/2} to preserve the product splitting L^2_{pot,0} x Lsolo.

A general symmetric positive block matrix does not, and block-diagonality alone is not enough either. Two independent obstructions:

• off-diagonal blocks mix the legs, and B v for a solenoidal v is in general not a gradient;
• even for a constant block-diagonal diag(A, D) with A symmetric positive but not scalar the potential leg fails. Minimal counterexample: d = 2, A = diag(1,2), u(x) = x_1 x_2, so grad u = (x_2, x_1) and A grad u = (x_2, 2 x_1), whose curl is 2 - 1 = 1 != 0; hence A grad u is not a gradient at all. The flux leg fails symmetrically: div(D g) = sum_{i,j} D_{ij} d_i g_j need not vanish when div g = 0 unless D is scalar.

So the sentence really does require a structural fact about bfAhom_{m-h}, and only scalarity of the diagonal blocks suffices.

The manuscript supplies the missing structural fact itself, and it is stronger than block-diagonality: by e.homs.defs and the hypercube symmetry sentences around it, bfAhom_m = diag(shom_m, shom_m^{-1}) with shom_m a positive scalar matrix. Hence bfAhom_{m-h}^{-1/2} acts on a pair as (u; v) |-> (shom^{-1/2} u; shom^{1/2} v), i.e. by a positive real scalar on each leg separately, and both Chapter-1 field spaces are closed under multiplication by a real scalar. principalLoadField is that action, written at the repository's already proved annealedLimitBlockInvSqrt, whose defining Ch02.blockDiag (shom^{-1/2}. 1) (shom^{1/2}. 1) is the scalar block diagonal of e.homs.defs; the closure of the two field spaces under a real scalar is potentialFieldOn_smul and solenoidalFieldOn_smul, and the step is taken in exactly that form inside isDoubledMuAdmissible_localizationBackground.

The only observation worth recording is presentational and is filed below as a declared divergence: the manuscript's "Since." clause names the memberships before the normalization is applied, so a reader must supply the scalarity of shom_{m-h} to complete the sentence.

Divergences from the printed statement

• Presentational. The membership clause is stated for the unnormalized pair; the normalization bfAhom_{m-h}^{-1/2} is what actually has to preserve the class. It does, by the scalarity of shom_{m-h}, which the sentence does not cite. This is a gap in the printed justification only, not in the result; no tex change is proposed beyond citing e.homs.defs.
• The Neumann gauge. H^1(cu_K) of e.def.w is normalized here by the mean-zero gauge H1MeanZeroFunction, exactly as in the already proved FreshShellExistence.lean; the gauge does not change the gradient, and solenoidalZeroNormalTraceFieldOn_neumannFluxField tests against all of H^1(cu_K) by passing to the mean-zero representative of the test function.
• The conormal boundary condition. n . (grad w_N + shom^{-1} h e') = 0 on d cu_K is the natural boundary condition of the weak formulation, so Lsolo membership is the weak formulation itself and not an extra input.
• . No localization scale and no buffer constant occurs below; the localization cube enters only as a free TriadicCube argument.
• Pin drift, reported not fixed. Corrector/FreshShellExistence.lean cites e.def.w as "". The mathematical content cited is unchanged and that module is not edited here.

Constant fields are gradients

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.linearH1OfDomain {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (p : HCPolySupport.Vec d) : HCPolySupport.H1Function U.carrier

The linear function x |-> p . x as an H^1 function on a Chapter-2 domain, assembled from the coordinate projections. Unconditional.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.linearH1OfDomain U p = ∑ i : Fin d, p i • HCPolySupport.H1Function.coordOnIsSobolevRegularDomain ⋯ i

@[simp]

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.linearH1OfDomain_grad {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (p : HCPolySupport.Vec d) : (linearH1OfDomain U p).grad = fun (x : HCPolySupport.Vec d) => p

The gradient of x |-> p . x is the constant field p. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.potentialFieldOn_const {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (p : HCPolySupport.Vec d) : HCPolySupport.Book.Ch01.PotentialFieldOn U.carrier fun (x : HCPolySupport.Vec d) => p

A constant field lies in Lpot(U). Unconditional.

Scalar multiples and differences of the Chapter-1 field spaces

The two zero-trace halves are already proved in the Section 2.4 path lane as Algsuperdiff.Section24.Sensitivity.Provider.Path.potentialZeroTraceFieldOn_smul and ..._solenoidalZeroNormalTraceFieldOn_smul, and are reused rather than restated. Only the two ambient halves, which that lane does not carry, are proved here.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.potentialFieldOn_smul {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (c : ℝ) (hf : HCPolySupport.Book.Ch01.PotentialFieldOn U f) : HCPolySupport.Book.Ch01.PotentialFieldOn U fun (x : HCPolySupport.Vec d) => c • f x

Lpot(U) is closed under real scalar multiplication. Conditional helper A: on the caller proposition hf (membership of f in Lpot(U)).

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.potentialFieldOn_sub {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.Book.Ch01.PotentialFieldOn U f) (hg : HCPolySupport.Book.Ch01.PotentialFieldOn U g) : HCPolySupport.Book.Ch01.PotentialFieldOn U fun (x : HCPolySupport.Vec d) => f x - g x

Lpot(U) is closed under differences. Conditional helper A: on the caller propositions hf, hg (membership of both fields in Lpot(U)).

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.solenoidalFieldOn_sub {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.Book.Ch01.SolenoidalFieldOn U f) (hg : HCPolySupport.Book.Ch01.SolenoidalFieldOn U g) : HCPolySupport.Book.Ch01.SolenoidalFieldOn U fun (x : HCPolySupport.Vec d) => f x - g x

Lsol(U) is closed under differences. Conditional helper A: on the caller propositions hf, hg (membership of both fields in Lsol(U)).

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.solenoidalFieldOn_smul {d : ℕ} {U : Set (HCPolySupport.Vec d)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (c : ℝ) (hg : HCPolySupport.Book.Ch01.SolenoidalFieldOn U g) : HCPolySupport.Book.Ch01.SolenoidalFieldOn U fun (x : HCPolySupport.Vec d) => c • g x

Lsol(U) is closed under real scalar multiplication. Conditional helper A: on the caller proposition hg (membership of g in Lsol(U)).

bfAhom^{-1/2} on a doubled field

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.principalLoadField {d : ℕ} (sigma : Observable.PositiveScalar) (X : HCPolySupport.Book.Ch02.DoubledField d) : HCPolySupport.Book.Ch02.DoubledField d

bfAhom^{-1/2} applied pointwise to a doubled field. By e.homs.defs and the scalarity sentences, the matrix is the scalar block diagonal diag(shom^{-1/2}, shom^{1/2}), so its action is a positive real scalar on each leg, i.e. the pointwise block action of annealedLimitBlockInvSqrt. Unconditional.

Equations

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

Restricting the ambient field spaces to a subdomain

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.solenoidalFieldOn_of_solenoidalZeroNormalTraceFieldOn_subset {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (hVopen : IsOpen V) (hVU : V ⊆ U) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U g) : HCPolySupport.Book.Ch01.SolenoidalFieldOn V g

A field with zero normal trace on U is solenoidal on every open subset V of U: an H^1_0(V) test function extends by zero to an H^1_0(U) one with gradient 1_V grad phi. Conditional helper A: on the caller propositions hU/hVopen/hVU (openness and inclusion of the subdomain) and hg (zero-normal-trace membership of g on U).

bfF_z and the background of the X_z display, on the doubled carrier

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.localizationFz {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : HCPolySupport.Book.Ch02.DoubledField d

e.Fz.def on Chapter 2's doubled-field carrier. The sample point omega is explicit: the flux leg carries the fresh shell h = k_{highScale} - k_{lowScale} of that sample through Corrector.streamForcing, so localizationFz is a genuinely per-sample field. The two components are PrincipalResponsePz.principalFz, so this is a repackaging of the already proved transcription and not a second reading of the display. Unconditional.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.localizationFz_potential {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : (localizationFz sigma omega lowScale highScale e' R wD wN).potential = fun (x : HCPolySupport.Vec d) => Observable.inverseSqrtLoad sigma (wD.grad x - HCPolySupport.cubeAverageVec R fun (y : HCPolySupport.Vec d) => wD.grad y)

The potential leg of e.Fz.def. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.localizationFz_flux {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : (localizationFz sigma omega lowScale highScale e' R wD wN).flux = fun (x : HCPolySupport.Vec d) => Observable.sqrtLoad sigma (neumannFluxField sigma omega lowScale highScale e' wN x - HCPolySupport.cubeAverageVec R (neumannFluxField sigma omega lowScale highScale e' wN))

The flux leg of e.Fz.def. Unconditional.

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.localizationBackground {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : HCPolySupport.Book.Ch02.DoubledField d

The affine background of the X_z display.

bfAhom_{m-h}^{-1/2} ( e' + grad w_{D,e}^{(K)};
  e  + grad w_{N,e'}^{(K)} + shom_{m-h}^{-1} h e' )

It does not depend on the localization cube: the z-dependence of the display sits entirely in the correction space (L^2_{pot,0} x Lsolo)(z+cu_n), which is why the single field below is the common background of all the cell problems. Unconditional.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.localizationBackground_potential {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : (localizationBackground sigma omega lowScale highScale e e' wD wN).potential = fun (x : HCPolySupport.Vec d) => Observable.inverseSqrtLoad sigma (e' + wD.grad x)

The potential leg of the background. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.localizationBackground_flux {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : (localizationBackground sigma omega lowScale highScale e e' wD wN).flux = fun (x : HCPolySupport.Vec d) => Observable.sqrtLoad sigma (e + neumannFluxField sigma omega lowScale highScale e' wN x)

The flux leg of the background. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.localizationBackground_eq_constantDoubledField_principalPz_add_localizationFz {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : constantDoubledField (principalPz sigma omega lowScale highScale e e' R wD wN) + localizationFz sigma omega lowScale highScale e' R wD wN = localizationBackground sigma omega lowScale highScale e e' wD wN

The identity behind, P_z + bfF_z. The background of the X_z display is the constant field of P_z (e.Pz.def) plus bfF_z (e.Fz.def), for every localization cube R. This is the field-level statement whose variational counterpart is X_z = S_z + tilde S_z. Unconditional.

The two membership clauses, derived

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.potentialZeroTraceFieldOn_grad_dirichletCorrector {d : ℕ} {Q : HCPolySupport.TriadicCube d} (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) : HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn (HCPolySupport.openCubeSet Q) wD.grad

The potential clause, derived. grad w_{D,e}^{(K)} in L^2_{pot,0}(cu_K), which is immediate from w_{D,e}^{(K)} in H^1_0(cu_K) -- exactly the manuscript's reason. No property of the Dirichlet leg of e.def.w beyond its carrier is used. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.solenoidalZeroNormalTraceFieldOn_neumannFluxField {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} {wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)} (hwN : HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) wN fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑sigma)⁻¹ omega lowScale highScale e' x) : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn (HCPolySupport.openCubeSet Q) (neumannFluxField sigma omega lowScale highScale e' wN)

The flux clause, derived. grad w_{N,e'}^{(K)} + shom_{m-h}^{-1} h e' in Lsolo(cu_K).

It is not a manuscript premise and is discharged unconditionally, on every triadic cube and at every sample point, by Corrector.exists_isMeanZeroNeumannRhsWeakSolution_streamForcing; see exists_localizationBackground_isDoubledMuAdmissible below for the produced form.

The manuscript's conormal condition n . (grad w_N + shom^{-1} h e') = 0 on d cu_K is the natural boundary condition of that weak formulation, so Lsolo membership is the formulation itself; the only work below is to pass from the mean-zero gauge in which the problem is posed to arbitrary H^1(cu_K) test functions, which is legitimate because subtracting the average does not change a gradient.

The actual-source hG, derived

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isDoubledMuAdmissible_localizationBackground {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) {wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)} (hwN : HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) wN fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑sigma)⁻¹ omega lowScale highScale e' x) : HCPolySupport.Book.Ch02.IsDoubledMuAdmissible (HCPolySupport.Book.Ch02.cubeDomain Q) (recurrenceP sigma e e') (localizationBackground sigma omega lowScale highScale e e' wD wN)

The membership assertion, at the actual correctors.

bfAhom_{m-h}^{-1/2} ( e' + grad w_D^{(K)}; e + grad w_N^{(K)} + shom_{m-h}^{-1} h e' )
    in  P + L^2_{pot,0}(cu_K) x Lsolo(cu_K) ,        P = bfAhom_{m-h}^{-1/2}(e'; e) .

This is the caller proposition hG of LocalizationGluingAdmissible.isDoubledMuAdmissible_gluedDoubledField, LocalizationGluingCompetitor.blockVecDot_coarseBlockMatrix_le_two_mul_doubledMuValue_glued and LocalizationSelectionFamily.exists_localizationCellSelection, D at the genuine carriers rather than assumed. The derivation is the manuscript's own: the potential leg is a gradient of an H^1_0(cu_K) function, the flux leg is the weak Neumann formulation of e.def.w, and the normalization bfAhom_{m-h}^{-1/2} preserves both classes because it is a scalar block diagonal (e.homs.defs; see the module header).

: on hwN only, the defining property of w_{N,e'}^{(K)}; see solenoidalZeroNormalTraceFieldOn_neumannFluxField and the produced form exists_localizationBackground_isDoubledMuAdmissible.

The actual-source hFpot, hFflux and ambient membership of bfF_z

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.memVectorL2_localizationFz_potential {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R S : HCPolySupport.TriadicCube d) (hsub : HCPolySupport.openCubeSet S ⊆ HCPolySupport.openCubeSet Q) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet S) (localizationFz sigma omega lowScale highScale e' R wD wN).potential

The caller proposition hFpot of LocalizationSelectionExistence.exists_isDoubledMuMinimizerField, derived. The potential leg of bfF_z is vector-L^2 on every subcube of cu_K: it is the gradient of the H^1_0(cu_K) corrector minus a constant, scaled by shom^{-1/2}.: on the inclusion hsub: openCubeSet S ⊆ openCubeSet Q (discharged by the descendant geometry at the call sites).

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.memVectorL2_localizationFz_flux {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R S : HCPolySupport.TriadicCube d) (hsub : HCPolySupport.openCubeSet S ⊆ HCPolySupport.openCubeSet Q) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) (wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)) : HCPolySupport.MemVectorL2 (HCPolySupport.openCubeSet S) (localizationFz sigma omega lowScale highScale e' R wD wN).flux

The caller proposition hFflux, derived. Same statement for the flux leg of bfF_z.: on the inclusion hsub: openCubeSet S ⊆ openCubeSet Q (discharged by the descendant geometry at the call sites); only square integrability is claimed here, and the fresh-shell forcing is continuous.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.isDoubledAmbientField_localizationFz {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} (R : HCPolySupport.TriadicCube d) (hsub : HCPolySupport.openCubeSet R ⊆ HCPolySupport.openCubeSet Q) (wD : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)) {wN : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)} (hwN : HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) wN fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑sigma)⁻¹ omega lowScale highScale e' x) : HCPolySupport.Book.Ch02.IsDoubledAmbientField (HCPolySupport.Book.Ch02.cubeDomain R) (localizationFz sigma omega lowScale highScale e' R wD wN)

The caller proposition hF of LocalizationSelectionVariation.isDoubledResponseField_of_isDoubledMuMinimizerField, derived. On a localization cell R contained in cu_K, bfF_z lies in Lpot(R) x Lsol(R).

The two legs are the manuscript's own: the potential leg is a gradient (of the H^1_0(cu_K) corrector restricted to R) minus a constant, and a constant is itself a gradient; the flux leg is the zero-normal-trace field of solenoidalZeroNormalTraceFieldOn_neumannFluxField restricted to R, minus a constant, and a constant is solenoidal on R because zero-trace test gradients integrate to zero. The normalization bfAhom_{m-h}^{-1/2} preserves both classes by the scalarity of shom_{m-h} (e.homs.defs).

: on hwN, the defining property of w_{N,e'}^{(K)}, and on the inclusion hsub : openCubeSet R ⊆ openCubeSet Q (the cell sits inside the big cube; discharged by the descendant geometry at the call sites).