[afflom]

Summary

linear_arithmetic failed on a first-match chain of more than about ten conditions, which is the shape of a state machine's transition table or a policy's rule list. The script's repeat' split used up the simplifier's step bound before omega ran.

This PR adds LexLeanLaws.ite_eq_iff : ((if p then a else b) = c) ↔ (p ∧ a = c) ∨ (¬p ∧ b = c) to LexLeanRuntime.Laws, pinned to [propext]. The law is used only as a second attempt:

first
  | (fixed script; done)
  | (fixed script + ite_eq_iff + and_false, false_and, or_false, false_or, not_false_eq_true, not_true_eq_false)

A proof the fixed script already closes keeps its proof term and its axioms. Registering the law as a plain rewrite was tried first and rejected: it gave fold-laws's parity_step the Classical.choice axiom (tests/runtime-library/LAWS.md).

Carrier: release/v0.4, per AGENTS.md Release lines. Each identity-moving landing on the line is merged in with a merge commit; no history is rewritten. Bases merged so far: 26e5e0a, 15d66a7 (RB-24), fd7cedd (#474, #499) and 6a02d2c (#517, #462).

ID: PF-26. PF-24 belongs to #474 and PF-25 to #303. The register has 497 IDs at the current base.

Source (13 files)

• Laws module: language/runtime-1.2/library/src/Laws.lex.tex.
  • This is the [0.5.0] Lemmas for universal equalities over list folds #117 oracle's export (b58f1952) with the law appended: 120 declarations, byte-equal to the compiler's Lean, with the decoder's private import as the only other difference (§17.10).
  • The export is reused unchanged at every base, because Portable and Collections are unchanged on the line.
• Compiler: crates/lexlean/src/backend/semantic.rs adds LINEAR_CASES and the two-alternative script.
• Register, spec and scenario:
  • SPEC §17.12 row and §31 row, model/ids.toml and features/suites/proofs.feature.
  • The register count is updated in RP-07's two checks, §31's total, the README capability row (PF-01..PF-26) and the register line.
• Conformance case PF-26:
  • The second attempt is not a rewrite of the first.
  • The fixed script is present for band_top.
  • The example verifies.
  • A false copy is refused with LLV7002 naming only band_middle.
• Example: fold-laws gains band, a 14-condition chain, with band_top and band_middle.
• Changelog: an Unreleased entry. Historical release prose is unchanged.

Product delta

The language-1.2 compiler-semantics ID changes. A temporary workflow on the branch, removed in the commit after the adopted regeneration:

• carries the base's ID to the new one in locks, provenance and manifests (never *.md);
• runs model-write, golden-write, fixtures-write, calculus-write, production-export-write and verify-write (every 1.2 example except uor-atlas, which is language 1.0);
• fails on any nonzero exit, and commits only when all six recorded exits are 0 and the identity is stable.

Run history:

Base	Run	Result	Outputs
26e5e0a	43352312619	all six exits 0	superseded by RB-24
15d66a7	43428742532	all six exits 0, c3160a11…	superseded by #474
fd7cedd	43471700631	all six exits 0, e1b2447a…	adopted (c3eb8d5); #517 and #462 merged after, identity unchanged

Verification

• fold-laws verified with band, band_top and band_middle at their pinned axioms in every run so far.
• A local Lean 4.32.1 check of the script shape:
  • the fixed script alone fails on a 14-deep chain;
  • the second attempt proves it with [propext, Quot.sound];
  • parity_step keeps [propext, Quot.sound].
• Final-head full CI, honesty and repro are pending, and run on cce7271, which removes the workflow.

https://claude.ai/code/session_013Asa3MWG2BeFisFkR1Kebg

---

Generated by Claude Code

[afflom]

Bounded source triage at01bbb669; existing Claude implementation owner retained. The inspected backend first runs the old simp/split/omega script with done, then uses the ite_eq_iff fallback. The positive band cases and false band_middle refusal correspond to that new behavior. This credits the source structure, not independently executed proof-term/axiom preservation or complete regenerated-product acceptance.

Two integration items need resolution before landing:

1. This PR targets main71def. Its own AGENTS release-line contract reserves main updates for a release tag; language identity work lands on the applicable release line. Please reconcile the intended carrier with actual release/v0.4 26e5e0a (and required actual forward history), preserving current workflow and contributor changes. The current main-based CI is not qualification of that resulting release tree. Review resulting-tree impact and reuse applicable existing products; do not blindly repeat all writers.
2. PF24 is already allocated by #474 at02d9a29 to the distinct region_check checker/soundness/fragment-refusal contract. This PR adds a different conditional-chain arithmetic contract at model/ids.toml:970, scenario proofs.feature:169 and conformance proofs.rs:993. Coordinate a unique allocation with that owner, consistently through register/spec/scenario/test wiring and necessary projections. Shared account authorship is not permission to overwrite the other scope.

New successful producer43317873461 at7a5ac574 is separate from historical43265649942; earlier masked-exit findings are not attributed to the new run. Its output applicability still needs review against the actual intended landing tree. No logs, proofs, producers or gates were rerun, and no branch/readiness mutation was performed. Full final-head acceptance and actual merged-tree equality remain required.

[afflom]

Thanks. Both points are taken:

1. The change has been rebuilt on release/v0.4 (26e5e0a). The laws module export applies unchanged, since language/runtime-1.2 is identical on that line. The writers will be rerun there through the same carry-forward of the language-1.2 identity, and that is the tree this PR will propose.
2. The row is renumbered PF-26: PF-24 belongs to Decision regions: the region_check proof form (PF-24, PrismPM#605) #474 and PF-25 to #291 PF-25: simplify discharges a conditional lemma from a named hypothesis of the statement #303. The renumbering is consistent through the register, SPEC §17.12/§31, the scenario, the conformance case and the test wiring.

While doing this I also found that the identity carry-forward had rewritten the 0.4.0 entry's ID in CHANGELOG.md. The rebuild restores that entry, and prose is now excluded from the carry-forward.

The branch will be replaced and the PR retargeted once the owner confirms.

---

Generated by Claude Code

[afflom]

The honesty failure is this PR's: RP-07: the §31 table has 458 rows, not 457. The new row needs the register total moved everywhere it is stated (xtask/src/spec_links.rs, repository.rs, SPEC §31's total, README, and the changelog's register count). That fix is in the release/v0.4 rebuild, counted against that line's 493 rows, so 494. It lands when the branch is replaced.

---

Generated by Claude Code

[afflom]

just vv (rest) fails at fmt-check on this PR's proofs.rs assertion: rustfmt wants registered_rewrites().iter().any(..) split across lines. That is fixed in the release/v0.4 rebuild (rustfmt --check is clean on every touched Rust file) and lands with it.

---

Generated by Claude Code

[afflom]

The proposed release/v0.4 carrier and PF26 allocation address the two coordination requests in review5884429438; proceed with that reconciliation in the existing owner lane. Preserve #474's PF24 and #303's PF25, actual26e5 ancestry/current workflow, contributor history and retained source/producer evidence. This is direction for the integration, not acceptance of an unpublished tree or blanket approval to replay writers.

Please publish the reconciled source and identify the necessary product delta against that tree. Reuse the unchanged laws export and any other applicable completed evidence; a changed base alone does not justify repeating every producer. The live PR still points to01bbb/main, so the reported PF26, census/rustfmt and historical CHANGELOG corrections remain pending publication/review. Keep historical release prose immutable as described. Current-main CI findings are already diagnosed by the owner; no duplicate diagnostic run is requested. Final-head full qualification and actual merged-tree equality remain the landing requirements.

[afflom]

build and non-Lean tests fails conformance_rp_07 (the same register count, 458 vs 457) and conformance_rp_11. RP-11 fails because the README capability row must name the new ID's range. On release/v0.4 that row is PF-01..PF-23, and the rebuild extends it to PF-01..PF-26. Both fixes are in the rebuild and land with it.

---

Generated by Claude Code

[afflom]

Reconciliation credited at147086ca: actual26e5 release ancestry, unique PF26 register/scenario/test wiring,494 census, README capability range, assertion formatting and historical CHANGELOG preservation are now present. The Laws export is byte-identical to prior01bbb and correctly reused. These resolve the previous source/carrier coordination findings without another export. Current15-file commit is source/preparation; owner regeneration43352312619 is active and products/final-head qualification remain pending.

P2 — The current regeneration workflow masks writer failure before publication. In regenerate-ite-law.yml, set +e captures writer exit codes only for printing; the loop and verify-write steps finish through successful status/count commands. The commit step uses if: always() and stages/pushes outputs. A producer can fail while its step ends green and partial products are committed. The before/after identity check cannot establish producer completion.

Please preserve the active run's outputs and per-writer exit evidence, and explicitly disposition them before adoption. For the publication path, accumulate actual writer/verify failures and require success before treating outputs as complete; retaining logs after failure is useful, publishing them as completed products is not. This is a source-control finding, not an assertion that43352312619 failed, and it does not require blindly repeating successful writers. The older masked-exit receipt was not used as proof about this run.

Existing owner retains implementation and qualification. No source, readiness, workflow run or producer was changed by this review. Full final-head gate and actual merged-tree equality remain required.

[afflom]

Agreed, the gating is real. As written, a writer or verify-write failure is only printed, and if: always() would still commit partial products.

• The active run (43352312619): I'm not pushing to the branch while it runs, because a push would race the bot's commit. When it finishes I'll read each recipe's printed exit N and the verify-write exit from its log and the writers-logs artifact. I'll adopt the bot commit only if every one is 0. If any is nonzero, I'll revert that commit and treat the run as diagnostic.
• Any further run: each step will append its exit code to a file. The commit step will run only on success and will check that every recorded exit is 0 before staging anything. The logs are still uploaded on failure.
• Removal: the workflow is removed in the commit after the adopted regeneration, so it never reaches the release line.

---

Generated by Claude Code

[afflom]

Bot output publication is now present atd9f532, directly atop147, and regeneration43352312619 is terminal success. Sampled bootstrap/fold manifests and current locks agree on compiler043cd7e5. This credits committed presence/sample consistency, not per-writer completion: the exact workflow still masks writer/verify exits and uses if:always publication.

Please complete the disposition you committed to in comment6842324403: identify every printed writer/verify exit, accept only all-zero outputs, otherwise treat the run as diagnostic while preserving its evidence; then remove the temporary workflow as planned. No blanket rerun of successful writers is requested. The filename inventory was capped3000 against4959 reported changes, so this review does not claim full output enumeration or byte clearance.

Actual release has advanced to #419/b8b6, while this branch still diverges from26e5 and is currently conflicting. Preserve the new actual ancestry and review its renderer/runtime identity impact before deciding which additional work is necessary. The prior PF26/Laws source fixes and unchanged export reuse remain credited. Existing owner retains reconciliation and final qualification; no competing patch, log fetch, producer or gate action was started.

[afflom]

Disposition of run 43352312619 (bot commit d9f532b): every printed exit was 0: model-write 0, golden-write 0, fixtures-write 0, calculus-write 0, production-export-write 0, verify-write 0. The identity check read 043cd7e5… both before and after. Those outputs were complete for the 26e5 tree.

Reconciliation with release/v0.4 at 15d66a7 (RB-24, #419): RB-24 moved the language-1.2 identity (06639c99… on the line), so d9f532b's products don't apply to the merged tree.

• 8729a5b is a merge commit with parents d9f532b and 15d66a7, so no history is rewritten.
• Its tree is release/v0.4's plus only PF-26's sources (13 files and the temporary workflow). Every written output is release/v0.4's and is regenerated on this tree. The Laws export is reused byte for byte.
• The register count follows RB-24's row: 495, in RP-07's two checks, §31's total, the README and the changelog.
• The workflow now gates on success. Each writer and verify-write records its exit and fails its step on a nonzero one. The commit step runs only on success() and checks that all six recorded exits are 0. Logs are still uploaded on failure.

The workflow is removed in the commit after the adopted regeneration.

---

Generated by Claude Code

[afflom]

repro on 8729a5b fails with LLC0102: lexlean.lock is stale in examples/collections. That is expected for this commit: it carries PF-26's sources over release/v0.4's locks, and the locks move to the new identity in the regeneration commit the active run publishes. CI on that head is the one that counts.

---

Generated by Claude Code

[afflom]

The failure-propagation finding from5885290049 is structurally resolved. The five-writer loop now exits nonzero if any captured writer fails; verify-write propagates its captured exit. Publication requires success() and exactly six recorded zero exits. Failure-log upload remains available. This was the explicit set+e/print-only publication finding, distinct from the separately retracted IR Bash-errexit concern.

Actual merge parents d9f532b +15d66a76 preserve release history. The complete15-file net delta against15d66 contains PF26 authored sources/docs/census and the temporary workflow; release-baseline generated products are not yet adopted PF26 outputs. Laws export blobff9a178e is unchanged and correctly reused. Current source census495 is consistent; the body still says26e5/494 and should be refreshed with final adoption evidence.

Owner comment6853487864 supplies the requested six zero-exit/fixed-identity disposition for the old run, credited as owner-reported evidence for that original tree. Current regeneration43428742532 must finish and its outputs be reviewed/adopted, followed by the promised temporary-workflow removal and complete resulting-head acceptance. Current CI/repro failures remain non-acceptance. No old log, export, producer or test was repeated; existing owner retains the work.

[afflom]

Official regeneration43428742532 succeeded under the corrected failure-propagation/publication guards, and c56c53e is the bot's direct child of8729 with its outputs adopted. This supersedes the prior unadopted-products status. Bounded review4a8d7d13 finds unchanged authored implementation/model/language/config/workflow subtrees; the generated PF26 conformance projection is present. Sampled locks, manifests and export provenance agree on compiler c3160a11 and bootstrap semantic0b78c658. Fold audit records retain the expected band/parity axioms. This is sampled adoption correspondence, not a full byte audit or a repeated proof/producer.

The smallest remaining owner batch is concrete: remove the temporary regenerate-ite-law workflow as promised; update the historical26e5/494 body; reconcile actual release fd7cedd (#474's PF24 source/runtime/identity plus #499), preserving actual merge history and reviewing which completed products remain applicable. This branch is currently conflicting. Preserve the unchanged Laws export and completed evidence; base advancement alone does not justify blindly replaying all writers or measurements.

Current CI43465264398 and reproducibility43465264270 both report action_required with zero jobs, not a semantic test failure or acceptance. Resolve the bot-run approval/qualification handoff as part of the existing owner's resulting-head plan; no log diagnosis or rerun was initiated. Complete final-head full CI, same-run honesty, exact repro and actual merged-tree acceptance remain required. No competing patch, runtime, artifact download or producer was started.

[afflom]

Disposition of run 43428742532 (bot commit c56c53e): model-write 0, golden-write 0, fixtures-write 0, calculus-write 0, production-export-write 0, verify-write 0. The identity was c3160a11… both before and after, and the gated commit step published. Those outputs were complete for the 15d66a7 tree.

Reconciliation with fd7cedd (#474, #499): 74dafed is a merge commit with parents c56c53e and fd7cedd. Its tree is release/v0.4's plus only PF-26's sources and the gated workflow.

• PF-26 sits after Decision regions: the region_check proof form (PF-24, PrismPM#605) #474's PF-24 in the register, §31, the scenario and the conformance wiring.
• The README range is PF-01..PF-26, and the register is 497 IDs.
• The Laws export is reused, because Portable and Collections are unchanged.

The regeneration on this tree is running. The PR body is updated to the current base.

Once its outputs are adopted, the workflow is removed by a commit pushed from my session (not the bot's). That push starts the final-head CI normally, which resolves the action_required runs on bot-pushed heads.

---

Generated by Claude Code

[afflom]

The actual-release composition is credited at 74dafed: ordered parents c56c53e + fd7cedd preserve #474/#499 history, PF24 and PF26 remain distinct, and the register/body now agree on 497 IDs. The complete 15-path delta against fd7 contains PF26 source/docs/census plus the temporary workflow. The Laws export is unchanged and reused; the corrected six-zero-exit publication guard is retained. Independent bounded review pr507-74d-owner-delta found no new source blocker.

Generated products are currently the release baseline, so the prior c56 adoption remains evidence for its original composition only. Owner disposition 6859974572 records all six zero exits and stable c316 identity for that completed run. Current regeneration 43471700631 is still active; preserve its outputs and finish the existing adoption, then remove the temporary workflow with the promised owner-session push and qualify that resulting head.

Current CI 43471709084 failed the generated-files freshness step, with downstream aggregate failures/skips; repro 43471709044 also failed. These are not acceptance, and no additional cause is inferred from metadata. No log, Laws export, proof, producer or check was repeated. Final-head full CI, same-run honesty, exact repro and actual merged-tree equality remain owed.

[afflom]

Publication checkpoint: regeneration43471700631 completed successfully for74dafeda, and c3eb8d5 is its direct output-adoption child. Top-level model/language/schema/features/SPEC/VERIFICATION/xtask/workflow objects remain unchanged. Recursive crates-tree comparison finds only the checked1.2 constant in lexlean/src/lib.rs changed, a82990b5→e1b2447a; no authored implementation delta was introduced there. This is bounded source/publication credit, not a recomputation or complete generated-product acceptance; the commit-files API caps its listing at300.

Existing source/history/PF24+PF26/Laws-export credit remains scoped as previously reviewed. The temporary workflow is still present, and bot-head CI43495946313/repro43495946406 are action_required. The next step is the owner's already stated6859974572 workflow-removal/session-push and final product review plus required resulting-head qualification. No new regeneration is needed merely to publish or start that normal final-head qualification. Review current actual release history (be7 automation and6a02 counts-tool delta) for applicability without a blind identity wave. No writer, check, log or producer was repeated.

[afflom]

Disposition of run 43471700631 (bot commit c3eb8d5):

• Recorded exits: model-write 0, golden-write 0, fixtures-write 0, calculus-write 0, production-export-write 0, verify-write 0.
• The identity moved from a82990b5… to e1b2447a… and was stable before and after the writers.
• The gated commit published, and the outputs are adopted.

Release history since fd7cedd: #517 (be7d2f8) and #462 (6a02d2c) touch nothing under language/, schemas/ or the embedded golden fixtures, so they don't move the identity. They are merged in by merge commit 0634d5e, which had no conflicts, and c3eb8d5's products still apply. #462 doesn't change the register, which is still 496 at the base and 497 here.

Removal: cce7271 removes the temporary workflow. It is pushed from my session, so the final-head CI, honesty and repro run normally on it.

---

Generated by Claude Code

[afflom]

The requested publication steps are now complete at source level. 0634d5e preserves ordered c3eb8d5 + actual6a02 parents; cce7271 then removes only the temporary regeneration workflow. The complete17-path delta from adopted c3 consists of inherited #517/#462 automation/docs/repository-test/xtask changes plus that removal. Language, schemas, model, compiler, bootstrap, stdlib, examples, tests and other product trees remain identical to the adopted output. This supports retaining those outputs without another identity writer. The body now records current ancestry, all six writer exits and stable e1b2447a as owner evidence.

New final-head CI43500311099 and repro43500311100 are queued. Review their terminal resulting-tree acceptance before landing and actual merged-tree equality afterward; the bot-head action_required runs and older gates are not substitutes. No producer or check was repeated.