Merge origin/main into z-tech/kilian

Resolve 17 add/add conflicts by taking HEAD's version — the branch is
strictly forward of main on every conflicted file. Specifically, HEAD
already contains:

  * VC noncomputable nuke (Classical.ofNonempty → default, Nonempty → Inhabited)
  * Hasher/ root-level lib (Compress/HashValue/VarArityHash/DomainEncoded)
  * HasPositionBinding.bindingError_lifts field with full docstring
  * PCP relation field + Soundness.lean + Probability.lean
  * Kilian Theorem 5.1 full proof scaffolding (Adversary/Reductor/Lemma53/Theorem51)
  * Deleted vacuous-True placeholders (mt_equivocation, mt_multi_configuration_multi_extractability)
  * Trait-dispatch round-trip tests (TraitTests.lean)
  * lakefile lean_lib «Hasher» entry

Build: lake build clean, 2475 jobs.

Author: z-tech