PF000E · theorem body

fermat_four_bounded_descent

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Ordinary bounded natural induction rejects every positive Fermat-four counterexample once an exact strictly smaller counterexample constructor is supplied.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ B. ∀ h. ∀ a. ∀ b. Le(h,B) → FermatFourStrictDescent() → ¬FermatFourCounterexample(a,b,h)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

CF0014 FermatFourCounterexample CF0015 FermatFourStrictDescent PD0001 Le

In local proof propositions

ND0072 SmallerFermatFourCounterexample PD0001 Le PD0002 Lt
Exact expanded first-order statement
forall B h a b. (exists gap. gap + h = B) -> (forall pff_first_bounded pff_second_bounded pff_hypotenuse_bounded. ((~((pff_first_bounded) = 0) /\ (~((pff_second_bounded) = 0) /\ (~((pff_hypotenuse_bounded) = 0) /\ ((pff_first_bounded) * (pff_first_bounded) * (pff_first_bounded) * (pff_first_bounded) + (pff_second_bounded) * (pff_second_bounded) * (pff_second_bounded) * (pff_second_bounded) = (pff_hypotenuse_bounded) * (pff_hypotenuse_bounded)))))) -> exists pff_smaller_first_bounded pff_smaller_second_bounded pff_smaller_hypotenuse_bounded. (((~((pff_smaller_first_bounded) = 0) /\ (~((pff_smaller_second_bounded) = 0) /\ (~((pff_smaller_hypotenuse_bounded) = 0) /\ ((pff_smaller_first_bounded) * (pff_smaller_first_bounded) * (pff_smaller_first_bounded) * (pff_smaller_first_bounded) + (pff_smaller_second_bounded) * (pff_smaller_second_bounded) * (pff_smaller_second_bounded) * (pff_smaller_second_bounded) = (pff_smaller_hypotenuse_bounded) * (pff_smaller_hypotenuse_bounded)))))) /\ (exists pff_gap_bounded. pff_gap_bounded + S pff_smaller_hypotenuse_bounded = pff_hypotenuse_bounded))) -> ~((~((a) = 0) /\ (~((b) = 0) /\ (~((h) = 0) /\ ((a) * (a) * (a) * (a) + (b) * (b) * (b) * (b) = (h) * (h))))))

Proof neighborhood

Direct theorem prerequisites

le_zero · Stable closed le_trans · Stable closed le_of_succ_le_succ · Stable closed

Direct theorem dependents

PF000F fermat_four_no_square_from_descent

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

50 script commands · 10 reading checkpoints · 3 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

01Fix variables and assumptionsL1–1

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro B
02Induction on BL2–8

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction B
  2. L3
    intro h
  3. L4
    intro a
  4. L5
    intro b
  5. L6
    intro hbound
  6. L7
    intro hstep
  7. L8
    intro hcounter
03Separate the logical casesL9–11

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L9
    cases hcounter
  2. L10
    cases hcounter_right
  3. L11
    cases hcounter_right_right
04Use earlier factsL12–15

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L12
    apply hcounter_right_right_left
  2. L13
    specialize le_zero h
  3. L14
    apply le_zero
  4. L15
    exact hbound
05Fix variables and assumptionsL16–21

Work with arbitrary variables or the premises of the current implication.

  1. L16
    intro h
  2. L17
    intro a
  3. L18
    intro b
  4. L19
    intro hbound
  5. L20
    intro hstep
  6. L21
    intro hcounter
06Establish hsmallerL22–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hstep.

  1. L22
    have hsmaller : ∃ first. ∃ second. ∃ smaller. SmallerFermatFourCounterexample(first,second,smaller,h)Definitions: SmallerFermatFourCounterexample(first,second,smaller,h)Original native command in the exact edition
  2. L23
    specialize hstep a
  3. L24
    specialize hstep b
  4. L25
    specialize hstep h
  5. L26
    apply hstep
  6. L27
    exact hcounter
07Separate the logical casesL28–31

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L28
    cases hsmaller
  2. L29
    cases hsmaller_witness
  3. L30
    cases hsmaller_witness_witness
  4. L31
    cases hsmaller_witness_witness_witness
08Establish hsuccessor_boundL32–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le trans.

  1. L32
    have hsuccessor_bound : Lt(x2,S B)Definitions: Lt(x2,S B)Original native command in the exact edition
  2. L33
    specialize le_trans (S x2)
  3. L34
    specialize le_trans h
  4. L35
    specialize le_trans (S B)
  5. L36
    apply le_trans
  6. L37
    exact hsmaller_witness_witness_witness_right
  7. L38
    exact hbound
09Establish hsmaller_boundL39–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L39
    have hsmaller_bound : Le(x2,B)Definitions: Le(x2,B)Original native command in the exact edition
  2. L40
    specialize le_of_succ_le_succ x2
  3. L41
    specialize le_of_succ_le_succ B
  4. L42
    apply le_of_succ_le_succ
  5. L43
    exact hsuccessor_bound
  6. L44
    specialize IH x2
  7. L45
    specialize IH x
  8. L46
    specialize IH x1
  9. L47
    apply IH
  10. L48
    exact hsmaller_bound
10Use earlier factsL49–50

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L49
    exact hstep
  2. L50
    exact hsmaller_witness_witness_witness_left

Library-wide reading audit

Original defined command ledger · 50 lines
  1. 0001intro B
  2. 0002induction B
  3. 0003intro h
  4. 0004intro a
  5. 0005intro b
  6. 0006intro hbound
  7. 0007intro hstep
  8. 0008intro hcounter
  9. 0009cases hcounter
  10. 0010cases hcounter_right
  11. 0011cases hcounter_right_right
  12. 0012apply hcounter_right_right_left
  13. 0013specialize le_zero h
  14. 0014apply le_zero
  15. 0015exact hbound
  16. 0016intro h
  17. 0017intro a
  18. 0018intro b
  19. 0019intro hbound
  20. 0020intro hstep
  21. 0021intro hcounter
  22. 0022have hsmaller : ∃ first. ∃ second. ∃ smaller. SmallerFermatFourCounterexample(first,second,smaller,h)
    Exact native replay linehave hsmaller : exists first second smaller. (((~((first) = 0) /\ (~((second) = 0) /\ (~((smaller) = 0) /\ ((first) * (first) * (first) * (first) + (second) * (second) * (second) * (second) = (smaller) * (smaller)))))) /\ (exists gap. gap + S smaller = h))
  23. 0023specialize hstep a
  24. 0024specialize hstep b
  25. 0025specialize hstep h
  26. 0026apply hstep
  27. 0027exact hcounter
  28. 0028cases hsmaller
  29. 0029cases hsmaller_witness
  30. 0030cases hsmaller_witness_witness
  31. 0031cases hsmaller_witness_witness_witness
  32. 0032have hsuccessor_bound : Lt(x2,S B)
    Exact native replay linehave hsuccessor_bound : exists gap. gap + S x2 = S B
  33. 0033specialize le_trans (S x2)
  34. 0034specialize le_trans h
  35. 0035specialize le_trans (S B)
  36. 0036apply le_trans
  37. 0037exact hsmaller_witness_witness_witness_right
  38. 0038exact hbound
  39. 0039have hsmaller_bound : Le(x2,B)
    Exact native replay linehave hsmaller_bound : exists gap. gap + x2 = B
  40. 0040specialize le_of_succ_le_succ x2
  41. 0041specialize le_of_succ_le_succ B
  42. 0042apply le_of_succ_le_succ
  43. 0043exact hsuccessor_bound
  44. 0044specialize IH x2
  45. 0045specialize IH x
  46. 0046specialize IH x1
  47. 0047apply IH
  48. 0048exact hsmaller_bound
  49. 0049exact hstep
  50. 0050exact hsmaller_witness_witness_witness_left