import PhysicsLogic.Papers.Bethe1949.BindingSensitivity
import PhysicsLogic.Papers.Bethe1949.IntensityExtraction

open PhysicsLogic.Papers.BlattJackson1949.ThresholdExtraction
open PhysicsLogic.Papers.Bethe1949.BindingSensitivity
open PhysicsLogic.Papers.Bethe1949.IntensityExtraction

variable (l : Lengths) (r : Real → Real) (b x y z : Real) (record : Real × Real)

example : parahydrogenIntensity l = (3 * l.triplet + l.singlet) ^ 2 := by rfl
example : intensityRecords.admissible l ↔ 0 < l.triplet ∧ l.singlet < 0 := by rfl
example : intensityRecords = records.mapRecords (fun reading => (reading.1, 4 * reading.2 ^ 2)) := rfl
example : intensityRecords.recordAt () l = (crossSection l, parahydrogenIntensity l) := by
  change (crossSection l, 4 * coherentAmplitude l ^ 2) = _
  congr 1
  dsimp [coherentAmplitude, parahydrogenIntensity]
  ring
example : intensityRecords.valueAt l = l.triplet := by rfl
example : negativeAmplitudeRecords.admissible l ↔
    (0 < l.triplet ∧ l.singlet < 0) ∧ coherentAmplitude l ≤ 0 := by rfl
example : negativeAmplitudeRecords =
    { intensityRecords with admissible := fun lengths =>
        intensityRecords.admissible lengths ∧ coherentAmplitude lengths ≤ 0 } := rfl
example : negativeAmplitudeRecords.recordAt () l = (crossSection l, parahydrogenIntensity l) := by
  change (crossSection l, 4 * coherentAmplitude l ^ 2) = _
  congr 1
  dsimp [coherentAmplitude, parahydrogenIntensity]
  ring
example : negativeAmplitudeRecords.valueAt l = l.triplet := by rfl
example : negativeBranchTriplet record =
    -Real.sqrt record.2 / 4 + Real.sqrt ((record.1 / Real.pi - (-Real.sqrt record.2 / 2) ^ 2) / 12) := by
  simp only [negativeBranchTriplet, centralTriplet]
  ring

-- Pin the decoder's literal signed input as well as its arithmetic readback.
example : negativeBranchTriplet record = centralTriplet (record.1, -Real.sqrt record.2 / 2) := by rfl
example : printedRadius b x = b * (1 + x / 2) := by rfl
example : kinematicRadius b x = b / Real.sqrt (1 + x) := by rfl
example : normalizedBindingInvariant r x = (1 + x) * r x ^ 2 := by rfl
example : printedTripletRange x y z = 156 / 100 + 27 / 10 * x + 5 * y - 3 / 2 * z := by rfl