JunctionDischargePrincipalSwitch

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

Junction 4 discharged: the principal comparison at the closure's own correctors

ABK26, l.approximate.recurrence.formula, Steps 1--3 and e.lower.bound.principal.one.

Closure.Junctions.PrincipalSwitchEndpoint is the proved principal-response terminal exists_const_descendantsAverage_integral_principalEnergy_le_annealedLimit, re-indexed from the terminal's (m - hgap, m) to the recurrence pair (n, n + h). Two things separate the two statements, and this module supplies both.

1. The integer re-indexing. Instantiating the terminal at m := n + h and hgap := h leaves the single rewrite n + h - h = n; that is the whole of the carrier difference, exactly as Closure.Junctions' header records.

2. The choice of correctors. The terminal produces its pair w_D, w_N existentially, indexed by the shell sequence. The closure assembly cannot use that pair: Steps 4 and 5 and the fresh-shell energy display all read the correctors along the increment path (Closure.alongIncrementPath), and one and the same pair has to serve all four junctions at every localization cube. So the terminal's conclusion has to be transported from its witness pair to the caller's pair. That transport is legitimate, and unconditional: the two problems of e.def.w determine their solutions' gradients (Corrector.FreshShellUniqueness), and both Closure.principalEnergyAverage and Closure.gaugeEnergyAverage see the correctors only through cubeAverageVec R (grad w) on the descendant cubes of cu_K. The congruence lemmas below make that visible, one carrier at a time, and principalSwitchEndpoint_of_terminal states the terminal at an arbitrary pair of solutions of e.def.w.

What is supplied

• cubeAverageVec_congr_ae --- the cube average only sees the a.e. class.
• grad_ae_eq_of_isZeroTraceDirichletRhsWeakSolution, grad_ae_eq_of_isMeanZeroNeumannRhsWeakSolution --- gradient uniqueness of e.def.w in the pointwise a.e. spelling the congruences consume.
• principalPz_congr_ae, gaugedPrincipalLoadShell_congr_ae, principalEnergyAverage_congr_ae, gaugeEnergyAverage_congr_ae, principalSwitchEndpoint_congr_ae --- the transport, carrier by carrier.
• principalSwitchEndpoint_of_terminal --- Closure.PrincipalSwitchEndpoint, proved, at any pair of e.def.w solutions, from the proved terminal.

The terminal's source premises, threaded

principalSwitchEndpoint_of_terminal carries exactly the terminal's own binders, re-indexed:

binder	terminal's form	here
induction state	inductionState M (m - 1) E	inductionState M (n + h - 1) Ec
shell nondegeneracy	0 < hgap	0 < h
regime	Cterm cstar^{-1} <= E	unchanged
fifth-root gate	cgamma <= E^{-5}	unchanged
shell budget	hgap <= 6 cstar cgamma^{-1}	unchanged
localization gap	10^10 cgamma^{-1} <= Kc - m	... <= Kc - (n + h)
directions	|e|, |e'| <= 1	unchanged
depth naming	Kc - j = recurrenceMesoScale a cgamma m hgap	at m = n + h

No binder is added, none is weakened, and no smallness beyond the terminal's own is assumed. The two corrector binders hwD, hwN are e.def.w itself --- the definition of the pair the caller is using, not an assumption about it.

References

• ABK26, l.approximate.recurrence.formula, Steps 1--3.
• ABK26, e.def.w; e.Pz.def.

The cube average sees only the a.e. class

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeAverageVec_congr_ae {d : ℕ} (R : HCPolySupport.TriadicCube d) {g1 g2 : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : g1 =ᵐ[MeasureTheory.volume.restrict (HCPolySupport.cubeSet R)] g2) : HCPolySupport.cubeAverageVec R g1 = HCPolySupport.cubeAverageVec R g2

Unconditional: two fields that agree a.e. on a triadic cube have the same cube average.

Gradient uniqueness of e.def.w, in the pointwise a.e. spelling

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.grad_ae_eq_of_isZeroTraceDirichletRhsWeakSolution {d : ℕ} (Q : HCPolySupport.TriadicCube d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {u v : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)} (hu : HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) u g) (hv : HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) v g) : (fun (x : HCPolySupport.Vec d) => u.grad x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet Q)] fun (x : HCPolySupport.Vec d) => v.grad x

Unconditional: two zero-trace Dirichlet weak solutions of e.def.w for one and the same forcing have a.e. equal gradients. This is Corrector.gradToVectorL2_eq_of_isZeroTraceDirichletRhsWeakSolution_openCubeSet read through H1Function.coeFn_gradToVectorL2.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.grad_ae_eq_of_isMeanZeroNeumannRhsWeakSolution {d : ℕ} (Q : HCPolySupport.TriadicCube d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {u v : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)} (hu : HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) u g) (hv : HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet Q) v g) : (fun (x : HCPolySupport.Vec d) => u.toH1Function.grad x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet Q)] fun (x : HCPolySupport.Vec d) => v.toH1Function.grad x

Unconditional: the mean-zero Neumann mirror.

The transport, carrier by carrier

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.principalPz_congr_ae {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} {j : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth Q j) {wD1 wD2 : HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)} {wN1 wN2 : HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)} (hD : (fun (x : HCPolySupport.Vec d) => wD1.grad x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet Q)] fun (x : HCPolySupport.Vec d) => wD2.grad x) (hN : (fun (x : HCPolySupport.Vec d) => wN1.toH1Function.grad x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet Q)] fun (x : HCPolySupport.Vec d) => wN2.toH1Function.grad x) : principalPz sigma omega lowScale highScale e e' R wD1 wN1 = principalPz sigma omega lowScale highScale e e' R wD2 wN2

Unconditional: e.Pz.def reads the two correctors only through their cube averages, so a.e. equal gradients give the same load.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gaugedPrincipalLoadShell_congr_ae {d : ℕ} (sigma : Observable.PositiveScalar) (omega : Cutoff.ShellSeq d) (lowScale highScale : ℤ) (e e' : HCPolySupport.Vec d) {Q : HCPolySupport.TriadicCube d} {j : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth Q j) {wD1 wD2 : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet Q)} {wN1 wN2 : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet Q)} (hD : (fun (x : HCPolySupport.Vec d) => (wD1 omega).grad x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet Q)] fun (x : HCPolySupport.Vec d) => (wD2 omega).grad x) (hN : (fun (x : HCPolySupport.Vec d) => (wN1 omega).toH1Function.grad x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet Q)] fun (x : HCPolySupport.Vec d) => (wN2 omega).toH1Function.grad x) : gaugedPrincipalLoadShell sigma R lowScale highScale e e' wD1 wN1 omega = gaugedPrincipalLoadShell sigma R lowScale highScale e e' wD2 wN2 omega

Unconditional: the gauged load of the terminal inherits the congruence.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.principalEnergyAverage_congr_ae {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (j : ℕ) (e e' : HCPolySupport.Vec d) {wD1 wD2 : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))} {wN1 wN2 : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))} (hD : ∀ (omega : Cutoff.ShellSeq d), (fun (x : HCPolySupport.Vec d) => (wD1 omega).grad x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))] fun (x : HCPolySupport.Vec d) => (wD2 omega).grad x) (hN : ∀ (omega : Cutoff.ShellSeq d), (fun (x : HCPolySupport.Vec d) => (wN1 omega).toH1Function.grad x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))] fun (x : HCPolySupport.Vec d) => (wN2 omega).toH1Function.grad x) : principalEnergyAverage M n h Kc j e e' wD1 wN1 = principalEnergyAverage M n h Kc j e e' wD2 wN2

Unconditional: the left-hand carrier of the terminal depends on the correctors only through their a.e. classes.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gaugeEnergyAverage_congr_ae {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (j : ℕ) (e e' : HCPolySupport.Vec d) {wD1 wD2 : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))} {wN1 wN2 : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))} (hD : ∀ (omega : Cutoff.ShellSeq d), (fun (x : HCPolySupport.Vec d) => (wD1 omega).grad x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))] fun (x : HCPolySupport.Vec d) => (wD2 omega).grad x) (hN : ∀ (omega : Cutoff.ShellSeq d), (fun (x : HCPolySupport.Vec d) => (wN1 omega).toH1Function.grad x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))] fun (x : HCPolySupport.Vec d) => (wN2 omega).toH1Function.grad x) : gaugeEnergyAverage M n h Kc j e e' wD1 wN1 = gaugeEnergyAverage M n h Kc j e e' wD2 wN2

Unconditional: the right-hand carrier of the terminal, likewise.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.principalSwitchEndpoint_congr_ae {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (Kc : ℤ) (j : ℕ) (Ec : { E : ℝ // 1 ≤ E }) (e e' : HCPolySupport.Vec d) {wD1 wD2 : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))} {wN1 wN2 : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))} (hD : ∀ (omega : Cutoff.ShellSeq d), (fun (x : HCPolySupport.Vec d) => (wD1 omega).grad x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))] fun (x : HCPolySupport.Vec d) => (wD2 omega).grad x) (hN : ∀ (omega : Cutoff.ShellSeq d), (fun (x : HCPolySupport.Vec d) => (wN1 omega).toH1Function.grad x) =ᵐ[HCPolySupport.volumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))] fun (x : HCPolySupport.Vec d) => (wN2 omega).toH1Function.grad x) (hswitch : PrincipalSwitchEndpoint M n h Kc j Ec e e' wD1 wN1) : PrincipalSwitchEndpoint M n h Kc j Ec e e' wD2 wN2

Unconditional: Closure.PrincipalSwitchEndpoint transports along a.e.-equal corrector gradients.

Junction 4, discharged

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.principalSwitchEndpoint_of_terminal (d : ℕ) (hd : 2 ≤ d) : ∃ (Cterm : ℝ), 0 < Cterm ∧ ∀ (M : ABKModel d) (n Kc : ℤ) (h : ℕ) (Ec : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (n + ↑h - 1) Ec → 0 < h → Cterm * (Disorder.cstar M)⁻¹ ≤ ↑Ec → M.gamma ≤ ↑Ec ^ (-5) → ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹ → 10 ^ 10 * M.gamma⁻¹ ≤ ↑Kc - ↑(n + ↑h) → ∀ (e e' : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e ≤ 1 → HCPolySupport.Book.Ch02.vecNorm e' ≤ 1 → ∀ (j : ℕ), (HCPolySupport.originCube d Kc).scale - ↑j = recurrenceMesoScale recurrenceGapMultiplier M.gamma (n + ↑h) ↑h → ∀ (wD : Cutoff.ShellSeq d → HCPolySupport.H10Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))) (wN : Cutoff.ShellSeq d → HCPolySupport.H1MeanZeroFunction (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc))), (∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsZeroTraceDirichletRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc)) (wD omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M n))⁻¹ omega n (n + ↑h) e x) → (∀ (omega : Cutoff.ShellSeq d), HCPolySupport.IsMeanZeroNeumannRhsWeakSolution (fun (x : HCPolySupport.Vec d) => 1) (HCPolySupport.openCubeSet (HCPolySupport.originCube d Kc)) (wN omega) fun (x : HCPolySupport.Vec d) => -Corrector.streamForcing (↑(Annealed.sigmaBar M n))⁻¹ omega n (n + ↑h) e' x) → PrincipalSwitchEndpoint M n h Kc j Ec e e' wD wN

Closure.PrincipalSwitchEndpoint, proved, at any pair of e.def.w solutions.

The constant Cterm is the proved terminal's own; the premises are the terminal's own, re-indexed from (m - hgap, m) to (n, n + h). hwD and hwN are the definition of the corrector pair the caller is using, i.e. e.def.w at the directions e, e'; the terminal's own witness pair is discarded in favour of the caller's by gradient uniqueness.

No incomplete-proof axiom is inherited. See the module header.