SuperposedFluxRateParameters

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

Integer rate parameters for the superposed-flux local payoff

This file selects the two integer parameters left open by SuperposedFluxLocalParameters. Write

R = siteRateBase d / 2 * (E⁻² * gamma⁻¹).

We take k₀ = floor R and kp = floor (R / 8). Thus k₀ is the manuscript's c E⁻² gamma⁻¹ depth, with the coefficient supplied by the proved percolation rate, and kp retains a fixed fraction of the same rate. In particular, this is not the merely qualitative kp = 0 choice from ConclusionFeasibility.lean.

The amended bad-cluster entropy gate, already implied by the frozen maximum and fifth-root hypotheses at b = 2⁻²⁰ and sigma / 4, makes R large enough to absorb the overlap prefactor 9 * 99^d. The floor loss costs one unit: both terms in the raw collar cap are at most exp (-R / 4), while the overlap prefactor is at most exp (R / 8). This leaves exp (-R / 8), which is at most exp (-kp).

These choices are internal proof parameters, not manuscript-stated or frozen declarations.

Rate-compatible real parameters

def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRateEps {d : ℕ} (M : ABKModel d) : ℝ

The layer slack used by the final rate estimate. Unlike the preliminary sigma-scaled choice, this is proportional to gamma, so multiplying it by the primary depth leaves a dimension-only exponent.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRateEps M = M.gamma

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRateBeta {d : ℕ} (M : ABKModel d) : ℝ

The collar exponent used by the final rate estimate. Its excess over the fixed profile slope is proportional to gamma for the same reason.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRateBeta M = Algsuperdiff.Section3.Provider.CoarseEllipticity.bfaProfileB + 2 * M.gamma

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRate {d : ℕ} (M : ABKModel d) (E : ℝ) : ℝ

The corrected percolation rate available to the first Step-3 layer sum.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRate M E = Algsuperdiff.Section3.Provider.Percolation.siteRateBase d / 2 * (E⁻¹ ^ 2 * M.gamma⁻¹)

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxPrimaryDepth {d : ℕ} (M : ABKModel d) (E : ℝ) : ℕ

The source-faithful primary depth k₀ = floor R.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxPrimaryDepth M E = ⌊Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRate M E⌋₊

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRareDepth {d : ℕ} (M : ABKModel d) (E : ℝ) : ℕ

The retained rare-rate depth kp = floor (R / 8).

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRareDepth M E = ⌊Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRate M E / 8⌋₊

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRate_pos {d : ℕ} (M : ABKModel d) {E : ℝ} (hE : 0 < E) : 0 < superposedFluxRate M E

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxDepth_floorWindows {d : ℕ} (M : ABKModel d) {E : ℝ} (hE : 0 < E) : ↑(superposedFluxPrimaryDepth M E) ≤ superposedFluxRate M E ∧ superposedFluxRate M E < ↑(superposedFluxPrimaryDepth M E) + 1 ∧ ↑(superposedFluxRareDepth M E) ≤ superposedFluxRate M E / 8 ∧ superposedFluxRate M E / 8 < ↑(superposedFluxRareDepth M E) + 1

The exact floor windows of the two selected integer parameters.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRateParameterGates_of_profileAuxiliaryMaxGate {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {sigma E : ℝ} (hE : 1 ≤ E) (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) : 3 ≤ superposedFluxPrimaryDepth M E ∧ ↑(superposedFluxPrimaryDepth M E) ≤ Percolation.siteRateBase d / 2 * (E⁻¹ ^ 2 * M.gamma⁻¹) ∧ 9 * 99 ^ d * (Real.exp (-(Percolation.siteRateBase d / 2 * (E⁻¹ ^ 2 * M.gamma⁻¹))) + 3 ^ (-(↑(superposedFluxPrimaryDepth M E) / 2))) ≤ Real.exp (-↑(superposedFluxRareDepth M E))

The two source-faithful integer choices discharge the primary-depth floor, the upper rate constraint used, and the exact cap consumed by slstar_descendantGrid_allL_ae_and_isBigOWith_of_gates.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxRateCompatible_allParameterGates_of_profileAuxiliaryMaxGate {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {sigma E : ℝ} (hE : 1 ≤ E) (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) : 0 < superposedFluxRateEps M ∧ 0 < superposedFluxRateBeta M ∧ 9 * superposedFluxRateBeta M ≤ 1 ∧ 2 * bfaProfileB + 2 * M.gamma + superposedFluxRateEps M ≤ 2 * superposedFluxRateBeta M ∧ 4 * (2 * M.gamma + superposedFluxRateEps M) ≤ 1 - superposedFluxRateBeta M ∧ 3 ≤ superposedFluxPrimaryDepth M E ∧ ↑(superposedFluxPrimaryDepth M E) ≤ Percolation.siteRateBase d / 2 * (E⁻¹ ^ 2 * M.gamma⁻¹) ∧ 9 * 99 ^ d * (Real.exp (-(Percolation.siteRateBase d / 2 * (E⁻¹ ^ 2 * M.gamma⁻¹))) + 3 ^ (-(↑(superposedFluxPrimaryDepth M E) / 2))) ≤ Real.exp (-↑(superposedFluxRareDepth M E)) ∧ superposedFluxLocalExponent M bfaProfileB (superposedFluxRateEps M) (superposedFluxRateBeta M) = 7 * M.gamma ∧ superposedFluxLocalExponent M bfaProfileB (superposedFluxRateEps M) (superposedFluxRateBeta M) ≤ bfaProfileB ∧ (1 - sigma) / 2 ≤ Multiscale.bfaTau (bfaProfileSigma sigma) (superposedFluxLocalExponent M bfaProfileB (superposedFluxRateEps M) (superposedFluxRateBeta M)) bfaProfileB

The rate-compatible real choices together with the two integer choices discharge the complete scalar interface of the local payoff. Their local exponent is exactly 7 * gamma; consequently every occurrence of the primary depth in the eventual profile estimate is multiplied by gamma.

The hmax argument is an internal conditional A obligation inherited from profileAuxiliaryConst; it is discharged downstream because the terminal constant superposedFluxLowerConst d dominates profileAuxiliaryConst d. Thus no numerical gate remains exposed by the terminal lower-leg composition, even though this intermediate helper remains conditional.