Show HN: Lean4 proof that SSOT requires definition-time hooks and introspection (zenodo.org)

I do not understand what this could mean.

There are clear formalizations of concepts like Consistency in distributed systems, and there are algorithms that correctly achieve Consensus.

What does it mean to formalize the "Single Source of Truth" principle, which is a guiding principle and not a predictive law?

Sorry for the caution but this is becoming very common. Lots of red flags for AI-Slop: Zenodo, single author work, lots of jargon, author has not had prior work in the field.

The file SSOT.lean is completely trivial, I think: Unfolding the definitions in the theorems, they say nothing but "x=1 => x=1", "x=1 => x≤1", and "x≠1 => x=0 ∨ x>1" (where x is a natural number). Basically, there's no actual proof here, at least not in that file....

This is indeed the danger of letting LLMs manage a "proof" end-to-end—they can just pick the wrong definitions and theorems to prove, and even though the proofs they then give will be formally sound, they won't prove anything useful.

Any example(s) of language that includes all the necessary features?

All the heavy lifting is done by the comments. For example: theorem dof_gt_one_inconsistent (dof : Nat) (h : dof > 1) dof ≠ 1 (in Basic.lean) is the well-known fact that any number > 1 is unequal to 1.

But the comment states: DOF > 1 implies potential inconsistency. Inconsistency of what? Lean doesn't know, or care....

Addressed the criticisms raised here.

The main gap was real: language capability claims (Python can achieve SSOT, Rust cannot) were derived from string matching, not from formalized semantics. Fixed.

Proof chain now:

python_can_achieve_ssot uses python_has_hooks (a Prop, not a Bool) uses init_subclass_in_class_definition derived from execute_class_statement (modeled Python class definition semantics)

To attack this, you must either show Python code where init_subclass does not run at class definition time (empirically false), or find a bug in Lean.

For Rust, rust_lacks_introspection is now a 40 line proof by contradiction, not rfl. It assumes a hypothetical introspection function exists, uses erasure_destroys_source to show user-written and macro-expanded code produce identical RuntimeItems, then derives that any query would need to return two different sources for the same item. Contradiction.

On the "SSOT.lean is trivial" point: that file is scaffolding (38 lines). The substantive proofs are in Inconsistency.lean (225 lines, formalizes inconsistency as a Prop, proves dof_gt_one_implies_inconsistency_possible with constructive witness) and Coherence.lean (264 lines, proves determinate_truth_forces_ssot).

On "proofs are just rfl": many foundational proofs are definitional by design. When you model correctly, theorems become structural. But the new rust_lacks_introspection shows non-trivial reasoning exists where needed.

Updated stats: 9351 lines, 26 files, 541 theorems, zero sorry. lake build passes.

Remaining attack surfaces are model fidelity (show me Python code that contradicts the model) and interpretation gap (philosophy, not math). Both are inherent to any formal verification of real systems.

Common rebuttals already addressed in the paper:

"OpenAPI/Swagger achieves SSOT without hooks": Yes, because the spec file IS the single source and generated code is derived. That instantiates DOF=1, it does not contradict it. External tooling can always enforce consistency by being the source. Our claim is about what the language itself can enforce.

"Model doesn't mirror rustc internals verbatim": We model observable behavior, not compiler implementation. The claim is: at runtime, you cannot distinguish hand-written code from macro-generated code. Challenge: produce Rust code that recovers macro provenance at runtime without external metadata files.

"You just need discipline": Discipline is the human oracle. The theorem says: with DOF > 1, consistency requires an external oracle (human memory, documentation, review process). That is not a counterargument, it is the theorem restated.

"Real codebases don't need formal DOF guarantees": Whether you need it is engineering judgment. We prove what is logically required IF you want guaranteed consistency. Same interpretation gap exists for CAP theorem, Rice's theorem, Halting problem. Philosophy, not math.

Full rebuttals section in the paper addresses these and more.