Provedaitherhot-reloadidentityb846d70

Aither: foreign-type insertion preserves ordinals; same-type insertion changes them

For all $\htmlData{mx=1}{t, u \in \htmlData{mx=0}{\operatorname{String}}}$ and $\htmlData{mx=3}{\mathit{before}, \mathit{suffix} \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{List}}\,\htmlData{mx=1}{\operatorname{String}}}}$ :

\begin{aligned} & \left(\right. \htmlData{mx=2}{u} \mathrel{\htmlData{mx=4}{\neq}} \htmlData{mx=3}{t} \\ & \htmlData{mx=1}{\implies} \htmlData{mx=13}{\htmlData{mx=6}{\operatorname{typeCount}}(\htmlData{mx=7}{t}, \htmlData{mx=12}{\htmlData{mx=11}{\htmlData{mx=8}{\mathit{before}} + \htmlData{mx=10}{\mathtt{+}(\htmlData{mx=9}{u})}}})} \\ & \quad \htmlData{mx=5}{=} \htmlData{mx=20}{\htmlData{mx=14}{\operatorname{typeCount}}(\htmlData{mx=15}{t}, \htmlData{mx=19}{\htmlData{mx=16}{\mathit{before}} + \htmlData{mx=18}{\mathtt{+}(\htmlData{mx=17}{\mathit{suffix}})}})} \left.\right) \\ & \htmlData{mx=0}{\land} \htmlData{mx=29}{\htmlData{mx=22}{\operatorname{typeCount}}(\htmlData{mx=23}{t}, \htmlData{mx=28}{\htmlData{mx=27}{\htmlData{mx=24}{\mathit{before}} + \htmlData{mx=26}{\mathtt{+}(\htmlData{mx=25}{t})}}})} \\ & \quad \htmlData{mx=21}{=} \htmlData{mx=37}{\htmlData{mx=36}{\htmlData{mx=30}{\operatorname{typeCount}}(\htmlData{mx=31}{t}, \htmlData{mx=35}{\htmlData{mx=32}{\mathit{before}} + \htmlData{mx=34}{\mathtt{+}(\htmlData{mx=33}{\mathit{suffix}})}})} + 1} \\ & \htmlData{mx=0}{\land} \htmlData{mx=45}{\htmlData{mx=38}{\operatorname{typeCount}}(\htmlData{mx=39}{t}, \htmlData{mx=44}{\htmlData{mx=43}{\htmlData{mx=40}{\mathit{before}} + \htmlData{mx=42}{\mathtt{+}(\htmlData{mx=41}{t})}}})} \mathrel{\htmlData{mx=53}{\neq}} \htmlData{mx=52}{\htmlData{mx=46}{\operatorname{typeCount}}(\htmlData{mx=47}{t}, \htmlData{mx=51}{\htmlData{mx=48}{\mathit{before}} + \htmlData{mx=50}{\mathtt{+}(\htmlData{mx=49}{\mathit{suffix}})}})} \end{aligned}

What the notation means · or point at any symbol

String: String: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (String)
x ∈ TVariables: t, u range over String: the statement must hold for every choice. ((t u : String))
List: List: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (List)
f(x)Function application: List applied to String. Lean writes f x; papers write f(x). (List String)
≠Not equal: u and t are different. (u ≠ t)
⟹Implies: If u ≠ t, then typeCount(t, before + +(u)) = typeCount(t, before + +(suff…. (Between types, A → B is the type of functions from A to B.) (u ≠ t → typeCount t (before ++ u :: suf…)
typeCount: typeCount: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (typeCount)
=Equality: typeCount(t, before + +(u)) and typeCount(t, before + +(suffix)) are the same. (typeCount t (before ++ u :: suffix) = t…)
(x : T)Type ascription: before + +(u) read as a :(suffix). Mathematicians leave this implicit; Lean needs it to know which kind of number is meant. ((before ++ u :: suffix))
+Addition: before plus +(u). (before ++ u)
∧And: Both hold: typeCount(t, before + +(t)) = typeCount(t, before + +(suff…, and typeCount(t, before + +(t)) ≠ typeCount(t, before + +(suff…. (typeCount t (before ++ t :: suffix) = t…)

theorem aither-b846-typed-ordinal-insertion (t u : String) (before suffix : List String) :
    (u ≠ t → typeCount t (before ++ u :: suffix) = typeCount t (before ++ suffix)) ∧ typeCount t (before ++ t :: suffix) = typeCount t (before ++ suffix) + 1 ∧ typeCount t (before ++ t :: suffix) ≠ typeCount t (before ++ suffix)

Natural-number abstraction of codegen.nim registerRegionInit typeCounter. Insertion of a different helper type preserves this type's ordinal; inserting an earlier helper of the same type increments it. Does not promise persistent semantic identity across arbitrary structural edits.

How it was proved

Proved: 1 October 2026
By: Ajax
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Quot.sound, propext
Proof: 24 lines of Lean

Aither: foreign-type insertion preserves ordinals; same-type insertion changes them

How it was proved

More proved statements