import PhysicsLogicConsumer.StatMech

open PhysicsLogic.Paradigm.ReductionAndEmergence
open PhysicsLogicConsumer.StatMech.StateSufficiencyReuse
open PhysicsLogicConsumer.StatMech.RealizerPrediction

example (time : Real) : PhysicsLogicConsumer.StatMech.InitialEnsembleReuse.propagator time =
    !![Real.cos time, Real.sin time, 0; -Real.sin time, Real.cos time, 0; 0, 0, 1] := rfl
example (time : Real) (state : Fin 2 → Real) : update time state =
    ![Real.cos time * state 0 + Real.sin time * state 1,
      -Real.sin time * state 0 + Real.cos time * state 1] := rfl
example (time : Real) (initial : Fin 3 → Real) : retainedState time initial =
    ![Real.cos time * initial 0 + Real.sin time * initial 1,
      -Real.sin time * initial 0 + Real.cos time * initial 1] := rfl
example (time : Real) (initial : Fin 3 → Real) : position time initial =
    Real.cos time * initial 0 + Real.sin time * initial 1 := rfl
example {Value : Type*} (readout : (Fin 2 → Real) → Value) :
    predictionRealization readout = ({
      realizes := fun initial present => readout (retainedState 0 initial) = present
      microSupports := fun initial behavior => readout (retainedState behavior.1 initial) = behavior.2
      macroExhibits := fun present behavior =>
        ∃ initial, readout (retainedState 0 initial) = present ∧
          readout (retainedState behavior.1 initial) = behavior.2
    } : RealizationContext (Fin 3 → Real) Value (Real × Value)) := rfl