import PhysicsLogicConsumer.NuclearScattering

open PhysicsLogicConsumer.NuclearScattering PhysicsLogic.Framework.ElasticSWave

example (d : LowEnergyData) : d =
    ⟨d.inverseScatteringLength, d.effectiveRange, d.momentum, d.referenceShortDistanceLength⟩ := rfl
example (d : LowEnergyData) (s : Real) : d.AdmissibleScaleAt s ↔
    0 < d.momentum ∧ d.inverseScatteringLength - s ≠ 0 := Iff.rfl
example (d : LowEnergyData) : d.LowEnergyHierarchyAt ↔
    0 < d.referenceShortDistanceLength ∧ |d.effectiveRange| ≤ d.referenceShortDistanceLength ∧
    |d.inverseScatteringLength| * d.referenceShortDistanceLength ≤ 1 / 16 ∧
    0 < d.momentum ∧ d.momentum * d.referenceShortDistanceLength ≤ 1 / 16 := Iff.rfl
example (d : LowEnergyData) (s : Real) : d.runningContact s = (d.inverseScatteringLength - s)⁻¹ := rfl
example (d : LowEnergyData) (s : Real) : d.derivativeInsertion s =
    d.effectiveRange / 2 * (d.runningContact s) ^ 2 * d.momentum ^ 2 := rfl
example (d : LowEnergyData) (s : Real) : d.leading s = contactAmplitude (d.runningContact s) s d.momentum := rfl
example (d : LowEnergyData) (s : Real) : d.correction s =
    contactInsertionAmplitude (d.runningContact s) (d.derivativeInsertion s) s d.momentum := rfl
example (d : LowEnergyData) (s : Real) : d.resummedDerivativeContact s =
    contactAmplitude (d.runningContact s + d.derivativeInsertion s) s d.momentum := rfl
example : nuclearData = (⟨-1, 1 / 16, 1, 1 / 16⟩ : LowEnergyData) := rfl