FS005E · theorem body

four_square_signed_absolute_congruence_divisible

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

Any natural absolute value of a balanced signed expression congruent to zero has an actual divisibility witness.

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

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

∀ k. ∀ positive. ∀ negative. ∀ magnitude. ModEq(k,positive,negative) → positive = negative + magnitude ∨ negative = positive + magnitude → Dvd(k,magnitude)

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

PD0003 Dvd PD0008 ModEq

In local proof propositions

none
Exact expanded first-order statement
forall k positive negative magnitude. (exists ftcn_left_fssq_absolute_mod ftcn_right_fssq_absolute_mod. (positive) + (k) * ftcn_left_fssq_absolute_mod = (negative) + (k) * ftcn_right_fssq_absolute_mod) -> (((positive) = (negative) + magnitude) \/ ((negative) = (positive) + magnitude)) -> (exists ftcn_factor_fssq_absolute_multiple. (magnitude) = (k) * ftcn_factor_fssq_absolute_multiple)

Proof neighborhood

Direct theorem prerequisites

mod_eq_symm · Stable closed mod_eq_ordered_gap_multiple · Stable closed add_comm · Stable closed

Direct theorem dependents

FS0057 four_square_signed_absolute_block_representation

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

31 script commands · 12 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–6

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

  1. L1
    intro k
  2. L2
    intro positive
  3. L3
    intro negative
  4. L4
    intro magnitude
  5. L5
    intro hcongruent
  6. L6
    intro habsolute
02Separate the logical casesL7–7

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

  1. L7
    cases habsolute
03Use earlier factsL8–12

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

  1. L8
    specialize mod_eq_ordered_gap_multiple k
  2. L9
    specialize mod_eq_ordered_gap_multiple magnitude
  3. L10
    specialize mod_eq_ordered_gap_multiple negative
  4. L11
    specialize mod_eq_ordered_gap_multiple positive
  5. L12
    apply mod_eq_ordered_gap_multiple
04Calculate and transport equalitiesL13–13

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L13
    trans negative + magnitude
05Use earlier factsL14–14

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

  1. L14
    apply add_comm
06Calculate and transport equalitiesL15–15

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L15
    symm
07Use earlier factsL16–25

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

  1. L16
    exact habsolute_left
  2. L17
    specialize mod_eq_symm k
  3. L18
    specialize mod_eq_symm positive
  4. L19
    specialize mod_eq_symm negative
  5. L20
    apply mod_eq_symm
  6. L21
    exact hcongruent
  7. L22
    specialize mod_eq_ordered_gap_multiple k
  8. L23
    specialize mod_eq_ordered_gap_multiple magnitude
  9. L24
    specialize mod_eq_ordered_gap_multiple positive
  10. L25
    specialize mod_eq_ordered_gap_multiple negative
08Use earlier factsL26–26

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

  1. L26
    apply mod_eq_ordered_gap_multiple
09Calculate and transport equalitiesL27–27

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L27
    trans positive + magnitude
10Use earlier factsL28–28

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

  1. L28
    apply add_comm
11Calculate and transport equalitiesL29–29

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L29
    symm
12Use earlier factsL30–31

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

  1. L30
    exact habsolute_right
  2. L31
    exact hcongruent

Library-wide reading audit

Original defined command ledger · 31 lines
  1. 0001intro k
  2. 0002intro positive
  3. 0003intro negative
  4. 0004intro magnitude
  5. 0005intro hcongruent
  6. 0006intro habsolute
  7. 0007cases habsolute
  8. 0008specialize mod_eq_ordered_gap_multiple k
  9. 0009specialize mod_eq_ordered_gap_multiple magnitude
  10. 0010specialize mod_eq_ordered_gap_multiple negative
  11. 0011specialize mod_eq_ordered_gap_multiple positive
  12. 0012apply mod_eq_ordered_gap_multiple
  13. 0013trans negative + magnitude
  14. 0014apply add_comm
  15. 0015symm
  16. 0016exact habsolute_left
  17. 0017specialize mod_eq_symm k
  18. 0018specialize mod_eq_symm positive
  19. 0019specialize mod_eq_symm negative
  20. 0020apply mod_eq_symm
  21. 0021exact hcongruent
  22. 0022specialize mod_eq_ordered_gap_multiple k
  23. 0023specialize mod_eq_ordered_gap_multiple magnitude
  24. 0024specialize mod_eq_ordered_gap_multiple positive
  25. 0025specialize mod_eq_ordered_gap_multiple negative
  26. 0026apply mod_eq_ordered_gap_multiple
  27. 0027trans positive + magnitude
  28. 0028apply add_comm
  29. 0029symm
  30. 0030exact habsolute_right
  31. 0031exact hcongruent