import FiniteRecordingEnergy

/-! An executable two-mode representation of the actual Signal8 operations.
Rational amplitudes and a natural phase counter suffice for this invariant
subspace. The embedding below proves the correspondence before evaluation.
-/
namespace ActualMathematics.FiniteRecording

open IndisputableMonolith.Foundation
open ComplexStructureForcing RecognitionProjective RecognitionHamiltonian
open CoherentRecordClock ConservedRecordedCommit
open IndisputableMonolith.Quantum.CodeCoherenceKept
open IndisputableMonolith.LightLanguage.Basis
open IndisputableMonolith.Quantum.EnvironmentClockSector
open NativeCliffordProjection ReciprocalComparison
open IndisputableMonolith.Foundation.DeltaTrace
open scoped BigOperators

structure Profile where
  evenAmp : ℚ
  oddAmp : ℚ
  phase : ℕ
  deriving DecidableEq, Repr

def Profile.advance (p : Profile) : Profile := {p with phase := p.phase + 1}

def profileTick (p r : Profile) : Profile × Profile :=
  (⟨r.evenAmp, p.oddAmp, p.phase+1⟩, ⟨p.evenAmp, r.oddAmp, r.phase+1⟩)

def Profile.intensity (p : Profile) : ℚ := p.evenAmp^2
def Profile.weight (p : Profile) : ℚ := p.evenAmp^2 + p.oddAmp^2
def prepared : Profile := ⟨3/5,4/5,0⟩
def blank : Profile := ⟨0,0,0⟩

noncomputable def Profile.embed (p : Profile) : ComplexStructureForcing.Signal8 :=
  (p.evenAmp : ℂ) • dft8_mode 2 +
    ((p.oddAmp : ℂ) * omega8^p.phase) • dft8_mode 1

theorem prepared_embeds : prepared.embed = concreteState := by
  simp [prepared, Profile.embed, concreteState, pair]

theorem blank_embeds : blank.embed = 0 := by simp [blank, Profile.embed]

theorem embed_advance (p : Profile) :
    p.advance.embed = quarterTurnBeat p.embed := by
  apply coeff_ext
  intro k
  simp only [Profile.embed, Profile.advance, coeff_beat, dft_coefficients_add,
    dft_coefficients_smul, dft_coefficients_mode]
  fin_cases k <;> norm_num [quarterTurnBeatWeight, quarterTurnModes, Fin.ext_iff, pow_succ] <;> ring

theorem profileTick_embeds (p r : Profile) :
    ((profileTick p r).1.embed, (profileTick p r).2.embed) =
      recordedTick quarterTurnSector (p.embed, r.embed) := by
  apply Prod.ext
  · apply coeff_ext
    intro k
    simp only [recordedTick, exchange_first_coeff, CompleteOutputClock.outputBeat,
      coeff_beat, profileTick, Profile.embed, dft_coefficients_add,
      dft_coefficients_smul, dft_coefficients_mode]
    fin_cases k <;> norm_num [quarterTurnSector, quarterTurnModes,
      quarterTurnBeatWeight, Fin.ext_iff, pow_succ] <;> ring
  · apply coeff_ext
    intro k
    simp only [recordedTick, exchange_second_coeff, CompleteOutputClock.outputBeat,
      coeff_beat, profileTick, Profile.embed, dft_coefficients_add,
      dft_coefficients_smul, dft_coefficients_mode]
    fin_cases k <;> norm_num [quarterTurnSector, quarterTurnModes,
      quarterTurnBeatWeight, Fin.ext_iff, pow_succ] <;> ring

theorem profile_intensity (p : Profile) :
    intensity p.embed = (p.intensity : ℝ) := by
  norm_num [intensity, Profile.embed, Profile.intensity, dft_coefficients_add,
    dft_coefficients_smul, dft_coefficients_mode, Fin.ext_iff,
    Complex.normSq, Complex.mul_re, Complex.mul_im]
  ring

theorem profile_energy (p : Profile) :
    signalEnergy p.embed = (p.weight : ℝ) := by
  have hu : Complex.normSq (omega8 ^ p.phase) = 1 := by
    rw [Complex.normSq_eq_norm_sq, norm_pow, omega8_abs]
    simp
  rw [signalEnergy, ← dft_parseval]
  norm_num [Fin.sum_univ_eight, Profile.embed, Profile.weight,
    dft_coefficients_add, dft_coefficients_smul, dft_coefficients_mode,
    Fin.ext_iff, Complex.normSq_mul, Complex.normSq_ratCast, hu]
  ring

def readProfiles : List Profile → Trace
  | [] => .empty
  | p :: ps => if 9/50 < p.intensity then Trace.step (readProfiles ps) else readProfiles ps

theorem profile_occupied (p : Profile) :
    occupied p.embed ↔ (9/50 : ℚ) < p.intensity := by
  rw [occupied, profile_intensity]
  simpa using (Rat.cast_lt (K := ℝ) (p := 9/50) (q := p.intensity))

theorem readProfiles_embeds (ps : List Profile) :
    read (ps.map Profile.embed) = readProfiles ps := by
  induction ps with
  | nil => rfl
  | cons p ps ih => simp [read, readProfiles, profile_occupied, ih]

theorem profileTick_weight (p r : Profile) :
    (profileTick p r).1.weight + (profileTick p r).2.weight =
      p.weight + r.weight := by
  simp only [profileTick, Profile.weight]
  ring

theorem advance_weight (p : Profile) : p.advance.weight = p.weight := rfl
theorem advance_intensity (p : Profile) : p.advance.intensity = p.intensity := rfl

end ActualMathematics.FiniteRecording

#print axioms ActualMathematics.FiniteRecording.profileTick_embeds
#print axioms ActualMathematics.FiniteRecording.embed_advance
#print axioms ActualMathematics.FiniteRecording.profile_intensity
#print axioms ActualMathematics.FiniteRecording.profileTick_weight
#print axioms ActualMathematics.FiniteRecording.profile_energy
#print axioms ActualMathematics.FiniteRecording.readProfiles_embeds