SuperposedFluxLocalParameters

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

Parameters for the superposed-flux local payoff

This file selects the two auxiliary exponents in the local lower-payoff producer. For the manuscript's fixed b = 2⁻²⁰ and external exponent sigma, set

eps  = b * sigma / 8,
beta = b + b * sigma / 4.

These are internal Lean proof parameters: the manuscript does not state these values, and neither definition is a frozen declaration. The exponential branch of the frozen maximum is stronger than the coarse gamma = O(b * sigma) estimate used by ProfileConstants.lean. Applying the same elementary exponential-decay lemma at the auxiliary scale b / 16 gives gamma ≤ (3 / 32) * b * sigma. This bound pays every eps- and beta-based scalar gate of slstar_descendantGrid_allL_ae_and_isBigOWith_of_gates, including its explicit superposedFluxLocalExponent ≤ b premise. It also keeps the resulting local Orlicz exponent at least (1 - sigma) / 2 after the source's sigma ↦ sigma / 4 substitution.

This file does not select the integers k₀ and kp, and it does not prove the separate rate-cap inequality hcap; those require another producer.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gamma_le_three_div_thirty_two_mul_bfaProfileB_mul_sigma_of_profileAuxiliaryMaxGate {d : ℕ} (M : ABKModel d) {sigma E : ℝ} (hE : 1 ≤ E) (hsigma : 0 < sigma) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) : M.gamma ≤ 3 / 32 * bfaProfileB * sigma

The exact frozen maximum and fifth-root gates give the sharper smallness needed by the superposed-flux parameter choice.