foldMinusOneProgram

formal source

 314  H.comm u
 315
 316/-- A constant LNAL program: decrement `nuPhi` by `1` (via `FOLD (-1)`). -/
 317@[simp] def foldMinusOneProgram : LProgram :=
 318  fun _ => LInstr.fold (-1)
 319
 320/-- One-voxel semantics for `foldMinusOneProgram`: decrement `nuPhi` by `1` (clamped); leave `aux5` unchanged. -/
 321lemma voxelStep_foldMinusOneProgram (v : LNALVoxel) :
 322    voxelStep foldMinusOneProgram v = ({ v.1 with nuPhi := clampI32 (v.1.nuPhi + (-1)) }, v.2) := by
 323  rcases v with ⟨r6, a5⟩
 324  simp [LNALSemantics.voxelStep, foldMinusOneProgram, lStep, -clampI32]
 325
 326/-- The corresponding discrete step on **decoded** Galerkin coefficients.
 327
 328We mimic the VM update on `nuPhi` (via `clampI32`) and then decode a nonnegative magnitude using `decodeMag`. -/
 329noncomputable def foldMinusOneDecodedStep {N : ℕ} (u : GalerkinState N) : GalerkinState N :=
 330  WithLp.toLp 2 (fun i : ((modes N) × Fin 2) =>
 331    let x : ℝ := u i
 332    let m : Int := decodeMag (clampI32 (coeffMag x + (-1)))
 333    let z : Int := (coeffSign x) * m
 334    (z : ℝ))
 335
 336/-- Decoding after a single `FOLD (-1)` step matches the corresponding decoded discrete step. -/
 337lemma decodeCoeff_voxelStep_foldMinusOne_encodeIndex {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) :
 338    decodeCoeff (voxelStep foldMinusOneProgram (encodeIndex u i)) = (foldMinusOneDecodedStep u) i := by
 339  classical
 340  -- both sides reduce to the same signed-integer expression
 341  simp [decodeCoeff, foldMinusOneDecodedStep, decodeMag, voxelStep_foldMinusOneProgram, encodeIndex, -clampI32]
 342
 343/-- A concrete, proved decay-step simulation instance (after decoding). -/
 344noncomputable def DecodedSimulationHypothesis.foldMinusOne (N : ℕ) : DecodedSimulationHypothesis N :=
 345  { P := foldMinusOneProgram
 346    step := foldMinusOneDecodedStep
 347    comm := by