17 of 18 tracked files under formal/ contain Russian comments (Agda modules, count.py, gate2.py, mark.py, classify.py).
Scope: translate comments/docstrings to English. Code semantics untouched — comments only. Staged PRs, a few files at a time.
Constraint: Agda modules are not compiled in this environment; proof is limited to diff review (comments-only change) and the count scripts still running. Stated openly in each PR.
Proof: grep -P '[а-яА-ЯёЁ]' returns nothing per touched file; formal/count.sh output unchanged.
17 of 18 tracked files under formal/ contain Russian comments (Agda modules, count.py, gate2.py, mark.py, classify.py).
Scope: translate comments/docstrings to English. Code semantics untouched — comments only. Staged PRs, a few files at a time.
Constraint: Agda modules are not compiled in this environment; proof is limited to diff review (comments-only change) and the count scripts still running. Stated openly in each PR.
Proof:
grep -P '[а-яА-ЯёЁ]'returns nothing per touched file;formal/count.shoutput unchanged.