[0.5.0] Lemmas for universal equalities over list folds #117

Activity

1. afflom commented on Oct 15, 2026

   

   afflom

   on Oct 15, 2026 – with Claude

   MemberAuthor

   More actions

   Probe result, the first step of this item. Run with LexLean at 54f2ec4 (the commit UOR-Foundation/MNIST pins) and Lean 4.32.1; it is re-run on main when this item starts.

   Statement probed. A one-channel requantization step from MNIST, with literal constants:

   clampStep x = clamp(((x + 20) · 9365133 + 2³¹) quot 2³², 0, 255)

   and its monotonicity, ∀ x y : Int, x ≤ y → clampStep x ≤ clampStep y. That is the universal half of UOR-Foundation/MNIST#6's first fact; it is linear arithmetic with constant coefficients once the ifs are split.

   What is missing, in the order it was hit.

   1. Order propositions over Int. le is Nat-only in the 1.2 surface: LLT4001 phase link: order left operand has type Int, expected Nat. The probe fell back to Boolean order (lessThan y x = false → lessThan (clampStep y) (clampStep x) = false).
   2. The linear_arithmetic simp set. Its fixed script unfolds the named document definitions and LexLeanRuntime.subtract / LexLeanRuntime.multiply, but not:
      • LexLeanCollections.lessThan, so Boolean order never becomes an inequality omega reads;
      • LexLeanRuntime.negate;
      • LexLeanRuntime.quotient, whose zero-divisor case is itself an if.
   3. Case splits on if. The proof forms have no split of if c then a else b (no split, split_ifs or apply_ite), so a clamp is opaque to omega.

   Lean's verdict: omega could not prove the goal: No usable constraints found.

   What this item therefore needs, stated generally (C1): order propositions over Int and the fixed-width integers; the runtime's comparison, negation and quotient-by-a-nonzero-literal in the linear_arithmetic lowering; and a case split on if (a proof form, or the split inside that lowering). The fold lemmas in this issue's body come on top of these, for statements quantified over lists.

   ---

   Generated by Claude Code
2. afflom commented on Oct 16, 2026

   

   afflom

   on Oct 16, 2026 – with Claude

   MemberAuthor

   More actions

   Taking this item (agent session, branch claude/dazzling-cerf-cgz94p). I re-ran the probe on main at 32afe5da, Lean 4.32.1:

   • clampStep monotonicity, written as less_than y x = false → less_than (clampStep y) (clampStep x) = false with linear_arithmetic{definitions: [clampStep]}: omega finds no usable constraints. All three gaps from the earlier probe are still there.
   • A two-program fold equality, doubledTotal xs = total xs + total xs where total = list_fold (acc + v) 0 and doubledTotal = list_fold ((acc + v) + v) 0: omega sees two unrelated listFold atoms. The missing lemma is a normal form for additive folds: a fold whose step is acc + k x equals initial + Σ k over the list, and Σ is linear in k. Once the folds are rewritten into that form, the equality becomes linear over the atom Σ id xs. I checked this in raw Lean.

   Scope of the PR, one register row each (R3):

   1. Order over integers. Under language 1.2, <= and < take two operands of one integer type: Nat, Int, or one fixed-width type. They lower to Lean's order, which on fixed-width types is the order of mathematical values. Language 1.1 stays Nat-only and byte-identical.

   2. linear_arithmetic reads the runtime. The fixed script also rewrites the following through bridge lemmas: less_than on every integer key type (to decide (a < b)), negate, quotient and remainder (the zero-divisor case becomes an if; Int.tdiv/tmod by a literal become ediv/emod plus a sign case), and fixed-width order (to toNat/toInt). After the simplifier it splits every if/match left in the goal, then runs omega. A false obligation is still refused by Lean.

   3. Fold laws as LexLean source. A new runtime module, exported once from Lean in the manner of tests/runtime-library/MIGRATION.md, with every row's axioms pinned. It contains:

      • the additive-fold normal form for Nat and Int over list_fold, set_fold and map_fold (a map's fold is the fold of its entries);
      • linearity of Σ;
      • invariance of Σ under permutation, plus the forms LexLean programs actually produce: append, and the reverse built by a cons fold;
      • fusion of two folds into one fold over a pair.

      The normal-form lemmas join the linear_arithmetic script. Fusion and permutation are applied by a closed law{...} proof form whose registry gives each law's parameter types, so linking checks the application the way it checks apply.

   Acceptance runs over corpus-kind equalities: integer kernels (clamp/requantize monotonicity with quot), long folds (fold equalities over all lists, sets and maps), and permutation invariance. All of them are proved for all inputs, with decide used only on closed instances. Planted defects go in VERIFICATION.md: a law with a wrong statement, a bridge lemma dropped from the script, and a false order obligation.

   This moves the language-1.2 compiler-semantics ID once. I will merge main and regenerate whatever lands first. Files I will not touch: the Rust AST/RustSemantics (#91), the certificates (#89/#146), the core decoder (#90), the text laws (#30/#82), SHA-256 (#126).

   ---

   Generated by Claude Code
3. humuhumu33

   added this to the LexLean v0.5 milestone on Oct 16, 2026
4. afflom

   added 9 commits that reference this issue on Oct 16, 2026

   feat(#117): integer order, linear_arithmetic over the runtime, and th…

   ...

   656d0f7

   chore(#117): regenerate the fixture expectations for the new language…

   ...

   c9ce73f

   style(#117): canonical notation for the fold-laws sources, and the PF…

   ...

   4319d85

   chore(#117): regenerate the fold-laws goldens for its canonical sources

   ...

   4a06235

   chore(#117): regenerate the verification records of the finished exam…

   ...

   258b878

   fix(#117): restore examples/uor-atlas, recorded as deleted while a lo…

   ...

   01f4194

   chore(#117): regenerate the verification records of the remaining lan…

   ...

   16bef9d

   fix(#117): reserve the names the extended script writes, and the case…

   ...

   b4a34c4

   docs(#117): record the planted defects of the fold laws, and format t…

   ...

   fc4533e
5. afflom

   closed this as completedin #158on Oct 16, 2026
6. afflom

   added 3 commits that reference this issue on Oct 16, 2026

   Merge pull request #158 from UOR-Foundation/claude/dazzling-cerf-cgz94p

   ...

   378628e

   fix(#117): the runtime gates know LexLeanLaws, and their namespace li…

   ...

   89b7bcf

   v0.4 train: byte literals (#68), widening (#151), dyadic floats (#150)…

   ...

   193cd21