# Typed normalization assurance adapter Initial decision: **Prototype an evidence-platform module**. First dossier, 9 October 2026 Australia/Brisbane. Demand and profitability remain unvalidated. ## Research finding Family 245 claims that system-wide weak beta normalization implies system-wide strong beta normalization for an arbitrary pure type system. It permits arbitrary sorts and nonfunctional axiom/product relations, open valid contexts and reduction inside annotations. Its selected formal scope matches this beta-only statement; no independent proof check was run here. ## Problem and buyer A team designing a dependent typed language, total DSL or proof checker may need to justify that reduction terminates under every strategy. Proving that every legal expression has a terminating route can be a different obligation from proving termination of every possible route. Teams also need to avoid carrying a termination claim across added rewrite rules, eta conversion or changed annotations. ## What the finding could enable A language assurance adapter can record the exact pure type specification, a separately established global weak-normalization proof and a mapping of the implemented syntax and reduction relation. The claimed theorem then supplies a route to strong beta normalization under those premises. This could introduce reusable normalization evidence for eligible language designs and a CI report when a language change invalidates the mapping. It does not establish weak normalization for the team or automatically handle a language extension. ## Technical and commercial limits The premise concerns every legal expression in every valid context. Finding a normal form for one term, a finite test suite or the evaluator's successful runs does not discharge it. Full annotation reduction is part of the model. The theorem makes no beta-eta assertion and does not cover arbitrary user rewrite rules, recursion, effects, external functions or the implemented evaluator without a separate correspondence proof. Termination supplies no practical bound on reduction length, memory or latency. Eligible designs may already have a conventional strong-normalization proof, eliminating the proposed saving. ## Minimal architecture Specification manifest with sorts, axioms and product rules -> syntax/reduction correspondence evidence -> global weak-normalization proof reference -> pinned theorem and checker trust record -> per-version documentary audit -> language-change impact report. A proof backend and performance benchmark are separate integrations. The current prototype only lints declared metadata; it grants neither a proof certificate nor approval of evidence contents. ## Existing alternatives and differentiation Dedukti already provides type checking for the lambda-Pi calculus modulo rewriting. Its manual separates type preservation from requirements for combined confluence and termination, and describes external confluence checking. The separate SizeChangeTool checks termination for higher-order rewriting with dependent types. These are existing workflows, not implementations of the source implication for arbitrary language extensions. Any adapter should export evidence to existing tools and test whether the pure-beta restriction actually saves work. [Dedukti manual](https://github.com/Deducteam/Dedukti), [SizeChangeTool](https://github.com/Deducteam/SizeChangeTool). ## Monetization hypothesis Hypothesis: an AUD 6,000–12,000 scoped language-assurance assessment, with recurring fees only for a team that repeatedly changes a qualifying specification. At an assumed AUD 8,000 fee and 30 expert hours at AUD 180/hour, direct labor is AUD 5,400 and the remainder is AUD 2,600 before maintenance, sales and overhead. Forty-five hours would already exceed that fee. This is a module of the evidence platform described in dossiers 001–003 and 020; do not count it as an independent subscription business with duplicated customers. ## Validation experiment Choose one small pure type specification with an independently established global weak-normalization proof. Compare the existing strong-normalization argument with the proposed implication and record the proof effort saved. Change the reduction to include eta or a user rule and require the adapter to refuse the source-derived claim until a separate bridge is supplied. Benchmark actual reduction cost independently. The manifest tests already detect the single-term, eta, additional-rule and runtime-bound mistakes; they do not prove normalization. ## Conditions to reject or defer Reject if eligible teams are too rare, all useful designs already have equivalent proofs, the correspondence proof costs more than the saved work, or existing evidence exports cover the need. Defer implementation certification until a trusted formal backend checks the exact implementation mapping and premises. No universal program-termination service is justified. ## Next concrete action Specify one eligible reference language and inventory its existing normalization proof before implementing a checker adapter. Use the `245-pts-beta-normalization` documentary contract in [audit_claim_contract.py](../../tools/audit_claim_contract.py) to capture the evidence gaps. ## Pinned research sources - [Main manuscript](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/preprints/Weak-and-strong-normalization-in-pure-type-systems-September-25-2026/paper.pdf), introduction, specification and main theorem read. - [Selected formal scope](https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/docs/245.md), read and compared; independently checking Lean remains pending.