3 ms·
You only read the 37 lines in SSOT.lean and stopped. It's the entry point that defines DOF=1 so other files can import it. The actual proofs are in Foundations.
by trissim 9mo ago
You only read the 37 lines in SSOT.lean and stopped. It's the entry point that defines DOF=1 so other files can import it. The actual proofs are in Foundations.lean (364 lines - timing trichotomy, causality), Requirements.lean (derives the two necessary language features), Completeness.lean (mechanism exhaustiveness), Derivation.lean (the uniqueness proof that achieves_ssot m = true iff m = source_hooks), Coherence.lean, CaseStudies.lean, LangPython.lean, LangRust.lean etc.
~2k lines total across the lean files. Zero sorry. Run grep -r "sorry" paper2_ssot/proofs/ if you don't believe me.
"Unfolding the definitions they say x=1 => x=1" applies to three sanity lemmas in the scaffolding file. It's like reading __init__.py and concluding the package is empty.
- BalinKing 9mo agoSee my other comment—LangRust.lean is the same way. EDIT: Just skimmed Completeness.lean, and it looks similar—at a glance, even the 3+-line proofs are very short and look a lot like boilerplate.
- trissim 9mo agoInteresting that you're using em dashes in your comments. Those require Alt+0151 or copy-paste. Glass houses.
- dwb 9mo agoAnd Option-Shift-Hyphen in macOS, which is easy if you know it. And a press and hold on a hyphen on iOS, which is discoverable, even.
- BalinKing 9mo agoYeah, I'm on macOS (although even back on Windows, I used to use the Character Map all the time).
- trissim 9mo agoFair, the em dash comment was a cheap shot. Withdrawn. The substantive point stands: you've now "skimmed" multiple files, called them all "boilerplate," and haven't engaged with the actual proof structure. The rebuttals section addresses "The Proofs Are Trivial" directly (Concern 9). At some point "I skimmed it and it looks trivial" stops being a critique and starts being "I didn't read it."