TF0001

beta_two_square_prefix_drop_last

Restricting a successor-length prefix preserves every witnessed two-square factor representation.

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

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.

The exact G025 progression-prime milestone is fully proved in unchanged constructive arithmetic; Mod4Three deliberately reuses its existing Quadratic Reciprocity definition PD0012. The much stronger full Dirichlet progression-prime milestone G030 remains open.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ l. (∀ x. ∀ y. Lt(x,S l) → BetaAt(b,c,x,y) → ∃ z. ∃ n. y = z · z + n · n) → ∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → ∃ z. ∃ n. y = z · z + n · n

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Lt(a,b) · 2BetaAt(b,c,i,x) · 2

Actual proof prerequisites

le_succ · checked external prerequisite
Original expanded first-order statement 
forall b c l. (forall ftsf_index_drop_next ftsf_factor_drop_next. (exists ftsf_gap_drop_next_bound. ftsf_gap_drop_next_bound + S ftsf_index_drop_next = (S l)) -> (((exists ff_h_ftsf_drop_next_entry. ff_h_ftsf_drop_next_entry + S (ftsf_factor_drop_next) = S ((S (ftsf_index_drop_next)) * c)) /\ exists ff_q_ftsf_drop_next_entry. b = ff_q_ftsf_drop_next_entry * S ((S (ftsf_index_drop_next)) * c) + (ftsf_factor_drop_next))) -> (exists ftsf_first_drop_next_representation ftsf_second_drop_next_representation. (ftsf_factor_drop_next) = ftsf_first_drop_next_representation * ftsf_first_drop_next_representation + ftsf_second_drop_next_representation * ftsf_second_drop_next_representation)) -> (forall ftsf_index_drop_old ftsf_factor_drop_old. (exists ftsf_gap_drop_old_bound. ftsf_gap_drop_old_bound + S ftsf_index_drop_old = (l)) -> (((exists ff_h_ftsf_drop_old_entry. ff_h_ftsf_drop_old_entry + S (ftsf_factor_drop_old) = S ((S (ftsf_index_drop_old)) * c)) /\ exists ff_q_ftsf_drop_old_entry. b = ff_q_ftsf_drop_old_entry * S ((S (ftsf_index_drop_old)) * c) + (ftsf_factor_drop_old))) -> (exists ftsf_first_drop_old_representation ftsf_second_drop_old_representation. (ftsf_factor_drop_old) = ftsf_first_drop_old_representation * ftsf_first_drop_old_representation + ftsf_second_drop_old_representation * ftsf_second_drop_old_representation))

Complete unchanged native tactic proof

All 16 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

16 script commands · 2 reading checkpoints · 0 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–8

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro hprefix
  5. L5
    intro i
  6. L6
    intro a
  7. L7
    intro hi
  8. L8
    intro ha
02Use earlier factsL9–16

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

  1. L9
    specialize hprefix i
  2. L10
    specialize hprefix a
  3. L11
    apply hprefix
  4. L12
    specialize le_succ (S i)
  5. L13
    specialize le_succ l
  6. L14
    apply le_succ
  7. L15
    exact hi
  8. L16
    exact ha

Library-wide reading audit

Original defined command ledger · 16 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro hprefix
  5. 0005intro i
  6. 0006intro a
  7. 0007intro hi
  8. 0008intro ha
  9. 0009specialize hprefix i
  10. 0010specialize hprefix a
  11. 0011apply hprefix
  12. 0012specialize le_succ (S i)
  13. 0013specialize le_succ l
  14. 0014apply le_succ
  15. 0015exact hi
  16. 0016exact ha