proof(lean4/LambdaCNO): close church_zero (1 of 6); document 5 spec-blocked sorries

L168 church_zero example
  - Was FALSE as stated. `(λf.λx.x)(λf.λx.x)` β-reduces by substituting
    the second copy for `f` in `LAbs (LVar 0)` — but `f` (de Bruijn 1
    inside the inner LAbs) does not occur, so the result is
    `LAbs (LVar 0)` = `lambda_id`, NOT `church_zero`. Restated to the
    correct target and closed in a single β-step.

The other 5 LambdaCNO sorries are spec-blocked, not proof-blocked.
Replaced bare `sorry` with detailed deferral comments enumerating the
spec choices the user needs to make:

  L114 lambda_id_is_cno (1 sorry inside)
    - β-reduction (λx.x) arg →* arg IS closed cleanly.
    - Remaining sorry is `isNormalForm arg` inside `evaluatesTo`.
      For arbitrary arg this is false; spec needs an arg-is-value
      hypothesis on `isLambdaCNO`, OR drop `isNormalForm nf` from
      `evaluatesTo`, OR restrict the universal to normal-form args.

  L138/L141 lambda_cno_composition (2 sorries inside)
    - `isLambdaCNO f` only gives `LApp f arg →* arg`; it does NOT tell
      us f = LAbs body, so we cannot perform the outer β-reduction.
      Spec needs either a syntactic f = LAbs _ constraint, an
      arg-as-value hypothesis, or an η-equivalence reformulation.

  L158 y_not_cno (1 sorry inside)
    - BetaReduceStar is inductive (only finite reduction sequences),
      so "no normal form exists for Y" cannot be proved directly. Need
      either an axiom y_combinator_no_normal_form (cheapest, matches
      file's existing axiom-heavy style - cf. eta_equivalence), a
      coinductive reformulation of reduction, or strong-normalization.

  L185 eta_expanded_id_is_cno (1 sorry, as written)
    - Same arg-is-value gap; the original explicit β-walk now actually
      builds under v4.16.0 (presumably because the seqComp abbrev
      change + ProgramState BEq derivation in CNO.lean indirectly
      affected simp normalization). Termination conjunct still gated
      on the spec choice.

LambdaCNO file builds cleanly: 4 declarations with sorry, all documented.

Author: hyperpolymath

proofs/lean4/LambdaCNO.lean

@@ -96,6 +96,21 @@ def isLambdaCNO (t : LambdaTerm) : Prop :=
 
 /-! ## Main Theorem: Identity is a CNO -/
 
+/-- Identity is a (lambda) CNO.
+
+    Partially proved: the β-reduction `(λx.x) arg →* arg` IS closed
+    cleanly. What remains as `sorry` is the `isNormalForm arg` conjunct
+    embedded in `evaluatesTo`.
+
+    DEFERRED — spec gap, not a proof gap. `isLambdaCNO` (line 92)
+    requires there *exists* a normal form `nf` of `LApp t arg`. For an
+    arbitrary `arg` this is false (e.g. `(λx.x)((λy.y)z)` is reachable
+    but not in normal form). The spec needs ONE of:
+      (a) Add an `arg`-is-value (or `isNormalForm arg`) hypothesis
+          inside the universal quantifier in `isLambdaCNO`; OR
+      (b) Drop `isNormalForm nf` from `evaluatesTo`; OR
+      (c) Restrict `isLambdaCNO` to quantify only over normal-form args.
+    Each choice changes downstream theorems. Defer to user. -/
 theorem lambda_id_is_cno : isLambdaCNO lambda_id := by
   unfold isLambdaCNO lambda_id
   intro arg
@@ -104,16 +119,16 @@ theorem lambda_id_is_cno : isLambdaCNO lambda_id := by
     exists arg
     unfold evaluatesTo
     constructor
-    · -- (λx.x) arg →* arg
+    · -- (λx.x) arg →* arg — provable directly.
       apply BetaReduceStar.beta_step
       · apply BetaReduce.beta_app
       · unfold subst
         simp
         apply BetaReduceStar.beta_refl
-    · -- arg is in normal form (assuming it's a value)
-      sorry  -- Requires assumption that arg is a value
+    · -- DEFERRED — `isNormalForm arg` requires arg-is-value spec change.
+      sorry
 
-  · -- Identity
+  · -- Identity: same single β-step as above.
     apply BetaReduceStar.beta_step
     · apply BetaReduce.beta_app
     · unfold subst
@@ -126,6 +141,19 @@ theorem lambda_id_is_cno : isLambdaCNO lambda_id := by
 def lambda_compose (f g : LambdaTerm) : LambdaTerm :=
   LAbs (LApp f (LApp g (LVar 0)))
 
+/-- Composing two lambda CNOs yields a CNO.
+
+    DEFERRED (×2) — spec gap. `isLambdaCNO f` only tells us that
+    `(LApp f arg) →* arg` for any `arg` — that "applying `f` returns
+    its argument back". It does NOT tell us `f = LAbs body`, so we
+    cannot pattern-match on `f` to perform the outer β-reduction of
+    `(λx. f (g x)) arg`. To close: ONE of
+      (a) `isLambdaCNO` should require `t = LAbs _` (rule out
+          non-abstraction "CNOs"); OR
+      (b) Add a value/normal-form hypothesis on `f`/`g`; OR
+      (c) Reformulate via the η-equivalence axiom on the outer LAbs.
+    The first sorry also inherits the arg-is-value gap from
+    `lambda_id_is_cno`. Defer to user. -/
 theorem lambda_cno_composition (f g : LambdaTerm) :
     isLambdaCNO f →
     isLambdaCNO g →
@@ -134,10 +162,9 @@ theorem lambda_cno_composition (f g : LambdaTerm) :
   unfold isLambdaCNO at *
   intro arg
   constructor
-  · -- Terminates
+  · -- DEFERRED — same arg-is-value gap as `lambda_id_is_cno`.
     sorry
-  · -- Identity: ((λx. f (g x)) arg) →* arg
-    -- Since f and g are both identity, this reduces to arg
+  · -- DEFERRED — requires `f`/`g` to be syntactic abstractions.
     sorry
 
 /-! ## Non-CNO Examples -/
@@ -148,24 +175,49 @@ def y_combinator : LambdaTerm :=
     (LAbs (LApp (LVar 1) (LApp (LVar 0) (LVar 0))))
     (LAbs (LApp (LVar 1) (LApp (LVar 0) (LVar 0)))))
 
-/-- Y is NOT a CNO because it doesn't terminate -/
+/-- Y is NOT a CNO because it doesn't terminate.
+
+    DEFERRED — Lean's `BetaReduceStar` is *inductive* (only finite
+    sequences), so "no normal form exists for Y" is a metatheoretic
+    claim that cannot be discharged via the existing reduction
+    relation. To close: ONE of
+      (a) Add an axiom: `axiom y_combinator_no_normal_form :
+          ¬ ∃ nf, evaluatesTo (LApp y_combinator lambda_id) nf` and
+          contradict `h_eval` with it (cheapest; matches the file's
+          existing axiom-heavy style — cf. `eta_equivalence`);
+      (b) Switch `BetaReduceStar` to coinductive and prove divergence
+          via that; OR
+      (c) Build a strong-normalization framework and show Y is not SN.
+    Defer to user. -/
 theorem y_not_cno : ¬ isLambdaCNO y_combinator := by
   unfold isLambdaCNO y_combinator
   intro h
-  -- Y applied to identity should terminate, but it doesn't
   have := h lambda_id
-  obtain ⟨⟨nf, h_eval⟩, _⟩ := this
-  sorry  -- Y diverges
+  obtain ⟨⟨_nf, _h_eval⟩, _⟩ := this
+  sorry
 
 /-! ## Church Encodings -/
 
 /-- Church encoding of zero: λf.λx.x -/
 def church_zero : LambdaTerm :=
   LAbs (LAbs (LVar 0))
 
-/-- Church encoding is a CNO for zero applied to zero -/
-example : BetaReduceStar (LApp church_zero church_zero) church_zero := by
-  sorry
+/-- Church encoding β-reduces to the identity when applied to itself.
+
+    Spec correction: the original example claimed
+    `(λf.λx.x)(λf.λx.x) →* λf.λx.x` (back to `church_zero`). That is
+    *false*: β-reducing `(LAbs (LAbs (LVar 0))) (LAbs (LAbs (LVar 0)))`
+    substitutes the second copy for `f` in `LAbs (LVar 0)`, but `f`
+    (= de Bruijn 1 inside the inner LAbs) does not occur, so the
+    result is `LAbs (LVar 0)` = `lambda_id`, *not* `church_zero`.
+    Restating to the correct target makes the example provable in one
+    β-step. -/
+example : BetaReduceStar (LApp church_zero church_zero) lambda_id := by
+  apply BetaReduceStar.beta_step _ lambda_id
+  · -- (LAbs (LAbs (LVar 0))) (LAbs (LAbs (LVar 0))) →β subst 0 _ (LAbs (LVar 0))
+    --                                              = LAbs (LVar 0) = lambda_id
+    exact BetaReduce.beta_app (LAbs (LVar 0)) church_zero
+  · exact BetaReduceStar.beta_refl lambda_id
 
 /-! ## Eta Equivalence -/