ShellLawPrefix

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

structure Algsuperdiff.Frozen.Assumptions.ShellLawPrefix (d : ℕ) (gamma : ℝ) (P : MeasureTheory.ProbabilityMeasure (ℤ → ShellField d)) : Prop

The nu-free shell-law prefix from ABK26: the paper-wide dimension and scaling parameters, mutual independence of all shells, and the exact marginal scaling law under the canonical sequence law. Molecular diffusivity nu > 0 is deferred to the cutoff/coefficient parameter surface. Antisymmetry and qualitative C^2 regularity hold by the ShellField carrier itself.

• dimension : 2 ≤ d
• gamma_pos : 0 < gamma
• gamma_le_quarter : gamma ≤ 1 / 4
• independent : ProbabilityTheory.iIndepFun (fun (k : ℤ) (F : ℤ → ShellField d) => F k) ↑P
• marginal_scaling (k : ℤ) : ShellField.shellMarginalLaw P k = (ShellField.zeroShellLaw P).map (ShellField.triadicScale gamma k)