SuperposedFluxLocalPayoff

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

Local lower payoff from the finite flux-coordinate conclusion

This file transports the proved local finite q-coordinate result from the centered cube to an arbitrary descendant. The transport is simultaneous over the countable family of cutoff indices L : ℤ. It then isolates the L-free flux constant and converts the resulting conditional Step-3 payoff to the existing local bfa lane.

The local hsepSet.Nonempty and literal random-profile wave envelopes stay explicit. In particular, no almost-everywhere statement is promoted to a pointwise statement, and no intersection over an uncountable load space is taken. The running diffusivity is used directly at i = m - 1; there is no comparison with another sigmaBar scale.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cutoffSigmaStarInvBlockFamily_translateCutoffSample {d : ℕ} [NeZero d] (M : ABKModel d) (L : ℤ) (scaling : ℝ) (R : HCPolySupport.TriadicCube d) (omega : Cutoff.CutoffSample d) : cutoffSigmaStarInvBlockFamily M L scaling R omega = cutoffSigmaStarInvBlockFamily M L scaling (HCPolySupport.originCube d R.scale) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)

Exact translation covariance of the normalized one-cube lower observable used by the payload sandwich. The totalized coefficient-field carrier is first identified with the literal cutoff family on both cubes.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.descendantInverseBlock_le_superposedFluxBasis_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m - 1) E) {b : ℝ} (hb0 : 0 < b) (hb : b ≤ 1 / 8) {k₀ : ℕ} (hk₀ : 3 ≤ k₀) {eps : ℝ} (heps : 0 < eps) {t : ℝ} (ht0 : 0 ≤ t) {beta : ℝ} (hbeta0 : 0 < beta) (hbeta9 : 9 * beta ≤ 1) (hbetab : 2 * b + 2 * M.gamma + eps ≤ 2 * beta) (hgammaWin : 4 * (2 * M.gamma + eps) ≤ 1 - beta) {kp : ℕ} (hcap : 9 * 99 ^ d * (Real.exp (-(Percolation.siteRateBase d / 2 * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) + 3 ^ (-(↑k₀ / 2))) ≤ Real.exp (-↑kp)) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), (Percolation.hsepSet M R.scale (↑E) b (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)).Nonempty → ∀ (L : ℤ), m - 1 ≤ L → (∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer R.scale (Whitney.whitneyScale M R.scale (↑E) b k₀ (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)) n, Stream.cubeSupBound Q Q.scale L ↑(Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega) ≤ Multiscale.whitneyWaveLayerScale M R.scale (Whitney.whitneyScale M R.scale (↑E) b k₀ (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)) n L * t) → cutoffSigmaStarInvBlockFamily M L (↑(Annealed.sigmaBar M (m - 1))) R omega ≤ ∑ j : Fin d, Multiscale.superposedConclusionPayload M R.scale (m - 1) L (↑E) b eps t beta k₀ kp (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega) 0 (HCPolySupport.basisVec j)

On an arbitrary descendant of originCube d m, the finite flux payoff is available almost surely and simultaneously for every cutoff index L ≥ m - 1. Both remaining local gates are literal predicates of the translated sample.

The L-free flux payload

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxCoordinateConst {d : ℕ} (M : ABKModel d) (n i : ℤ) (eps beta : ℝ) (kp : ℕ) : ℝ

Sum of the finite flux-coordinate layer constants after setting the irrelevant potential load and its wave-envelope slot to zero.

Equations

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

def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxLocalExponent {d : ℕ} (M : ABKModel d) (b eps beta : ℝ) : ℝ

The exponent left on the random separation scale after moving the 2 * b collar power into the standard local lane.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxLocalExponent M b eps beta = 2 * M.gamma + eps + 2 * (beta - b)

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxLocalConst {d : ℕ} (M : ABKModel d) (n i : ℤ) (eps beta : ℝ) (k₀ kp : ℕ) : ℝ

The deterministic k₀ shift absorbed into the local payoff constant.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRare (kp : ℕ) : ℝ

The exact rare factor inherited from the corrected layer summation.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRare kp = Real.exp (-(↑kp / 36))

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.sum_superposedConclusionPayload_flux_basis_eq {d : ℕ} (M : ABKModel d) (n i L : ℤ) (E b eps t beta : ℝ) (k₀ kp : ℕ) (omega : Cutoff.CutoffSample d) : ∑ j : Fin d, Multiscale.superposedConclusionPayload M n i L E b eps t beta k₀ kp omega 0 (HCPolySupport.basisVec j) = superposedFluxCoordinateConst M n i eps beta kp * (3 ^ ((2 * M.gamma + eps) * ↑(Percolation.hsep M n E b omega + k₀)) * (1 + 3 ^ (2 * beta * ↑(Percolation.hsep M n E b omega + k₀)) * superposedFluxRare kp))

For pure flux basis loads, both analytic layer constants are independent of L and of the literal wave amplitude t.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxCoordinateConst_nonneg {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (n i : ℤ) (eps beta : ℝ) (kp : ℕ) : 0 ≤ superposedFluxCoordinateConst M n i eps beta kp

The finite flux-coordinate constant is nonnegative.

Conditional local payoff