feat(proofs): program equalities over all inputs: integer order, linear_arithmetic over the runtime, fold laws, and the law form (PF-20..PF-23, #117)

CHANGELOG.md

@@ -15,6 +15,27 @@ versions, and the entries below say what each tag does and does not claim.
 
 ## Unreleased
 
+- Program equalities over all inputs (#117, SPEC.md §17.12, `PF-20`..`PF-23`,
+  no new diagnostic code). Language 1.2 orders `Int` and every fixed-width
+  integer type with `<=` and `<`, by mathematical value; language 1.1 keeps
+  `Nat` only. `linear_arithmetic` now reads the runtime: `less_than`,
+  `equal`, `negate`, `quotient`, `remainder` (truncating division by a
+  literal included), and fixed-width order and equality become linear
+  arithmetic, every `if` and `match` left in the goal is split, and `omega`
+  decides each case. The fold laws are LexLean source, the native runtime
+  module `LexLeanRuntime.Laws` (`tests/runtime-library/LAWS.md`). It holds
+  the normal form of additive list, set, and map folds as sums, their
+  linearity, and their invariance under permutation, append, and reverse,
+  which `linear_arithmetic` rewrites with, plus fusion, the fold of a pair,
+  and the fold of an append. The closed `law` proof form applies one of
+  these registered laws (`language/runtime-1.2/laws.toml`) with linking
+  checks. `examples/fold-laws` verifies integer kernels and fold equalities
+  for all inputs, with `decide` only on closed instances. The
+  language-1.2 compiler-semantics ID changes (`semantic_ir` 11,
+  `lean_backend` 18, `proof_lowering` 3), and every language-1.2 lock,
+  golden, fixture expectation, calculus package, production export, and
+  verified record is regenerated. The register holds 391 IDs.
+
 - The runtime gates read what they claimed to (#154, follow-up to #144; no new
   diagnostic code, no new ID). `RT-04` finds a Lean runtime text in any string
   literal of the compiler's source outside unit-test items, in production code

CONFORMANCE.md

@@ -392,6 +392,10 @@ the error registry does not sanction (R5, `ERRORS.md`).
 | `PF-17` | `build` | native_decide is never accepted or generated. |
 | `PF-18` | `build` | Lean proof failures remap to the smallest originating LexLean proof or statement span. |
 | `PF-19` | `build` | The language-1.2 linear_arithmetic proof form names only the prior document definitions it unfolds, lowers to one fixed omega script, proves true linear obligations, and is refused by Lean on a false one. |
+| `PF-20` | `build` | Under language 1.2 the order propositions <= and < take two operands of one integer type, Nat, Int, or one fixed-width type, and lower to Lean's order on that type; language 1.1 keeps them over Nat only. |
+| `PF-21` | `build` | The language-1.2 linear_arithmetic proof form reads the runtime: it rewrites less_than, equal, negate, quotient, remainder, and fixed-width order and equality into linear arithmetic over mathematical values, splits every if and match left in the goal, proves integer kernels for all inputs, and is refused by Lean on a false one. |
+| `PF-22` | `build` | The runtime module LexLeanRuntime.Laws states the fold laws as LexLean source with every row's axioms pinned, and linear_arithmetic rewrites additive list, set, and map folds into sums that are linear and invariant under append and reverse, so fold equalities verify for all inputs with decide only on closed instances. |
+| `PF-23` | `build` | The language-1.2 law proof form applies one registered fold law (fusion, the fold of a pair, or the fold of an append) to checked type arguments, arguments, and prior theorems discharging its premises, and is refused in linking for an unregistered law, a wrong argument count or type, or a missing premise, and by Lean for a statement the law does not prove. |
 
 ## reasoning
 

README.md

@@ -126,6 +126,7 @@ Every directory under [examples/](examples/) is discovered by the example gate (
 | [production-coverage](examples/production-coverage/) | Language-1.2 semantic preservation coverage (SPEC.md §17.17): 33 production roots across four modules that together exercise every runtime row of the production registry (§17.13) — fixed-width arithmetic at every width, text, bytes, and decimal parsing and formatting, records, options, generic and nested inductive types, higher-order functions with captures, structural, mutual, and well-founded recursion, and every collection template and key order; verification extracts every root and checks its certificate A. |
 | [models](examples/models/) | Language-1.2 models (SPEC.md §17.12) across nine modules: a stateful deterministic session with an invariant, a rule policy, a statistical triage and an integer feed-forward digit recognizer whose weights are content-addressed artifacts embedded with kernel-checked decodings, stateful ledgers in every contract shape whose evidence leaves runtime checks open, every composite form over stateless and stateful stages (stateful sequences with proved and checked junctions, stateful fan-out, product, and branch, and stages checked after they run), every claim kind discharged by statement-exact theorems and restated against the fixed model semantics, every runtime refusal decided by the kernel, and production roots that apply models through their required runtime checks, extracted through Lean. |
 | [reasoning](examples/reasoning/) | Language-1.2 reasoning machines (SPEC.md §17.12) across five modules: a clinical forward expert system whose eight guarded rules derive a multi-step triage with its invariant and termination proved, a generic terminating countdown, a deduplicating breadth-first jug planner, a depth-first search and a generate-and-verify reasoner over a model's proposals, an answer proved correct under the logic's invariant with its check erased, forged traces and inapplicable steps refused at run time, the six-counter ledger of each run and every generated theorem kernel-checked, and production roots extracted through Lean and transcribed to calculus programs the compiler project checks against the reasoners themselves. |
+| [fold-laws](examples/fold-laws/) | Language-1.2 program equalities over all inputs (SPEC.md §17.12, *Fold laws*) across three modules: a clamped requantization step monotone and bounded for every `Int`, truncating division by positive and negative literals, order and equality over `UInt8` and `Int8`, additive folds over lists, sets, and maps equal as sums (doubling, counting, weighting, append in either order, reverse, debits against credits, a map's keys and values), a single-pass statistics fold and a fused parity fold proved by the `law` form, and `decide` only on closed instances. |
 | [uor-atlas](examples/uor-atlas/) | The complete native Atlas declaration and proof graph, including the census/group chain, `S37`, `S38`, and the authoritative integer-uniqueness statement `S43`; no handwritten Atlas module is a generated dependency. |
 
 ## Building and running the gate
@@ -137,7 +138,7 @@ just vv        # the complete normative acceptance gate (SPEC.md §9.2)
 just release   # vv, then the §30 release criterion; refused until 1.0.0
 ```
 
-All 387 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
+All 391 registered conformance IDs are implemented and pass; `just vv` runs clean from a checkout with the pinned toolchain installed.
 
 The differential against the independent generator `lean4-prod` (SPEC.md §17.19, `OR-01`..`OR-08`) acquires it at its pinned commit: from the checkout `LEXLEAN_ORACLE_DIR` names, or by fetching the commit with `git` into the Cargo target directory (`LEXLEAN_ORACLE_CACHE` overrides), and builds it with the pinned Lean and Rust toolchains. It is validation evidence only and no input to any identity. An oracle that cannot be acquired, is not the pinned files, or fails is unavailable: that fails the gate on Linux x86-64 and is printed as `NOT VALIDATED` elsewhere, and is never reported as agreement.
 
@@ -156,7 +157,7 @@ Every row is validated by `just vv`; the IDs link the claim to its register row,
 | Fixed structural, mathematical, and proposition grammar with closed ambiguity handling | `GR-01`..`GR-16` | `build` |
 | Typed closed IR with canonical serialization, native core modules (and the second schema of them that lossless migration of the proof library needs), portable language-1.1 application data and operations, versioned language-1.2 semantic modules, products, and first-class functions, ordered collections and graphs, semantic snapshots, alpha identities, recursion evidence, and content identities | `SM-01`..`SM-31` | `build` |
 | Document and generic semantic declarations with exact self-application, type checking, structural recursion, recursive and mutual language-1.2 data, generic and executable higher-order definitions, mutual and well-founded recursion with semantic evidence, explicit state threading, and acyclicity rules | `DF-01`..`DF-18` | `build` |
-| The structured proof language with pinned Lean lowerings, including closed linear arithmetic | `PF-01`..`PF-19` | `build` |
+| The structured proof language with pinned Lean lowerings, including closed linear arithmetic, integer order, and the fold laws | `PF-01`..`PF-23` | `build` |
 | Prose-free deterministic generated Lean with complete token traceability | `LN-01`..`LN-12` | `build` |
 | Canonical LaTeX regeneration and the optional hash-checked PDF provider | `TX-01`..`TX-12` | `build` |
 | Canonical diagnostics, source maps, coverage, manifests, and reproducible builds | `AR-01`..`AR-14` | `build` |