Manuscript Oai227-A@1 · Oai227-A.tex · section · 7f45f607
Source and formalization status
Scope and the necessary debugging › Source and formalization status · lines 185–205
The inspected external quench manuscript is attributed to OpenAI and dated 5 October 2026. Its stationary companion has the same date OAI227Quench,OAI227Stationary.
The scope note lean/docs/227.md describes selected
high-temperature, critical-mixing, and barrier statements;
it does not describe a formalization of the functional
autocorrelation limit Lean227.
Moreover, the inspected Comparator targets
SKRatio.lean and CriticalSKMixing.lean
contain theorem bodies ending in sorry
LeanSKRatio,LeanCriticalMixing.
They are not presented here as completed executed proofs.
No conclusion is drawn about uninspected artifacts.
The supplied Cheung passages are documentary comparisons. Their model-specific theorems are not assumptions of the finite SK calculation.