OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/FiniteStackArithmetic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Faithfulness of finite little-endian integer stacks, including their infinite zero tails. This is used for the entire finite recorder table.

  1. theorem OAI.ForcedComputation.Lattice.stackValue_injective_prefix line 10
  2. theorem OAI.ForcedComputation.Lattice.stackValue_injective_zero_tail line 31
  3. theorem OAI.ForcedComputation.Lattice.prepend_injective line 40
  4. theorem OAI.ForcedComputation.Lattice.nat_eq_of_mod_div_eq line 50
  5. theorem OAI.ForcedComputation.Lattice.nextStacks_recover line 59

    Source documentation

    The written digit and both old stack tails are recoverable from the new stacks, once the incoming movement is known.

    theorem nextStacks_recover {b L₁ L₂ R₁ R₂ a₁ a₂ : ℕ}
    (hb : 0 < b) (ha₁ : a₁ < b) (ha₂ : a₂ < b) (m : Fin 3)
    (hL : nextLeft b L₁ a₁ m = nextLeft b L₂ a₂ m)
    (hR : nextRight b L₁ R₁ a₁ m = nextRight b L₂ R₂ a₂ m) :
    L₁ = L₂ ∧ R₁ / b = R₂ / b ∧ a₁ = a₂ := by
…

    Mentions: OAI.ForcedComputation.Lattice.nextLeft, OAI.ForcedComputation.Lattice.nextRight

  6. theorem OAI.ForcedComputation.Lattice.nextStacks_injective_of_read line 76