diff --git a/cedar-lean/Cedar/Spec/Ext/Decimal.lean b/cedar-lean/Cedar/Spec/Ext/Decimal.lean
index 949d72db6..f37c8e669 100644
--- a/cedar-lean/Cedar/Spec/Ext/Decimal.lean
+++ b/cedar-lean/Cedar/Spec/Ext/Decimal.lean
@@ -33,7 +33,7 @@ For instance, 10.234 is a decimal number. Its integer part is 10 and its fractio
 We restrict the number of the digits after the decimal point to 4.
 -/
 
-def DECIMAL_DIGITS : Nat := 4
+public abbrev DECIMAL_DIGITS : Nat := 4
 
 public abbrev Decimal := Int64
 
@@ -47,7 +47,7 @@ public def decimal? (i : Int) : Option Decimal :=
 
 public def parse (str : String) : Option Decimal :=
   match str.splitToList (· = '.') with
-  | ["-", _] => .none -- String.toInt? "-" == some 0
+  | ["-", _] => .none -- guard against bare "-"; redundant on current stdlib (`String.toInt? "-" = none`) but robust to stdlib changes
   | [left, right] =>
     let rlen := right.length
     if 0 < rlen ∧ rlen ≤ DECIMAL_DIGITS
@@ -62,7 +62,7 @@ public def parse (str : String) : Option Decimal :=
     else .none
   | _ => .none
 
-instance : ToString Decimal where
+public instance : ToString Decimal where
   toString (d : Decimal) : String :=
     let neg   := if d < 0 then "-" else ""
     let d     := d.natAbs
diff --git a/cedar-lean/Cedar/Thm/Data/String.lean b/cedar-lean/Cedar/Thm/Data/String.lean
new file mode 100644
index 000000000..8464fedc6
--- /dev/null
+++ b/cedar-lean/Cedar/Thm/Data/String.lean
@@ -0,0 +1,268 @@
+module
+
+public import Std.Data.String
+public import Batteries.Data.String
+public import Cedar.Spec.Ext.Util
+import all Cedar.Spec.Ext.Util
+import all Init.Data.String.Search
+import all Init.Data.String.Slice
+
+open Cedar.Spec.Ext
+
+/-! ==============================================================================================
+    # Digit strings (`Digit⁺`) and their correspondence with `toNat?'`
+
+    `IsDigits` is the grammar-level notion of a non-empty run of digit characters — the
+    `Digit⁺` production common to numeric grammars. These lemmas connect it to the stdlib
+    natural-number parser `toNat?'`: a digit string is exactly one `toNat?'` accepts (modulo the
+    `'_'` separator, which `toNat?'` rejects and `Char.isDigit` never admits). The `IsDigits.*`
+    projections at the end give dot-notation for the facts parser proofs consume.
+    ============================================================================================== -/
+
+/-- `Digit⁺`: a non-empty string all of whose characters are decimal digits. -/
+public def IsDigits (s : String) : Prop :=
+  0 < s.length ∧ ∀ c ∈ s.toList, c.isDigit = true
+
+/-- `Digit{n}`: a run of exactly `n` decimal digits. The fixed-width refinement of `IsDigits`,
+    used wherever a grammar pins a field's width (the datetime grammar's `YYYY`, `MM`, `SSS`, …). -/
+-- ANCHOR: IsFixedDigits
+public def IsFixedDigits (n : Nat) (s : String) : Prop :=
+  IsDigits s ∧ s.length = n
+-- ANCHOR_END: IsFixedDigits
+
+/-- `Digit{1,n}`: between one and `n` decimal digits. `IsDigits` supplies the lower bound and the
+    length constraint the upper (the decimal grammar's `Fraction ::= Digit{1,4}`). -/
+-- ANCHOR: IsDigitsUpTo
+public def IsDigitsUpTo (n : Nat) (s : String) : Prop :=
+  IsDigits s ∧ s.length ≤ n
+-- ANCHOR_END: IsDigitsUpTo
+
+/-- `['-']`: an optional leading minus sign, either present or absent. Shared by the numeric
+    grammars that admit a signed literal (decimal's `Sign`, duration's leading `'-'`). -/
+-- ANCHOR: IsWfSign
+public def IsWfSign (s : String) : Prop :=
+  s = "-" ∨ s = ""
+-- ANCHOR_END: IsWfSign
+
+/-- A digit string contains no `'_'`, so `toInt?'`/`toNat?'` (which reject `'_'`) do not
+    short-circuit on it. -/
+theorem no_underscore_of_isDigits {s : String} (h : IsDigits s) : s.contains '_' = false := by
+  obtain ⟨_, hdig⟩ := h
+  have hnot : ¬ ('_' ∈ s.toList) := by
+    intro hm; have := hdig '_' hm; simp at this
+  simpa [String.contains] using hnot
+
+/-- A digit string is a well-formed natural-number literal (`String.isNat`). -/
+theorem isNat_of_isDigits {s : String} (h : IsDigits s) : s.isNat = true := by
+  obtain ⟨hlen, hdig⟩ := h
+  have hne : s.toList ≠ [] := List.ne_nil_of_length_pos hlen
+  rw [String.isNat_iff]
+  refine ⟨?_, ?_, ?_, ?_, ?_⟩
+  · intro hs; rw [hs] at hlen; simp at hlen
+  · intro c hc; left; exact hdig c hc
+  · intro hinfix
+    rcases hinfix with ⟨p, t, ht⟩
+    have : '_' ∈ s.toList := by rw [← ht]; simp [List.mem_append]
+    have := hdig '_' this; simp at this
+  · intro hh
+    have hmem : '_' ∈ s.toList := by
+      have heq : s.toList.head hne = '_' := by
+        have := List.head?_eq_some_head hne
+        rw [this] at hh; injection hh
+      exact heq ▸ List.head_mem hne
+    have := hdig '_' hmem; simp at this
+  · intro hh
+    have hmem := List.getLast_mem hne
+    rw [List.getLast?_eq_some_getLast hne] at hh
+    injection hh with hh
+    rw [hh] at hmem
+    have := hdig '_' hmem; simp at this
+
+/-- Conversely, a natural-number literal with no `'_'` is a digit string. -/
+theorem isDigits_of_isNat {s : String} (hisnat : s.isNat = true)
+    (hnc : s.contains '_' = false) : IsDigits s := by
+  rw [String.isNat_iff] at hisnat
+  obtain ⟨hne_empty, hchars, _, _, _⟩ := hisnat
+  refine ⟨?_, ?_⟩
+  · rw [← String.length_toList]
+    apply List.length_pos_iff.mpr
+    intro he; apply hne_empty; rw [← String.toList_inj]; simpa using he
+  · intro c hc
+    cases hchars c hc with
+    | inl h => exact h
+    | inr h =>
+      subst h
+      have hcontains : s.contains '_' = true := by simpa [String.contains] using hc
+      rw [hcontains] at hnc; simp at hnc
+
+/-- Forward bridge: a `Digit⁺` string parses as a natural number. -/
+theorem toNat?'_isSome_of_isDigits {s : String} (h : IsDigits s) :
+    (toNat?' s).isSome = true := by
+  unfold toNat?'
+  rw [no_underscore_of_isDigits h]
+  simp only [Bool.false_eq_true, ↓reduceIte]
+  rw [show s.toNat?.isSome = s.isNat from String.isSome_toNat?]
+  exact isNat_of_isDigits h
+
+/-- Backward bridge: anything `toNat?'` accepts is a `Digit⁺` string. -/
+theorem isDigits_of_toNat?'_isSome {s : String} (h : (toNat?' s).isSome = true) :
+    IsDigits s := by
+  unfold toNat?' at h
+  split at h
+  · simp at h
+  · rename_i hnc
+    rw [Bool.not_eq_true] at hnc
+    rw [show s.toNat?.isSome = s.isNat from String.isSome_toNat?] at h
+    exact isDigits_of_isNat h hnc
+
+/-- A digit string is nonempty. -/
+theorem IsDigits.ne_empty {s : String} (h : IsDigits s) : s ≠ "" := by
+  intro he; rw [he] at h; exact absurd h.1 (by simp)
+
+/-- A digit string is accepted by `toNat?'` (dot-notation alias of `toNat?'_isSome_of_isDigits`,
+    used to recover the numeric value). -/
+theorem IsDigits.toNat?'_isSome {s : String} (h : IsDigits s) : (toNat?' s).isSome = true :=
+  toNat?'_isSome_of_isDigits h
+
+/-- Every character of a digit string is a digit (the second component of `IsDigits`). -/
+theorem IsDigits.all_isDigit {s : String} (h : IsDigits s) :
+    ∀ c ∈ s.toList, c.isDigit = true := h.2
+
+/-- If `toNat?'` succeeds then the string is non-empty. -/
+theorem toNat?'_isSome_length_pos (s : String) (h : (toNat?' s).isSome) : s.length > 0 := by
+  by_contra hlen
+  simp at hlen
+  subst hlen
+  have hcontains : ("".contains '_') = false := by simp
+  simp only [toNat?', hcontains, Bool.false_eq_true, ↓reduceIte] at h
+  rw [String.isSome_toNat?, String.isNat_iff] at h
+  exact h.1 rfl
+
+/-! ==============================================================================================
+    # Splitting a string on a separator
+    ============================================================================================== -/
+
+/-- If no element of `l` satisfies `P`, then `splitOnPPrepend P l acc` returns
+    the single segment `[acc.reverse ++ l]` (the accumulator is prepended in reverse). -/
+theorem splitOnPPrepend_no_sep (P : α → Bool) (l acc : List α)
+    (h : ∀ x ∈ l, P x = false) :
+    List.splitOnPPrepend P l acc = [(acc.reverse ++ l)] := by
+  induction l generalizing acc with
+  | nil => simp
+  | cons a t ih =>
+    have ha : P a = false := h a (List.mem_cons.mpr (.inl rfl))
+    rw [List.splitOnPPrepend_cons_neg ha]
+    rw [ih (a :: acc) (fun x hx => h x (List.mem_cons.mpr (.inr hx)))]
+    simp [List.reverse_cons, List.append_assoc]
+
+/-- If `as ++ [sep] ++ bs` has exactly one element satisfying `P` (namely `sep`),
+    then `splitOnPPrepend P (as ++ sep :: bs) acc` returns `[acc.reverse ++ as, bs]`. -/
+theorem splitOnPPrepend_one_sep (P : α → Bool) (as bs acc : List α) (sep : α)
+    (hsep : P sep = true) (has : ∀ x ∈ as, P x = false) (hbs : ∀ x ∈ bs, P x = false) :
+    List.splitOnPPrepend P (as ++ sep :: bs) acc = (acc.reverse ++ as) :: [bs] := by
+  induction as generalizing acc with
+  | nil =>
+    rw [List.nil_append, List.splitOnPPrepend_cons_eq_if, hsep]
+    rw [List.splitOnP_eq_splitOnPPrepend, splitOnPPrepend_no_sep P bs [] hbs]
+    simp
+  | cons a t ih =>
+    simp only [List.cons_append]
+    have ha : P a = false := has a (List.mem_cons.mpr (.inl rfl))
+    rw [List.splitOnPPrepend_cons_neg ha]
+    rw [ih (a :: acc) (fun x hx => has x (List.mem_cons.mpr (.inr hx)))]
+    simp [List.reverse_cons, List.append_assoc]
+
+/-- Splitting `s₁ ++ sep ++ s₂` on `sep` yields `[s₁, s₂]` when neither part contains `sep`. -/
+theorem splitToList_eq (s₁ s₂ : String) (p : Char → Bool) (sep : Char)
+    (hsep : p sep = true) (h₁ : ∀ c ∈ s₁.toList, p c = false)
+    (h₂ : ∀ c ∈ s₂.toList, p c = false) :
+    (s₁ ++ String.singleton sep ++ s₂).splitToList p = [s₁, s₂] := by
+  rw [String.splitToList_of_valid]
+  simp [String.toList_append, List.append_assoc]
+  rw [List.splitOnP_eq_splitOnPPrepend]
+  rw [splitOnPPrepend_one_sep p s₁.toList s₂.toList [] sep hsep h₁ h₂]
+  simp
+
+/-- Converse of `splitToList_eq`: if splitting `s` on `'.'` yields exactly two parts, then `s` is
+    their concatenation with the separator between them. Rejoining the split is the inverse of
+    splitting, so this recovers the rendering from the parser's view of a string. -/
+theorem join_splitToList {s left right : String}
+    (h : s.splitToList (· = '.') = [left, right]) :
+    s = left ++ "." ++ right := by
+  rw [String.splitToList_of_valid] at h
+  have hp : (fun x : Char => decide (x = '.')) = (fun x => x == '.') := by
+    funext x
+    apply Bool.eq_iff_iff.mpr
+    rw [decide_eq_true_eq, beq_iff_eq]
+  have hsplits : List.splitOn '.' s.toList = [left.toList, right.toList] := by
+    rw [List.splitOn_eq_splitOnP]
+    have h' := congrArg (List.map String.toList) h
+    simpa [Function.comp_def, hp] using h'
+  have hi := congrArg (List.intercalate ['.']) hsplits
+  rw [List.intercalate_splitOn] at hi
+  rw [← String.toList_inj]
+  simpa [List.intercalate] using hi
+
+/-! ==============================================================================================
+    # `toString`/`repr` of naturals contains no `'.'`
+    ============================================================================================== -/
+
+/-- No character in `toString n` is `'.'` (digits never produce a dot). -/
+theorem repr_no_dot (n : Nat) :
+    ∀ c ∈ (toString n).toList, (fun x : Char => decide (x = '.')) c = false := by
+  intro c hc; simp only [decide_eq_false_iff_not]; intro heq
+  have hc' : c ∈ (Nat.repr n).toList := by rwa [← Nat.toString_eq_repr]
+  have hc'' : c ∈ Nat.toDigits 10 n := by
+    rwa [Nat.repr_eq_ofList_toDigits, String.toList_ofList] at hc'
+  rw [heq] at hc''
+  exact absurd (Nat.isDigit_of_mem_toDigits (by omega) (by omega) hc'') (by decide)
+
+/-- No character in a zero-padded `toString n` string is `'.'`. -/
+theorem zeros_repr_no_dot (zeros : String) (n : Nat)
+    (hz : ∀ c ∈ zeros.toList, c = '0') :
+    ∀ c ∈ (zeros ++ toString n).toList, (fun x : Char => decide (x = '.')) c = false := by
+  intro c hc; rw [String.toList_append] at hc
+  simp only [decide_eq_false_iff_not]; intro heq
+  cases List.mem_append.mp hc with
+  | inl h => rw [hz c h] at heq; exact absurd heq (by decide)
+  | inr h =>
+    have := repr_no_dot n c h
+    simp [heq] at this
+
+/-! ==============================================================================================
+    # Digit-accumulating folds and `Nat.toDigits` roundtrip
+    ============================================================================================== -/
+
+/-- When no character in `l` is `'_'`, the underscore-skipping foldl reduces to the plain
+    digit-accumulating foldl. -/
+theorem foldl_no_underscore_eq (l : List Char) (acc : Nat)
+    (hno : ∀ c ∈ l, c ≠ '_') :
+    List.foldl (fun n c => if c = '_' then n else n * 10 + (c.toNat - 48)) acc l =
+    List.foldl (fun n c => n * 10 + (c.toNat - 48)) acc l := by
+  induction l generalizing acc with
+  | nil => rfl
+  | cons a t ih =>
+    simp only [List.foldl]
+    have ha : a ≠ '_' := hno a (List.Mem.head _)
+    simp only [ha, ↓reduceIte]
+    exact ih _ (fun c hc => hno c (List.Mem.tail _ hc))
+
+/-- The plain digit-accumulating foldl is equivalent to `Nat.ofDigitChars 10 l acc`. -/
+theorem foldl_eq_ofDigitChars (l : List Char) (acc : Nat) :
+    List.foldl (fun n c => n * 10 + (c.toNat - 48)) acc l =
+    Nat.ofDigitChars 10 l acc := by
+  rw [Nat.ofDigitChars_eq_foldl]
+  induction l generalizing acc with
+  | nil => rfl
+  | cons a t ih =>
+    simp only [List.foldl, show Char.toNat '0' = 48 from by rfl]
+    rw [Nat.mul_comm 10 acc]
+    exact ih _
+
+/-- Folding the underscore-skipping digit accumulator over `Nat.toDigits 10 n` recovers `n`. -/
+theorem toDigits_foldl_roundtrip (n : Nat) :
+    List.foldl (fun acc c => if c = '_' then acc else acc * 10 + (c.toNat - 48)) 0
+      (Nat.toDigits 10 n) = n := by
+  rw [foldl_no_underscore_eq _ 0 (fun c hc heq => Nat.underscore_not_in_toDigits (heq ▸ hc)),
+    foldl_eq_ofDigitChars]
+  exact Nat.ofDigitChars_toDigits (by omega) (by omega)
diff --git a/cedar-lean/Cedar/Thm/Ext/Decimal.lean b/cedar-lean/Cedar/Thm/Ext/Decimal.lean
new file mode 100644
index 000000000..af7f5f6f2
--- /dev/null
+++ b/cedar-lean/Cedar/Thm/Ext/Decimal.lean
@@ -0,0 +1,175 @@
+module
+
+public import Cedar.Thm.Ext.Decimal.Lemmas
+
+import all Cedar.Data.Int64
+import all Cedar.Spec.Ext.Decimal
+import all Cedar.Spec.Ext.Util
+import all Cedar.Thm.Ext.Decimal.Grammar
+import all Cedar.Thm.Ext.Decimal.Lemmas
+
+namespace Cedar.Thm.Decimal
+open Cedar.Spec.Ext
+
+/-- Completeness of `Decimal.parse`: if a string is well-formed and its computed value
+    matches `d.toInt`, then parsing accepts the string as `d`. -/
+public theorem parse_complete (s : String) (d : Decimal)
+    (hwf : IsWfDecimal s) (hval : computeValue s = some d.toInt) :
+    Decimal.parse s = some d := by
+  obtain ⟨left, right, h_split, h_ne, h_rpos, h_rle, h_lint, h_rnat⟩ := isWfDecimal_iff.mp hwf
+  unfold Decimal.parse
+  rw [h_split]
+  split
+  · rename_i heq; exact absurd ((List.cons.inj heq).1) h_ne
+  · rename_i _ _ _ heq; simp at heq; obtain ⟨hl', hr'⟩ := heq; subst hl'; subst hr'
+    simp only [show 0 < right.length ∧ right.length ≤ DECIMAL_DIGITS from ⟨h_rpos, h_rle⟩]
+    obtain ⟨l, hl⟩ := Option.isSome_iff_exists.mp h_lint
+    obtain ⟨r, hr⟩ := Option.isSome_iff_exists.mp h_rnat
+    simp only [hl, hr, Decimal.decimal?]
+    have hval' : (if !left.startsWith "-"
+        then l * Int.pow 10 DECIMAL_DIGITS + ↑r * Int.pow 10 (DECIMAL_DIGITS - right.length)
+        else l * Int.pow 10 DECIMAL_DIGITS - ↑r * Int.pow 10 (DECIMAL_DIGITS - right.length))
+        = d.toInt := by
+      have := hval
+      rw [computeValue_eq_parser_value hwf h_split hl hr] at this
+      exact Option.some.inj this
+    rw [hval']
+    exact Int64.ofInt?_toInt d
+  · rename_i h; exact (h left right rfl).elim
+
+/-- Parsing the canonical string representation of a decimal returns the same decimal. -/
+public theorem parse_toString_roundtrip (d : Decimal) :
+    Decimal.parse (toString d) = some d :=
+  parse_complete (toString d) d (toString_isWfDecimal d) (computeValue_toString d)
+
+/-- Failure characterization for `Decimal.parse`: parsing rejects exactly strings that are
+    not well-formed or whose computed value overflows the `Int64` range. -/
+public theorem parse_eq_none_iff (s : String) :
+    Decimal.parse s = none ↔ ¬ IsWfDecimal s ∨
+    ∃ v, computeValue s = some v ∧ (v < Int64.MIN ∨ v > Int64.MAX) := by
+  constructor
+  · -- → direction: parse s = none implies malformed or overflow
+    intro h
+    by_cases hwf : IsWfDecimal s
+    · -- s is well-formed, so it must be overflow
+      right
+      obtain ⟨left, right, h_split, h_ne, h_rpos, h_rle, h_lint, h_rnat⟩ := isWfDecimal_iff.mp hwf
+      obtain ⟨l, hl⟩ := Option.isSome_iff_exists.mp h_lint
+      obtain ⟨r, hr⟩ := Option.isSome_iff_exists.mp h_rnat
+      -- parse returned none despite well-formedness → decimal? returned none → overflow
+      unfold Decimal.parse at h
+      rw [h_split] at h
+      simp only [show 0 < right.length ∧ right.length ≤ DECIMAL_DIGITS from ⟨h_rpos, h_rle⟩,
+        hl, hr, Decimal.decimal?, ite_true, and_true] at h
+      -- h : Int64.ofInt? (if ... then ... + ... else ... - ...) = none
+      refine ⟨_, ?_, Int64.ofInt?_none_iff.mpr h⟩
+      exact computeValue_eq_parser_value hwf h_split hl hr
+    · left; exact hwf
+  · -- ← direction: malformed or overflow implies parse s = none
+    intro h
+    rcases h with h | ⟨v, hcv, hovf⟩
+    · -- ¬ IsWfDecimal s → parse s = none
+      by_contra hne
+      have ⟨d, hd⟩ := Option.ne_none_iff_exists'.mp hne
+      exact absurd (parse_some_isWfDecimal s d hd) h
+    · -- overflow → parse s = none
+      -- If s is not well-formed, parse = none trivially
+      by_cases hwf : IsWfDecimal s
+      · -- s is well-formed but overflows
+        obtain ⟨left, right, h_split, h_ne, h_rpos, h_rle, h_lint, h_rnat⟩ := isWfDecimal_iff.mp hwf
+        obtain ⟨l, hl⟩ := Option.isSome_iff_exists.mp h_lint
+        obtain ⟨r, hr⟩ := Option.isSome_iff_exists.mp h_rnat
+        unfold Decimal.parse
+        rw [h_split]
+        simp only [show 0 < right.length ∧ right.length ≤ DECIMAL_DIGITS from ⟨h_rpos, h_rle⟩,
+          hl, hr, Decimal.decimal?, ite_true, and_true]
+        -- Goal: Int64.ofInt? (if ... then ... else ...) = none
+        -- computeValue s = some v is out of range, and equals this branching expression
+        have hcv' : (if !left.startsWith "-"
+            then l * Int.pow 10 DECIMAL_DIGITS + ↑r * Int.pow 10 (DECIMAL_DIGITS - right.length)
+            else l * Int.pow 10 DECIMAL_DIGITS - ↑r * Int.pow 10 (DECIMAL_DIGITS - right.length))
+            = v := by
+          have := hcv
+          rw [computeValue_eq_parser_value hwf h_split hl hr] at this
+          exact Option.some.inj this
+        rw [hcv']
+        exact Int64.ofInt?_none_iff.mp hovf
+      · -- s is not well-formed → parse = none (same as the other branch)
+        by_contra hne
+        have ⟨d, hd⟩ := Option.ne_none_iff_exists'.mp hne
+        exact absurd (parse_some_isWfDecimal s d hd) hwf
+
+where
+  parse_some_isWfDecimal (s : String) (d : Decimal) (h : Decimal.parse s = some d) : IsWfDecimal s := by
+    unfold Decimal.parse at h
+    split at h
+    · exact absurd h (by simp)
+    · rename_i left right h_ne h_split
+      split at h
+      · rename_i l r heq_l heq_r
+        have h_len : 0 < right.length ∧ right.length ≤ DECIMAL_DIGITS := by
+          by_contra hc; simp [hc] at h
+        exact isWfDecimal_iff.mpr ⟨left, right, h_split, h_ne, h_len.1, h_len.2,
+          by rw [heq_l]; rfl, by rw [heq_r]; rfl⟩
+      · simp at h
+    · simp at h
+
+/-- Soundness of `Decimal.parse`: if parsing succeeds, then the input is well-formed and its
+    computed value is exactly the returned decimal's value. (The value is automatically in `Int64`
+    range, since `d : Decimal = Int64`, so no range conjunct is stated.) -/
+public theorem parse_sound (s : String) (d : Decimal) (h : Decimal.parse s = some d) :
+    IsWfDecimal s ∧ computeValue s = some d.toInt := by
+  -- parse succeeded, so `parse_eq_none_iff` rules out both malformedness and overflow.
+  have hnot_bad : ¬ (¬ IsWfDecimal s ∨
+      ∃ v, computeValue s = some v ∧ (v < Int64.MIN ∨ v > Int64.MAX)) := by
+    intro hbad
+    have hnone := (parse_eq_none_iff s).mpr hbad
+    simp [h] at hnone
+  have hwf : IsWfDecimal s := by
+    by_contra hnwf
+    exact hnot_bad (Or.inl hnwf)
+  -- well-formed ⇒ `computeValue s = some v` for some value `v`.
+  obtain ⟨v, hv⟩ := Option.isSome_iff_exists.mp (computeValue_isSome_of_isWfDecimal hwf)
+  have hnot_ovf : ¬ (v < Int64.MIN ∨ v > Int64.MAX) := fun hovf =>
+    hnot_bad (Or.inr ⟨v, hv, hovf⟩)
+  have hmin : Int64.MIN ≤ v := by omega
+  have hmax : v ≤ Int64.MAX := by omega
+  -- reconstruct the decimal from `v` and show it is exactly `d`.
+  let d' : Decimal := Int64.ofInt v
+  have hd'_toInt : d'.toInt = v := by
+    dsimp [d']
+    exact Int64.toInt_ofInt_of_le
+      (by simp only [Int64.MIN] at hmin ⊢; omega)
+      (by simp only [Int64.MAX] at hmax ⊢; omega)
+  have hparse' : Decimal.parse s = some d' :=
+    parse_complete s d' hwf (by rw [hv, hd'_toInt])
+  have hd_eq : d = d' := by
+    rw [h] at hparse'
+    exact Option.some.inj hparse'
+  exact ⟨hwf, by rw [hv, hd_eq, hd'_toInt]⟩
+
+/-- `toString` is injective: distinct decimals produce distinct strings. -/
+public theorem toString_injective (d d' : Decimal) (h : toString d = toString d') : d = d' := by
+  have h1 := parse_toString_roundtrip d
+  have h2 := parse_toString_roundtrip d'
+  rw [h] at h1
+  rw [h1] at h2
+  injection h2
+
+/-- Equal normal form iff equal value: normalization decides decimal equality. -/
+public theorem normalize_eq_iff_parse_eq (s s' : String) :
+    normalize s = normalize s' ↔ Decimal.parse s = Decimal.parse s' := by
+  constructor
+  · intro h
+    unfold normalize at h
+    match hps : Decimal.parse s, hps' : Decimal.parse s' with
+    | .some d, .some d' =>
+      simp [hps, hps', Option.map] at h
+      exact congrArg _ (toString_injective d d' h)
+    | .some d, .none => simp [hps, hps', Option.map] at h
+    | .none, .some d' => simp [hps, hps', Option.map] at h
+    | .none, .none => rfl
+  · intro h
+    simp [normalize, h]
+
+end Cedar.Thm.Decimal
diff --git a/cedar-lean/Cedar/Thm/Ext/Decimal/Grammar.lean b/cedar-lean/Cedar/Thm/Ext/Decimal/Grammar.lean
new file mode 100644
index 000000000..11a4044a7
--- /dev/null
+++ b/cedar-lean/Cedar/Thm/Ext/Decimal/Grammar.lean
@@ -0,0 +1,78 @@
+module
+
+public import Cedar.Spec.Ext.Decimal
+public import Std.Data.String
+public import Cedar.Thm.Data.String
+
+import all Cedar.Spec.Ext.Decimal
+import all Cedar.Spec.Ext.Util
+
+namespace Cedar.Thm.Decimal
+open Cedar.Spec.Ext
+
+/-! # Decimal grammar: definitions
+
+This file contains only the grammar-level definitions — the well-formedness predicates and the
+value function — as a direct, parser-independent transcription of the decimal grammar. Each
+production becomes a predicate, and `IsWfDecimal` says the string is their rendering. The lemmas
+connecting these definitions to `Decimal.parse` (in particular the digit-string ↔
+`toInt?'`/`toNat?'` bridges) live in `Cedar.Thm.Ext.Decimal.Lemmas`.
+
+`Sign ::= ['-']` uses the shared `IsWfSign` predicate. The decimal-specific `Natural` and
+`Fraction` productions are named locally using the shared digit predicates `IsDigits` and
+`IsDigitsUpTo`; their string-to-number bridges live in `Cedar.Thm.Data.String`. -/
+
+/-- The grammar's `Natural ::= Digit⁺`: the unsigned natural-number production. An `abbrev` for
+    the shared `IsDigits` predicate, so every `IsDigits` lemma applies without unfolding. -/
+-- ANCHOR: IsNatural
+public abbrev IsNatural (s : String) : Prop := IsDigits s
+-- ANCHOR_END: IsNatural
+
+/-- The grammar's `Fraction ::= Digit{1,4}`: 1 to `DECIMAL_DIGITS` digits, an instance of the
+    shared bounded-digits predicate. -/
+-- ANCHOR: IsWfFrac
+public def IsWfFrac (s : String) : Prop :=
+  IsDigitsUpTo DECIMAL_DIGITS s
+-- ANCHOR_END: IsWfFrac
+
+/-- Well-formed decimal syntax: `s` is the rendering of a well-formed `Sign ::= ['-']`,
+    `Natural ::= Digit⁺`, `'.'`, and `Fraction ::= Digit{1,4}`, concatenated in that order.
+    Phrasing well-formedness existentially over the rendering bakes in the separator and field
+    order without introducing a record for this single flat production. This is a direct
+    transcription of the grammar's character-level productions, independent of any
+    string-to-number parser. -/
+-- ANCHOR: IsWfDecimal
+public def IsWfDecimal (s : String) : Prop :=
+  ∃ sign natural fraction,
+    s = sign ++ natural ++ "." ++ fraction ∧
+    IsWfSign sign ∧
+    IsNatural natural ∧
+    IsWfFrac fraction
+-- ANCHOR_END: IsWfDecimal
+
+/-- Compute the integer value that a decimal string represents, or `none` if its unsigned body
+    does not split into parsable `Natural` and `Fraction` fields. This directly implements the
+    grammar's value function:
+
+      value = sign × (nat(Natural) × 10⁴ + nat(Fraction) × 10^(4 − |Fraction|))
+      where sign = −1 if Sign is '-', else 1
+ -/
+-- ANCHOR: computeValue
+public def computeValue (s : String) : Option Int :=
+  let (sign, body) :=
+    if s.front = '-' then ((-1 : Int), (s.drop 1).copy) else (1, s)
+  match body.splitToList (· = '.') with
+  | [natural, fraction] =>
+    match toNat?' natural, toNat?' fraction with
+    | some n, some f =>
+      some (sign * (n * Int.pow 10 DECIMAL_DIGITS
+        + f * Int.pow 10 (DECIMAL_DIGITS - fraction.length)))
+    | _, _ => none
+  | _ => none
+-- ANCHOR_END: computeValue
+
+/-- Canonical-form normalizer: parse the string and re-serialize.
+    Returns `none` for malformed or out-of-range inputs. -/
+public def normalize (s : String) : Option String := (Decimal.parse s).map toString
+
+end Cedar.Thm.Decimal
diff --git a/cedar-lean/Cedar/Thm/Ext/Decimal/Lemmas.lean b/cedar-lean/Cedar/Thm/Ext/Decimal/Lemmas.lean
new file mode 100644
index 000000000..a84a77412
--- /dev/null
+++ b/cedar-lean/Cedar/Thm/Ext/Decimal/Lemmas.lean
@@ -0,0 +1,561 @@
+module
+
+public import Cedar.Thm.Ext.Decimal.Grammar
+
+import all Cedar.Data.Int64
+import all Cedar.Spec.Ext.Decimal
+import all Cedar.Spec.Ext.Util
+import all Cedar.Thm.Data.String
+import all Cedar.Thm.Ext.Decimal.Grammar
+import all Init.Data.Nat.ToString
+import all Init.Data.String.Search
+import all Init.Data.String.Slice
+
+namespace Cedar.Thm.Decimal
+open Cedar.Spec.Ext
+
+/-! ============================================================================================
+    # Grammar ↔ parser bridge lemmas
+
+    `IsWfDecimal` is phrased over the grammar's productions (`IsWfSign`/`IsNatural`/`IsWfFrac`) as
+    a rendering `sign ++ natural ++ "." ++ fraction`. `computeValue` strips that outer sign and
+    parses the two unsigned fields, while `Decimal.parse` splits first and parses the signed left
+    field through `toInt?'`. These lemmas connect the views: the rendering splits back into its
+    parts, a digit string is exactly one the stdlib parser accepts, and both value expressions are
+    equal on well-formed inputs. They let the soundness/completeness proofs move between the
+    grammar view and the parser view.
+
+    The `IsDigits` predicate and its `toNat?'` bridges (`no_underscore_of_isDigits`,
+    `isNat_of_isDigits`, `isDigits_of_isNat`, `toNat?'_isSome_of_isDigits`,
+    `isDigits_of_toNat?'_isSome`) are shared with the duration grammar and live in
+    `Cedar.Thm.Data.String`; the integer-specific lemmas below build on them.
+    ============================================================================================ -/
+
+/-- The concatenation of a well-formed `Sign` and `Natural` — the grammar's integer part —
+    contains no `'_'`. -/
+theorem no_underscore_of_sign_nat {sign natural : String}
+    (hs : IsWfSign sign) (hn : IsDigits natural) : (sign ++ natural).contains '_' = false := by
+  obtain ⟨_, hnd⟩ := hn
+  have hnot : ¬ ('_' ∈ (sign ++ natural).toList) := by
+    rw [String.toList_append]; intro hm
+    cases List.mem_append.mp hm with
+    | inl h => rcases hs with rfl | rfl <;> simp at h
+    | inr h => have := hnd '_' h; simp at this
+  simpa [String.contains] using hnot
+
+/-- Forward bridge (integer): a well-formed `Sign` followed by a `Natural` parses as an integer. -/
+theorem toInt?'_isSome_of_sign_nat {sign natural : String}
+    (hs : IsWfSign sign) (hn : IsDigits natural) :
+    (toInt?' (sign ++ natural)).isSome = true := by
+  unfold toInt?'
+  rw [no_underscore_of_sign_nat hs hn]
+  simp only [Bool.false_eq_true, ↓reduceIte]
+  rw [show (sign ++ natural).toInt?.isSome = (sign ++ natural).isInt from String.isSome_toInt?,
+    String.isInt_iff]
+  rcases hs with rfl | rfl
+  · right; exact ⟨natural, rfl, isNat_of_isDigits hn⟩
+  · left; simpa using isNat_of_isDigits hn
+
+/-- Backward bridge (integer): anything `toInt?'` accepts splits into a well-formed `Sign` and
+    `Natural`. -/
+theorem sign_nat_of_toInt?'_isSome {s : String} (h : (toInt?' s).isSome = true) :
+    ∃ sign natural, s = sign ++ natural ∧ IsWfSign sign ∧ IsDigits natural := by
+  unfold toInt?' at h
+  split at h
+  · simp at h
+  · rename_i hnc
+    rw [Bool.not_eq_true] at hnc
+    rw [show s.toInt?.isSome = s.isInt from String.isSome_toInt?, String.isInt_iff] at h
+    rcases h with hnat | ⟨t, hst, htnat⟩
+    · exact ⟨"", s, by simp, Or.inr rfl, isDigits_of_isNat hnat hnc⟩
+    · refine ⟨"-", t, hst, Or.inl rfl, ?_⟩
+      have hnct : t.contains '_' = false := by
+        by_contra hc
+        rw [Bool.not_eq_false] at hc
+        have ht : '_' ∈ t.toList := by simpa [String.contains] using hc
+        have hs : '_' ∈ s.toList := by
+          rw [hst, String.toList_append]; exact List.mem_append_right _ ht
+        have hcontains : s.contains '_' = true := by simpa [String.contains] using hs
+        rw [hcontains] at hnc; simp at hnc
+      exact isDigits_of_isNat htnat hnct
+
+/-- A well-formed integer part is never a bare `"-"`: the grammar's `Digit⁺` requires at least one
+    digit after the sign. This is what the `left ≠ "-"` side condition asserts explicitly. -/
+theorem ne_dash_of_sign_nat {sign natural : String}
+    (hs : IsWfSign sign) (hn : IsDigits natural) : sign ++ natural ≠ "-" := by
+  obtain ⟨hlen, hdig⟩ := hn
+  rcases hs with rfl | rfl
+  · intro hEq
+    have ht : natural = "" := by
+      have hl := congrArg String.length hEq
+      simp only [String.length_append] at hl
+      have h1 : ("-" : String).length = 1 := by decide
+      rw [h1] at hl
+      have hz : natural.length = 0 := by omega
+      rw [← String.length_toList] at hz
+      rw [← String.toList_inj]; simpa using List.eq_nil_of_length_eq_zero hz
+    rw [ht] at hlen; simp at hlen
+  · intro hEq
+    simp only [String.empty_append] at hEq
+    subst hEq
+    have := hdig '-' (by decide); simp at this
+
+/-- A digit string contains no `'.'` — the separator can only appear where the grammar puts it. -/
+theorem no_dot_of_isDigits {s : String} (h : IsDigits s) :
+    ∀ c ∈ s.toList, decide (c = '.') = false := by
+  intro c hc
+  simp only [decide_eq_false_iff_not]
+  intro heq; subst c
+  have := h.2 '.' hc; simp at this
+
+/-- The grammar's integer part contains no `'.'`. -/
+theorem no_dot_of_sign_nat {sign natural : String}
+    (hs : IsWfSign sign) (hn : IsDigits natural) :
+    ∀ c ∈ (sign ++ natural).toList, decide (c = '.') = false := by
+  intro c hc
+  rw [String.toList_append] at hc
+  cases List.mem_append.mp hc with
+  | inl h =>
+    rcases hs with rfl | rfl
+    · have hc' : c = '-' := by simpa using h
+      subst hc'; decide
+    · simp at h
+  | inr h => exact no_dot_of_isDigits hn c h
+
+/-- Splitting a well-formed rendering on `'.'` recovers the integer part and the fraction: the
+    only `'.'` in `sign ++ natural ++ "." ++ fraction` is the separator the grammar writes. -/
+theorem splitToList_of_isWfDecimal {sign natural fraction : String}
+    (hs : IsWfSign sign) (hn : IsDigits natural) (hf : IsWfFrac fraction) :
+    (sign ++ natural ++ "." ++ fraction).splitToList (· = '.') = [sign ++ natural, fraction] :=
+  splitToList_eq (sign ++ natural) fraction (· = '.') '.' (by decide)
+    (no_dot_of_sign_nat hs hn) (no_dot_of_isDigits hf.1)
+
+private theorem dash_append_front_eq_dash (body : String) :
+    ("-" ++ body).front = '-' := by
+  simp [String.front_eq, String.front?_eq, String.toList_append]
+
+private theorem dash_append_drop_one_copy (body : String) :
+    (("-" ++ body).drop 1).copy = body := by
+  apply String.ext
+  simp [String.toList_append]
+
+private theorem startsWith_dash_eq_false_of_isDigits {natural : String}
+    (hn : IsDigits natural) : natural.startsWith "-" = false := by
+  apply Bool.eq_false_iff.mpr
+  intro h
+  cases hs : natural.toList with
+  | nil =>
+    have hp := hn.1
+    rw [← String.length_toList, hs] at hp
+    simp at hp
+  | cons c cs =>
+    have hc : c.isDigit = true := hn.2 c (by rw [hs]; simp)
+    have hceq : c = '-' := by
+      have hcopy : natural = String.ofList (c :: cs) := by
+        rw [← String.toList_inj, hs, String.toList_ofList]
+      rw [hcopy] at h
+      simp at h
+      exact h.symm
+    rw [hceq] at hc
+    simp at hc
+
+private theorem front_ne_dash_of_isDigits_append {natural fraction : String}
+    (hn : IsDigits natural) : (natural ++ "." ++ fraction).front ≠ '-' := by
+  intro h
+  cases hs : natural.toList with
+  | nil =>
+    have hp := hn.1
+    rw [← String.length_toList, hs] at hp
+    simp at hp
+  | cons c cs =>
+    have hc : c.isDigit = true := hn.2 c (by rw [hs]; simp)
+    have hceq : c = '-' := by
+      simpa [String.front_eq, String.front?_eq, String.toList_append, hs] using h
+    rw [hceq] at hc
+    simp at hc
+
+private theorem toInt?'_eq_some_of_toNat?' {natural : String} {n : Nat}
+    (hn : IsDigits natural) (h : toNat?' natural = some n) :
+    toInt?' natural = some (n : Int) := by
+  unfold toInt?' toNat?' at *
+  rw [no_underscore_of_isDigits hn]
+  rw [no_underscore_of_isDigits hn] at h
+  simp only [Bool.false_eq_true, ↓reduceIte] at h ⊢
+  rw [String.toInt?, String.Slice.toInt?_eq_some_iff]
+  left
+  exact ⟨n, by rwa [String.toNat?_toSlice], rfl⟩
+
+private theorem toInt?'_dash_eq_some_of_toNat?' {natural : String} {n : Nat}
+    (hn : IsDigits natural) (h : toNat?' natural = some n) :
+    toInt?' ("-" ++ natural) = some (-(n : Int)) := by
+  unfold toInt?' toNat?' at *
+  rw [no_underscore_of_isDigits hn] at h
+  have hno : ("-" ++ natural).contains '_' = false :=
+    no_underscore_of_sign_nat (Or.inl rfl) hn
+  rw [hno]
+  simp only [Bool.false_eq_true, ↓reduceIte] at h ⊢
+  rw [String.toInt?, String.Slice.toInt?_eq_some_iff]
+  right
+  refine ⟨natural, ?_, n, h, rfl⟩
+  rw [String.copy_toSlice]
+
+/-- `IsWfDecimal` restated in the parser-primitive form the parse proofs consume: the rendering
+    becomes a split on `'.'`, the digit-string clauses become `(toInt?'/toNat?').isSome`, and
+    `left ≠ "-"` / `0 < right.length` fall out of the grammar's `Digit⁺` productions. -/
+theorem isWfDecimal_iff {s : String} :
+    IsWfDecimal s ↔
+      ∃ left right,
+        s.splitToList (· = '.') = [left, right] ∧
+        left ≠ "-" ∧
+        0 < right.length ∧
+        right.length ≤ DECIMAL_DIGITS ∧
+        (toInt?' left).isSome ∧
+        (toNat?' right).isSome := by
+  constructor
+  · rintro ⟨sign, natural, fraction, rfl, hs, hn, hf⟩
+    exact ⟨sign ++ natural, fraction, splitToList_of_isWfDecimal hs hn hf,
+      ne_dash_of_sign_nat hs hn, hf.1.1, hf.2,
+      toInt?'_isSome_of_sign_nat hs hn, toNat?'_isSome_of_isDigits hf.1⟩
+  · rintro ⟨left, right, h_split, _, _, h_rle, h_lint, h_rnat⟩
+    obtain ⟨sign, natural, rfl, hs, hn⟩ := sign_nat_of_toInt?'_isSome h_lint
+    refine ⟨sign, natural, right, ?_, hs, hn,
+      ⟨isDigits_of_toNat?'_isSome h_rnat, h_rle⟩⟩
+    have hjoin := join_splitToList h_split
+    simp only [String.append_assoc] at hjoin ⊢
+    exact hjoin
+
+/-- On a well-formed input, the grammar's outer-sign value equals the parser's expression, which
+    reads the sign together with the left field and branches between adding and subtracting the
+    fraction. -/
+theorem computeValue_eq_parser_value {s left right : String} {l : Int} {r : Nat}
+    (hwf : IsWfDecimal s)
+    (h_split : s.splitToList (· = '.') = [left, right])
+    (hl : toInt?' left = some l) (hr : toNat?' right = some r) :
+    computeValue s = some (if !left.startsWith "-"
+      then l * Int.pow 10 DECIMAL_DIGITS + r * Int.pow 10 (DECIMAL_DIGITS - right.length)
+      else l * Int.pow 10 DECIMAL_DIGITS - r * Int.pow 10 (DECIMAL_DIGITS - right.length)) := by
+  obtain ⟨sign, natural, fraction, hs, hsign, hn, hf⟩ := hwf
+  have hparts : left = sign ++ natural ∧ right = fraction := by
+    have h := h_split
+    rw [hs, splitToList_of_isWfDecimal hsign hn hf] at h
+    exact ⟨(List.cons.inj h).1.symm, (List.cons.inj (List.cons.inj h).2).1.symm⟩
+  rcases hparts with ⟨rfl, rfl⟩
+  obtain ⟨n, hnat⟩ := Option.isSome_iff_exists.mp (toNat?'_isSome_of_isDigits hn)
+  have hbody_split :
+      (natural ++ "." ++ right).splitToList (· = '.') = [natural, right] :=
+    splitToList_eq natural right (· = '.') '.' (by decide)
+      (no_dot_of_isDigits hn) (no_dot_of_isDigits hf.1)
+  rcases hsign with rfl | rfl
+  · have hl' := toInt?'_dash_eq_some_of_toNat?' hn hnat
+    rw [hl'] at hl
+    injection hl with hl
+    subst l
+    rw [hs]
+    rw [show "-" ++ natural ++ "." ++ right = "-" ++ (natural ++ "." ++ right) by
+      simp [String.append_assoc]]
+    unfold computeValue
+    rw [dash_append_front_eq_dash, if_pos rfl, dash_append_drop_one_copy]
+    simp only
+    rw [hbody_split]
+    simp only
+    rw [hnat, hr]
+    simp [Int.sub_eq_add_neg, Int.neg_add, Int.neg_mul]
+  · simp only [String.empty_append] at hl hs ⊢
+    have hl' := toInt?'_eq_some_of_toNat?' hn hnat
+    rw [hl'] at hl
+    injection hl with hl
+    subst l
+    rw [hs]
+    have hfront := front_ne_dash_of_isDigits_append (fraction := right) hn
+    have hstarts := startsWith_dash_eq_false_of_isDigits hn
+    unfold computeValue
+    rw [if_neg hfront]
+    simp only
+    rw [hbody_split]
+    simp only
+    rw [hnat, hr]
+    simp [hstarts]
+
+/-- A well-formed string always has a computed value: `computeValue` succeeds because both the
+    parser split and numeric primitives succeed. (The converse fails: `computeValue` can succeed
+    on strings that violate the `right.length ≤ DECIMAL_DIGITS` bound.) -/
+theorem computeValue_isSome_of_isWfDecimal {s : String} (h : IsWfDecimal s) :
+    (computeValue s).isSome = true := by
+  obtain ⟨left, right, h_split, _, _, _, h_lint, h_rnat⟩ := isWfDecimal_iff.mp h
+  obtain ⟨l, hl⟩ := Option.isSome_iff_exists.mp h_lint
+  obtain ⟨r, hr⟩ := Option.isSome_iff_exists.mp h_rnat
+  rw [computeValue_eq_parser_value h h_split hl hr]
+  rfl
+
+/-! ============================================================================================
+    # `toString` well-formedness and value
+    ============================================================================================ -/
+
+/-- Prepending zero characters to a natural number's string representation does not change
+    the value accepted by `toNat?'`. -/
+private theorem zeroPad_toNat? (pad : String) (n : Nat)
+    (hp : ∀ c ∈ pad.toList, c = '0') :
+    toNat?' (pad ++ toString n) = some n := by
+  simp only [toNat?']
+  have hno_us : (pad ++ toString n).contains '_' = false := by
+    have h : ¬ ('_' ∈ (pad ++ toString n).toList) := by
+      rw [String.toList_append]
+      intro h
+      cases List.mem_append.mp h with
+      | inl h => exact absurd (hp '_' h) (by decide)
+      | inr h =>
+        rw [Nat.toString_eq_repr, Nat.toList_repr] at h
+        exact Nat.underscore_not_in_toDigits h
+    simpa [String.contains] using h
+  rw [hno_us]
+  simp [String.toNat?, String.Slice.toNat?]
+  simp [String.isNat_iff]
+  refine ⟨?_, ?_⟩
+  · refine ⟨?_, ?_, ?_, ?_⟩
+    · intro c hc
+      cases hc with
+      | inl h =>
+        left
+        rw [hp c h]
+        rfl
+      | inr h =>
+        left
+        exact Nat.isDigit_of_mem_toDigits (by omega) (by omega) h
+    · intro hsub
+      rcases hsub with ⟨s, t, ht⟩
+      have hmem : '_' ∈ pad.toList ++ Nat.toDigits 10 n := by
+        rw [← ht]
+        simp [List.mem_append, List.mem_cons]
+      cases List.mem_append.mp hmem with
+      | inl h => exact absurd (hp '_' h) (by decide)
+      | inr h => exact Nat.underscore_not_in_toDigits h
+    · refine ⟨?_, ?_⟩
+      · intro hhead
+        cases hlist : pad.toList with
+        | nil => simp [hlist] at hhead
+        | cons c cs =>
+          have hc : c = '0' := hp c (by rw [hlist]; exact List.Mem.head _)
+          simp [hlist] at hhead
+          rw [hhead] at hc
+          exact absurd hc (by decide)
+      · intro _ hhead
+        have hmem : '_' ∈ Nat.toDigits 10 n := by
+          cases hlist : Nat.toDigits 10 n with
+          | nil => simp [hlist] at hhead
+          | cons c cs =>
+            simp [hlist] at hhead
+            rw [← hhead]
+            exact List.Mem.head _
+        exact Nat.underscore_not_in_toDigits hmem
+    · intro hlast
+      have hne : Nat.toDigits 10 n ≠ [] := Nat.toDigits_ne_nil
+      rw [List.getLast?_eq_some_getLast hne] at hlast
+      have hmem := List.getLast_mem hne
+      injection hlast with hlast
+      rw [hlast] at hmem
+      exact Nat.underscore_not_in_toDigits hmem
+  · have hpad_fold : ∀ l, (∀ c ∈ l, c = '0') →
+        List.foldl (fun n c => if c = '_' then n else n * 10 + (c.toNat - 48)) 0 l = 0 := by
+      intro l hz
+      induction l with
+      | nil => rfl
+      | cons c cs ih =>
+        have hc : c = '0' := hz c (List.Mem.head _)
+        have hcs : ∀ x ∈ cs, x = '0' := fun x hx => hz x (List.Mem.tail _ hx)
+        simp [List.foldl, hc, ih hcs]
+    rw [hpad_fold pad.toList hp]
+    exact toDigits_foldl_roundtrip n
+
+/-- Decomposes `toString d` into its left (integer) and right (fractional) parts, establishing
+    their split structure, right-part length, parsability, and sign behavior. -/
+private theorem toString_split (d : Decimal) :
+    let leftPart := (if d < 0 then "-" else "") ++ toString (d.natAbs / Nat.pow 10 4)
+    let rightNat := d.natAbs % Nat.pow 10 4
+    let rightPart :=
+      if rightNat < 10 then "000" ++ toString rightNat
+      else if rightNat < 100 then "00" ++ toString rightNat
+      else if rightNat < 1000 then "0" ++ toString rightNat
+      else toString rightNat
+    (toString d).splitToList (· = '.') = [leftPart, rightPart] ∧
+    rightPart.length = 4 ∧
+    toInt?' leftPart = some (if d < 0 then -(↑(d.natAbs / Nat.pow 10 4) : Int)
+      else (↑(d.natAbs / Nat.pow 10 4) : Int)) ∧
+    toNat?' rightPart = some rightNat ∧
+    (!leftPart.startsWith "-") = !(d < 0) := by
+  intro leftPart rightNat rightPart
+  refine ⟨?_, ?_, ?_, ?_, ?_⟩
+  · -- splitToList
+    have h_left_no_dot : ∀ c ∈ leftPart.toList,
+        (fun x : Char => decide (x = '.')) c = false := by
+      intro c hc; simp only [leftPart, String.toList_append] at hc
+      simp only [decide_eq_false_iff_not]; intro heq
+      cases List.mem_append.mp hc with
+      | inl h =>
+        split at h
+        · simp at h; rw [h] at heq; exact absurd heq (by decide)
+        · simp at h
+      | inr h => exact absurd (repr_no_dot _ c h) (by simp [heq])
+    have h_right_no_dot : ∀ c ∈ rightPart.toList,
+        (fun x : Char => decide (x = '.')) c = false := by
+      intro c hc; simp only [rightPart] at hc
+      split at hc
+      · exact zeros_repr_no_dot "000" _ (by simp) c hc
+      · split at hc
+        · exact zeros_repr_no_dot "00" _ (by simp) c hc
+        · split at hc
+          · exact zeros_repr_no_dot "0" _ (by simp) c hc
+          · exact repr_no_dot _ c hc
+    have h_toString : toString d = leftPart ++ String.singleton '.' ++ rightPart := by
+      show leftPart ++ (if rightNat < 10 then ".000" ++ toString rightNat
+        else if rightNat < 100 then ".00" ++ toString rightNat
+        else if rightNat < 1000 then ".0" ++ toString rightNat
+        else "." ++ toString rightNat) = leftPart ++ String.singleton '.' ++ rightPart
+      simp only [rightPart, String.append_assoc]; congr 1
+      split
+      · rfl
+      · split
+        · rfl
+        · split
+          · rfl
+          · rfl
+    rw [h_toString]
+    exact splitToList_eq leftPart rightPart _ '.' (by rfl) h_left_no_dot h_right_no_dot
+  · -- rightPart.length = 4
+    simp only [rightPart, rightNat]
+    split
+    · have : ("000" : String).length = 3 := by rfl
+      have : (d.natAbs % Nat.pow 10 4).repr.length = 1 := by
+        rw [Nat.repr_eq_ofList_toDigits, String.length_ofList, Nat.toDigits,
+          show d.natAbs % Nat.pow 10 4 + 1 = Nat.succ (d.natAbs % Nat.pow 10 4) from rfl,
+          Nat.toDigitsCore.eq_def]
+        simp [show d.natAbs % Nat.pow 10 4 / 10 = 0 from by omega]
+      simp [*]
+    · split
+      · have : ("00" : String).length = 2 := by rfl
+        have : (d.natAbs % Nat.pow 10 4).repr.length = 2 := by
+          rw [Nat.repr_eq_ofList_toDigits, String.length_ofList, Nat.toDigits,
+            show d.natAbs % Nat.pow 10 4 + 1 = Nat.succ (d.natAbs % Nat.pow 10 4) from rfl,
+            Nat.toDigitsCore.eq_def]
+          simp only [show d.natAbs % Nat.pow 10 4 / 10 ≠ 0 from by omega]
+          rw [show d.natAbs % Nat.pow 10 4 = Nat.succ (d.natAbs % Nat.pow 10 4 - 1) from by omega,
+            Nat.toDigitsCore.eq_def]
+          simp [show (d.natAbs % Nat.pow 10 4 - 1).succ / 10 / 10 = 0 from by omega]
+        simp [*]
+      · split
+        · have : ("0" : String).length = 1 := by rfl
+          have : (d.natAbs % Nat.pow 10 4).repr.length = 3 := by
+            rw [Nat.repr_eq_ofList_toDigits, String.length_ofList, Nat.toDigits,
+              show d.natAbs % Nat.pow 10 4 + 1 = Nat.succ (d.natAbs % Nat.pow 10 4) from rfl,
+              Nat.toDigitsCore.eq_def]
+            simp only [show d.natAbs % Nat.pow 10 4 / 10 ≠ 0 from by omega]
+            rw [show d.natAbs % Nat.pow 10 4 = Nat.succ (d.natAbs % Nat.pow 10 4 - 1) from by omega,
+              Nat.toDigitsCore.eq_def]
+            simp only [show (d.natAbs % Nat.pow 10 4 - 1).succ / 10 / 10 ≠ 0 from by omega, ↓reduceIte]
+            rw [show (d.natAbs % Nat.pow 10 4 - 1) = Nat.succ (d.natAbs % Nat.pow 10 4 - 2) from by omega,
+              Nat.toDigitsCore.eq_def]
+            simp [show (d.natAbs % Nat.pow 10 4 - 2).succ.succ / 10 / 10 / 10 = 0 from by omega]
+          simp [*]
+        · have : (d.natAbs % Nat.pow 10 4).repr.length = 4 := by
+            rw [Nat.repr_eq_ofList_toDigits, String.length_ofList, Nat.toDigits,
+              show d.natAbs % Nat.pow 10 4 + 1 = Nat.succ (d.natAbs % Nat.pow 10 4) from rfl,
+              Nat.toDigitsCore.eq_def]
+            simp only [show d.natAbs % Nat.pow 10 4 / 10 ≠ 0 from by omega]
+            rw [show d.natAbs % Nat.pow 10 4 = Nat.succ (d.natAbs % Nat.pow 10 4 - 1) from by omega,
+              Nat.toDigitsCore.eq_def]
+            simp only [show (d.natAbs % Nat.pow 10 4 - 1).succ / 10 / 10 ≠ 0 from by omega]
+            rw [show (d.natAbs % Nat.pow 10 4 - 1) = Nat.succ (d.natAbs % Nat.pow 10 4 - 2) from by omega,
+              Nat.toDigitsCore.eq_def]
+            simp only [show (d.natAbs % Nat.pow 10 4 - 2).succ.succ / 10 / 10 / 10 ≠ 0 from by omega]
+            rw [show (d.natAbs % Nat.pow 10 4 - 2) = Nat.succ (d.natAbs % Nat.pow 10 4 - 3) from by omega,
+              Nat.toDigitsCore.eq_def]
+            simp [show (d.natAbs % Nat.pow 10 4 - 3).succ.succ.succ / 10 / 10 / 10 / 10 = 0 from
+              by simp; omega]
+          simp [*]
+  · -- toInt?' leftPart = some (...)
+    simp only [leftPart, toInt?']
+    split <;> simp
+  · -- toNat?' rightPart = some rightNat
+    simp only [rightPart, rightNat]
+    split
+    · -- "000" ++ toString n, n < 10
+      exact zeroPad_toNat? "000" _ (by simp)
+    · split
+      · -- "00" ++ toString n, 10 ≤ n < 100
+        exact zeroPad_toNat? "00" _ (by simp)
+      · split
+        · -- "0" ++ toString n, 100 ≤ n < 1000
+          exact zeroPad_toNat? "0" _ (by simp)
+        · -- toString n, 1000 ≤ n < 10000
+          have hpad : ∀ c ∈ ("".toList), c = '0' := by simp
+          have hempty : "" ++ toString (d.natAbs % Nat.pow 10 4) =
+              toString (d.natAbs % Nat.pow 10 4) := String.empty_append
+          rw [← hempty]
+          exact zeroPad_toNat? "" (d.natAbs % Nat.pow 10 4) hpad
+  · -- (!leftPart.startsWith "-") = !(d < 0)
+    simp [leftPart]
+    by_cases hd : d < 0
+    · simp [hd]
+    · simp [hd]
+      intro h
+      have hmem : '-' ∈ Nat.toDigits 10 (d.natAbs / 10000) :=
+        List.IsPrefix.subset h (List.Mem.head _)
+      exact absurd (Nat.isDigit_of_mem_toDigits (by omega) (by omega) hmem) (by decide)
+
+/-- The string produced by `toString d` is well-formed for parsing. -/
+public theorem toString_isWfDecimal (d : Decimal) : IsWfDecimal (toString d) := by
+  obtain ⟨h_split, h_rlen, h_lint, h_rnat, _⟩ := toString_split d
+  refine isWfDecimal_iff.mpr ⟨_, _, h_split, ?_, ?_, ?_, ?_, ?_⟩
+  · -- leftPart ≠ "-"
+    intro h; by_cases hd : d < 0
+    · simp [hd] at h
+    · simp [hd] at h
+      have hdigits : ∀ c ∈ (d.natAbs / 10000).repr.toList, c.isDigit = true := by
+        intro c hc
+        have hc' : c ∈ Nat.toDigits 10 (d.natAbs / 10000) := by
+          rwa [Nat.repr_eq_ofList_toDigits, String.toList_ofList] at hc
+        exact Nat.isDigit_of_mem_toDigits (by omega) (by omega) hc'
+      rw [h] at hdigits; exact absurd (hdigits '-' (by simp)) (by decide)
+  · -- 0 < rightPart.length
+    rw [h_rlen]; omega
+  · -- rightPart.length ≤ DECIMAL_DIGITS
+    rw [h_rlen]; simp [DECIMAL_DIGITS]
+  · -- (toInt?' leftPart).isSome
+    rw [h_lint]; simp
+  · -- (toNat?' rightPart).isSome
+    rw [h_rnat]; simp
+
+/-- The canonical string representation of a decimal encodes the same integer value. -/
+public theorem computeValue_toString (d : Decimal) : computeValue (toString d) = some d.toInt := by
+  obtain ⟨h_split, h_rlen, h_lint, h_rnat, h_starts⟩ := toString_split d
+  rw [computeValue_eq_parser_value (toString_isWfDecimal d) h_split h_lint h_rnat]
+  simp only [h_rlen, h_starts, DECIMAL_DIGITS, Option.some.injEq]
+  simp only [show Nat.pow 10 4 = 10000 from rfl, show (4 : Nat) - 4 = 0 from rfl,
+    show Int.pow 10 4 = (10000 : Int) from rfl,
+    show Int.pow 10 0 = (1 : Int) from rfl, Int.mul_one]
+  simp (config := { decide := true }) only [Int64.natAbs]
+  by_cases hd : d < 0
+  · simp only [hd, ↓reduceIte, decide_true, Bool.not_true, Bool.false_eq_true]
+    have h3 :
+        -(↑(d.toInt.natAbs / 10000) : Int) * 10000 + -↑(d.toInt.natAbs % 10000) =
+          -↑d.toInt.natAbs := by
+      have := Nat.div_add_mod d.toInt.natAbs 10000
+      omega
+    rw [Int.sub_eq_add_neg, h3]
+    exact Eq.symm (Int.eq_neg_natAbs_of_nonpos (by
+      rw [Int64.lt_def_toInt] at hd
+      have : (0 : Int64).toInt = 0 := by rfl
+      omega))
+  ·
+    simp only [hd, ↓reduceIte, decide_false, Bool.not_false]
+    have hge : d.toInt ≥ 0 := by
+      simp only [Int64.lt_def_toInt] at hd
+      have : (0 : Int64).toInt = 0 := by rfl
+      omega
+    have h3 :
+        (↑(d.toInt.natAbs / 10000) : Int) * 10000 + ↑(d.toInt.natAbs % 10000) =
+          ↑d.toInt.natAbs := by
+      have := Nat.div_add_mod d.toInt.natAbs 10000
+      omega
+    rw [h3, Int.natAbs_of_nonneg hge]
+
+end Cedar.Thm.Decimal