decodeMag

formal source

 219
 220We interpret negative values as `0` (via `Int.toNat`) so that a decrement step can “saturate at 0”
 221even if the underlying register becomes negative. -/
 222def decodeMag (z : Int) : Int :=
 223  Int.ofNat (Int.toNat z)
 224
 225/-- Decode a single real coefficient from a voxel: sign from `sigma`, magnitude from `nuPhi`. -/
 226noncomputable def decodeCoeff (v : LNALVoxel) : ℝ :=
 227  ((v.1.sigma * decodeMag v.1.nuPhi : Int) : ℝ)
 228
 229/-- Decode an `LNALField` (of the expected Galerkin encoding length) back to a Galerkin state.
 230
 231This is a left-inverse of `encodeGalerkin2D` only up to the coarse quantization used by `coeffMag`.
 232-/
 233noncomputable def decodeGalerkin2D {N : ℕ} (field : LNALField)
 234    (hsize : field.size = Fintype.card ((modes N) × Fin 2)) : GalerkinState N :=
 235  WithLp.toLp 2 (fun i : ((modes N) × Fin 2) =>
 236    let j : Fin (Fintype.card ((modes N) × Fin 2)) := (Fintype.equivFin ((modes N) × Fin 2)) i
 237    decodeCoeff (field[(Fin.cast hsize.symm j)]))
 238
 239/-- Hypothesis: one LNAL spatial step simulates one discrete Galerkin step (exactly). -/
 240structure SimulationHypothesis (N : ℕ) where
 241  /-- The LNAL program used for the simulation. -/
 242  P : LProgram
 243  /-- The discrete (time-stepping) map on Galerkin states. -/
 244  step : GalerkinState N → GalerkinState N
 245  /-- One-step commutation: execute then encode = encode then step. -/
 246  comm :
 247      ∀ u : GalerkinState N,
 248        (independent.step P (encodeGalerkin2D u)) = encodeGalerkin2D (step u)
 249
 250/-- Trivial simulation: use the `LISTEN noop` LNAL program and take the discrete step as `id`. -/
 251@[simp] def SimulationHypothesis.trivial (N : ℕ) : SimulationHypothesis N :=
 252  { P := listenNoopProgram