Pure-beta normalization assurance has a global premise

Family 245; scoped reading addendum, 9 October 2026 Australia/Brisbane. Source revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb.

Source finding

The full introduction, syntax/typing definitions and main theorem were read, together with the selected formal scope. The claim applies to arbitrary pure type specifications, including nonfunctional relations, and to all legal expressions in all valid contexts under beta reduction inside annotations.

Applicability boundary

One normalizing term or a successful finite evaluator test is insufficient. The theorem supplies no eta or added-rewrite-rule guarantee and no practical reduction-length bound. The proof and implementation correspondence have not been independently checked.

Business decision

Added dossier 038 and a documentary contract; global weak normalization and implementation mapping remain separate proof obligations.

Exact sections read

• preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/build/sections/introduction.tex.
• lean/docs/245.md.

These readings establish recorded source scope, not proof correctness. No independent Lean verification was run. Companion manuscripts and construction effectiveness remain separately tracked. See source metadata.