I have a Lean-verified lemma formalizing a standard locality step in finite model theory / EF-game arguments: from a bounded-radius Duplicator winning condition (LocalDuplicatorWins), one can explicitly construct a finite partial isomorphism on the corresponding neighborhoods.
The result is:
- constructive (no choice or noncomputable axioms),
- radius-bounded,
- independent of global EF-game theorems,
- intended as reusable infrastructure rather than a standalone theory.
I would like guidance on:
(1) whether this fits CSLIB’s scope, and
(2) the appropriate namespace / level of generality before opening a PR.
Frozen reference artifact (self-contained Lean development):
https://github.com/inaciovasquez2020/cyclone-terminal-obstruction
I have a Lean-verified lemma formalizing a standard locality step in finite model theory / EF-game arguments: from a bounded-radius Duplicator winning condition (LocalDuplicatorWins), one can explicitly construct a finite partial isomorphism on the corresponding neighborhoods.
The result is:
I would like guidance on:
(1) whether this fits CSLIB’s scope, and
(2) the appropriate namespace / level of generality before opening a PR.
Frozen reference artifact (self-contained Lean development):
https://github.com/inaciovasquez2020/cyclone-terminal-obstruction