[humuhumu33]

Fixes #291 on the 0.5.0 line. simplify can now discharge a conditional lemma's condition from a hypothesis of the theorem's statement, so a theorem of the form P x → (f x = 0 ↔ Q x) is proved from a lemma that holds under P x. This is the statement UOR-Foundation/MCP#24 could not write.

The form (SPEC §17.12, PF-25)

The row added to the §17.12 table of language-1.2 constructs:

| simplify hypotheses | lexlean/semantic-module/2 | {"kind":"simplify","definitions":[...],"hypotheses":[h...]} (hypotheses omitted when empty): names for the leading premises of the goal, in order. It lowers to intro h1 … hn and then simp only [h1, …, hn, d1, …]: the hypotheses lead the rule set, which is still exactly the names the source states. Lean discharges the condition of a conditional rule by simplifying it with the same set, so a prior theorem whose rewrite holds under a condition (P x → f x = v) rewrites where a named hypothesis discharges that condition. Linking requires the goal to be the theorem's statement (the proof itself or a branch of cases or induction), at most as many names as it has leading implications, and names that are fresh and distinct, so none of them is among the definitions. A theorem whose hypotheses do not discharge a rule's condition is rejected by Lean (LLV7002). |

The hypothesis is bound by the statement's →, the way nested_induction binds its induction hypotheses in #278. No tactic, option or lemma comes from anywhere but the source, and no raw Lean enters.

In the notation:

theorem{
  name: three_byte_complete_zero_iff,
  parameters: [b1 : Nat, b2 : Nat, b3 : Nat],
  statement: (((leadE1ToEC b1) = true) -> (((scanThree b1 b2 b3) = 0) <-> (((inRange 128 b2 191) = true) /\ ((inRange 128 b3 191) = true)))),
  proof: simplify{definitions: [lead_e1_ec_step, three_byte_zero_iff], hypotheses: [lead]},
  axioms: [Classical.choice, Quot.sound, propext]
}

This lowers to:

  intro lead
  simp only [lead, lead_e1_ec_step, three_byte_zero_iff]

Register (R3)

• PF-25 (proofs, §17.12) is the one new row. Its statement covers the form, the linking refusals, and Lean's rejection of a hypothesis that does not discharge the condition. That rejection uses the existing LLV7002, so no new diagnostic code is registered. If you want a separate row or code for that refusal, say so.
• Numbering. PF-24 belongs to draft #263 PF-24: runtime bounds a law proof cites (split_exact, UTF-8 decode, UInt32 checked_add) #296, so this takes PF-25. The head contains release/v0.5 at 34cfc12 ([0.5.0] #113: release identity, §2.3 completion release 0.5.0 and §30 for languages 1.0-1.2 (RP-17, CL-18) #288 and #124: the general performance corpus (PC-01, PC-02, L4.6 of #106) #289), so the register count is 448.
• Commit order. 78a732a holds the row, the scenario and the failing conformance_pf_25. On that commit the case fails with unknown field `hypotheses` . The implementation follows in 186f028.

The case (conformance_pf_25)

The case builds a module in the shape of MCP#24's three-byte row for lead bytes E1..EC (Table 3-7):

• lead_e1_ec_step is conditional on the lead byte's class.
• three_byte_zero_iff holds for all bounds.
• three_byte_complete_zero_iff composes the two, as above.

Copy	Result
The module	Lean verifies it with exact policies: the step lemma [Quot.sound, propext], the zero test and the composed statement [Classical.choice, Quot.sound, propext]
The premise of the ED class (leadED b1 = true), which does not imply the lemma's condition	LLV7002, `simp` made no progress
A policy without Classical.choice	LLV7005
Hypotheses in a constructor branch, more names than premises, a parameter's name, a hypothesis also named among the definitions, the form under language 1.1	LLT4001 at linking, before any build output

The case also checks the generated Lean: intro lead, then simp only [lead, …].

Plants (VERIFICATION.md)

Each plant was one edit in a separate worktree, restored with git checkout. Each turns conformance_pf_25 red.

1. The hypotheses dropped from the simp set, with the intro kept. lexlean verify reports LLV7002, `simp` made no progress: no other rule discharges the condition.
2. The ED variant made true. The case fails because the copy now verifies.
3. The forged policy made the observed one. The case fails because no LLV7005 comes.

Identity

The language-1.2 compiler-semantics ID moves, from 5262e5b4… to 583ff8e2…. The reasons:

• The simplify alternatives of schemas/semantic-module-v2.schema.json and schemas/semantic-snapshot-v2.schema.json gain the optional hypotheses.
• semantic_ir moves from 15 to 16 and proof_lowering from 3 to 4, the convention [v0.4] Add language-model semantic components and compositional text-processing pipeline #30 and [0.5.0] Lemmas for universal equalities over list folds #117 followed.
• Languages 1.0 and 1.1 do not move.
• No existing module changes bytes, because the member is skipped when empty.

Commit f48de99 substitutes the ID and lets the writers regenerate their records: check-golden, check-calculus, check-production-export, check-fixtures, then verify-examples without uor-atlas. All 15 non-Atlas examples, compiler, stdlib and bootstrap verified under the new compiler, so every committed proof still verifies.

State of the base. #296 landed on release/v0.5 at 80bf4ba after this head was pushed, and it moves the same ID (to 9fdf4d30…). This PR therefore conflicts on every lock and expected record, and the ID it computes (583ff8e2…) is stale. #295 and #300 move the ID as well. The merge with #296 and one more run of the writers are needed once, on top of whichever identity PR lands last, so I have not repeated them for each landing. Say which order you want, or merge this one last.

Run locally (WSL, Linux x86-64, Lean 4.32.1)

• fmt, validate-model (446 ids), validate-spec-links and check-test-inventory pass.
• Clippy on lexlean and repo-conformance with -D warnings passes, and so do the 211 tests of cargo test -p lexlean --lib.
• On f48de99, before [0.5.0] #113: release identity, §2.3 completion release 0.5.0 and §30 for languages 1.0-1.2 (RP-17, CL-18) #288 landed, these conformance cases pass: conformance_pf_25, _pf_09, _pf_21, _pf_23, _sm_16, _sm_17, _rp_07 and _rp_11.
• The verification records of every non-Atlas project were rewritten by verify-examples --write.
• The branch merges release/v0.5 at 34cfc12 ([0.5.0] #113: release identity, §2.3 completion release 0.5.0 and §30 for languages 1.0-1.2 (RP-17, CL-18) #288, #124: the general performance corpus (PC-01, PC-02, L4.6 of #106) #289; the merge of #124: the general performance corpus (PC-01, PC-02, L4.6 of #106) #289 also regenerated the new performance-corpus example under this PR's ID, the only records that changed). Earlier it merged 655d9ae ([0.5.0] #113: release identity, §2.3 completion release 0.5.0 and §30 for languages 1.0-1.2 (RP-17, CL-18) #288). The merge resolves two appends, in CHANGELOG and VERIFICATION, and moves the README count to 446. The merge left the generated total of SPEC.md §31 at 445, so validate-model and validate-spec-links failed on b53aedb. The next commit regenerates it with validate-model --write, one line.
• After that commit, validate-model (446 ids), validate-spec-links (446 rows bijective) and check-test-inventory pass, and conformance_rp_07, _rp_11 and _pf_25 pass. On b53aedb, _rp_17 and _cl_18 also passed.
• [0.5.0] #113: release identity, §2.3 completion release 0.5.0 and §30 for languages 1.0-1.2 (RP-17, CL-18) #288's VERIFICATION record quotes lexlean --version output with the old 1.2 ID. It stays as recorded, because it is a past output.

Not verified locally

• uor-atlas. It was not verified here, because it is CI-only evidence. It is a language-1.0 project, whose ID does not move, and no file of it changed, so its records stand.
• The rest of just vv. That includes the full bdd suite, which is CI's.

🤖 Generated with Claude Code

[afflom]

Maintainer review of 551b0f985 (read from the diff against its merge-base 34cfc1282, nothing built). Accepted in shape; it lands on release/v0.5 after #300, once it is re-merged and regenerated. Nothing in PF-25 itself needs a design change.

What checked out. R3 order (78a732a95 holds the row, the scenario and conformance_pf_25 at conformance.rs:798; the implementation follows in 186f0284f); the statement is byte-equal at ids.toml:962, proofs.feature:170 and the §31 row, and both spec rows are made in spec/src/Chapter17.lex.tex:883 and IdsPF.lex.tex:191-197 with SPEC.md as their projection. The schema stays closed (hypotheses: array of names, minItems 1, uniqueItems, additionalProperties: false kept in both v2 schemas; the 1.1 schema untouched). Linking is the §17.12 rule as written: check_proof carries the goal (Some(statement) from check_theorem, through cases/induction, None through constructor), check_simplify_hypotheses (semantic.rs:8503-8534) requires 1.2, counts the leading implications, refuses excess, repeated and in-scope names, and the hypotheses join proof_binders, so binder hygiene refuses one spelled like a declaration or a built-in. The lowering (backend/semantic.rs:1219-1241) emits intro only when there are names and the rule set is exactly the source's names, hypotheses first. Every refusal is under a registered code (LLT4001, LLV7002, LLV7005; no new code, so ERRORS.md rightly unchanged). Three plants with red lines at VERIFICATION.md:17006-17062. No deferral marker.

Identity. Keep both bumps (semantic_ir 15→16, proof_lowering 3→4): the IR gains a member and the generated script gains a line form, which is what the two version (§21.2). Languages 1.0 and 1.1 do not move (their semantics files and every 1.0/1.1 lock are untouched). The branch's 583ff8e2… is superseded by the merged tree's digest in any case.

Before it can land (blocking, as you anticipated):

1. The branch is unmergeable: #263 PF-24: runtime bounds a law proof cites (split_exact, UTF-8 decode, UInt32 checked_add) #296 (PF-24) moved the same 1.2 ID, so 2,547 paths conflict (every regenerated record and lock, plus CONFORMANCE.md, README.md, SPEC.md, VERIFICATION.md, model/ids.toml, proofs.feature, IdsPF.lex.tex, spec/lexlean.lock, cases/proofs.rs, conformance.rs). Merge release/v0.5 (after [0.5.0] #279: a fallible loop's ends are in its function's tail (RB-21) #300 lands, so you do it once), resolve the PF-24/PF-25 appends, set the count to the merged register at README, SPEC §31 total and the CHANGELOG sentence, then rerun the writers on the merged tree (check-golden, check-calculus, check-production-export, check-fixtures, verify-examples --write, without the Atlas).
2. The PR body still says 446; state the merged count and the final 1.2 ID.

Nits, in the same push: the stray blank line after the "Register 445." CHANGELOG entry; proofs.rs:1 doc range (PF-01..PF-25) once PF-24 is in; conformance_pf_25 exercises the in-scope name but not a repeated name nor one spelled like a declaration, one refused copy of each would plant the two branches the schema and hygiene carry; and settle "hypotheses": []: the schema says minItems 1 while check_simplify_hypotheses is skipped on an empty list, so either the schema validation already refuses it before serde (then say so) or the check runs on the empty list too.

Order on the 0.5.0 line: #300 (one push owed, then merge), then this one, then #295. Say the head here when it is up.

---

Generated by Claude Code

[afflom]

release/v0.5 now carries the 0.4.0 line (#322 merged at 61b4638cd; register 472; #279's loop-end row is RB-22 and #126 stage 2's rows are SL-06 to SL-08, the release/v0.4 rows keeping their numbers). Merge origin/release/v0.5 into this branch and recount; it then proceeds in the v0.5 order. The second forward merge (H5, H6, the release-workflow fixes) follows #304's landing.

---

Generated by Claude Code

[afflom]

release/v0.5 moved: the second forward merge (#327) is merged at 1046646ed, bringing release/v0.4 at a1b925dc6 (the v0.4.0 tag, H5 #298, H6 #304, the release-workflow fixes #320/#321/#323) onto this line. Language 1.2 identity dcdf8a721708f0a9c5e57303f78eef5f5e37c58b7a11a04272d8670f618a699f (1.1 and 1.0 unchanged); register 474 (RB-21 and SP-30 join; RB-16, RB-17, RB-19, RB-20, SP-29, BS-05, BS-06, BS-09 restated). Before the next push here, merge origin/release/v0.5 by merge commit and recount; locks and records are regenerated at the landing, not in the draft.

---

Generated by Claude Code