UpperHeadSharpCoordinate

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

Sharp one-coordinate wave-head consumption

This file retains the gamma * hsep factor in the squared wave-head bound. The profile hypotheses are derived from the existing induction and energy gates.

The terminal declarations also assemble the tuned collar-head coordinate estimate, finite trace, and deterministic scale absorption.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collar_head_layer_le {d : ℕ} (M : ABKModel d) {m : ℤ} {k : ℕ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d m) (m - 1 - ↑k)) (E : ℝ) (n : ℕ) (j : Fin d) (omega : Cutoff.CutoffSample d) : Multiscale.probeSharpFramedCollarWavePart M R.scale E bfaProfileB (collarBandMeanDepth M E) n (m - 1) (HCPolySupport.basisVec j) (Affine.superposedGradConst d) (fun (eta : Cutoff.CutoffSample d) => Multiscale.waveHeadTerm M R.scale E bfaProfileB (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M E) n) eta ^ 2) omega ≤ Multiscale.probeMeanGoodWaveConst M * HCPolySupport.vecNormSq (HCPolySupport.basisVec j) * (5 * ↑d ^ 2 * Multiscale.waveL4HeadConst d ^ 2) * (4 * Affine.superposedGradConst d ^ 2 * probeSharpCollarBandMeanCapQuarter M E (collarBandMeanDepth M E) * probeSharpCollarBandMeanMassQuarterConst d * 3 ^ (2 * bfaProfileB * ↑(collarBandMeanDepth M E)) * 3 ^ (1 / 16) * whitneyDecayRatio ^ n) * (Multiscale.slstarPowerTerm M R.scale E bfaProfileB M.gamma omega * (M.gamma * ↑(Percolation.hsep M R.scale E bfaProfileB omega)))

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collar_head_coordinate_is_big_o_with {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 }} (hstate : Frozen.Section3.inductionState M (m - 1) E) {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hEgamma : ↑E ≤ M.gamma ^ (-(1 / 5))) (j : Fin d) : have D₀ := Multiscale.probeMeanGoodWaveConst M * HCPolySupport.vecNormSq (HCPolySupport.basisVec j) * (5 * ↑d ^ 2 * Multiscale.waveL4HeadConst d ^ 2) * (4 * Affine.superposedGradConst d ^ 2 * probeSharpCollarBandMeanCapQuarter M (↑E) (collarBandMeanDepth M ↑E) * probeSharpCollarBandMeanMassQuarterConst d * 3 ^ (2 * bfaProfileB * ↑(collarBandMeanDepth M ↑E)) * 3 ^ (1 / 16)); have alpha := upperProfileBaseSigma sigma / ((2 * (M.gamma / 2) + 2 * bfaProfileB) / bfaProfileB); have AP := Percolation.hsepAmplitude (upperProfileSigma sigma) bfaProfileB ^ Multiscale.bfaPower M.gamma bfaProfileB; have AG := upperHeadHsepOneScale sigma M.gamma; HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma)) (fun (omega : Cutoff.CutoffSample d) => ∑' (n : ℕ), Multiscale.probeSharpFramedCollarWavePart M R.scale (↑E) bfaProfileB (collarBandMeanDepth M ↑E) n (m - 1) (HCPolySupport.basisVec j) (Affine.superposedGradConst d) (fun (eta : Cutoff.CutoffSample d) => Multiscale.waveHeadTerm M R.scale (↑E) bfaProfileB (probeSharpLayerAnchor R.scale bfaProfileB (collarBandMeanDepth M ↑E) n) eta ^ 2) (Cutoff.translateCutoffSample (HCPolySupport.triadicCubeShift R) omega)) ((∑' (n : ℕ), D₀ * whitneyDecayRatio ^ n) * (HCPolySupport.Book.Ch04.gammaProductConst alpha 1 * AP * AG))

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.collarHeadHsepOneConst : ℝ

The collar-head constant converting separation height into a linear budget.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.collarHeadTunedTracePrefactor (d : ℕ) : ℝ

The dimension prefactor for the tuned collar-head finite trace.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.collarHeadTunedOutputConst (d : ℕ) : ℝ

The terminal threshold paying the tuned collar-head prefactor.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collar_head_tuned_trace_prefactor_nonneg {d : ℕ} (hd : 2 ≤ d) : 0 ≤ collarHeadTunedTracePrefactor d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collar_head_tuned_output_const_pos {d : ℕ} (hd : 2 ≤ d) : 0 < collarHeadTunedOutputConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gamma_product_const_collar_head_le_sixty_four {sigma gamma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hgamma0 : 0 ≤ gamma) (hgamma : gamma / 2 ≤ bfaProfileB * sigma) : HCPolySupport.Book.Ch04.gammaProductConst (upperProfileBaseSigma sigma / ((2 * (gamma / 2) + 2 * bfaProfileB) / bfaProfileB)) 1 ≤ 64

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upper_head_hsep_one_scale_le_const_mul_gamma {sigma gamma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hgamma : 0 ≤ gamma) : upperHeadHsepOneScale sigma gamma ≤ collarHeadHsepOneConst * gamma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.collar_head_tuned_trace_scale_le_exp {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {E sigma : ℝ} (hE : 0 < E) (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hgammaB : M.gamma ≤ bfaProfileB) (hgammaHalf : M.gamma / 2 ≤ bfaProfileB * sigma) (hlarge : collarBandMeanDepthThreshold d ≤ E⁻¹ ^ 2 * M.gamma⁻¹) : have D₀ := Multiscale.probeMeanGoodWaveConst M * (5 * ↑d ^ 2 * Multiscale.waveL4HeadConst d ^ 2) * (4 * Affine.superposedGradConst d ^ 2 * probeSharpCollarBandMeanCapQuarter M E (collarBandMeanDepth M E) * probeSharpCollarBandMeanMassQuarterConst d * 3 ^ (2 * bfaProfileB * ↑(collarBandMeanDepth M E)) * 3 ^ (1 / 16)); have alpha := upperProfileBaseSigma sigma / ((2 * (M.gamma / 2) + 2 * bfaProfileB) / bfaProfileB); have AP := Percolation.hsepAmplitude (upperProfileSigma sigma) bfaProfileB ^ Multiscale.bfaPower M.gamma bfaProfileB; have AG := upperHeadHsepOneScale sigma M.gamma; ↑d * ((∑' (n : ℕ), D₀ * whitneyDecayRatio ^ n) * (HCPolySupport.Book.Ch04.gammaProductConst alpha 1 * AP * AG)) ≤ collarHeadTunedTracePrefactor d * (Disorder.cstar M)⁻¹ * M.gamma * Real.exp (-(collarBandMeanTunedDecayRate d * (E⁻¹ ^ 2 * M.gamma⁻¹)))

The exact finite-coordinate scale produced by the tuned collar-head estimate has a dimension-only prefactor, the indispensable cstar⁻¹ * gamma, and genuine tuned exponential decay.