FS0057 · theorem body

four_square_signed_absolute_block_representation

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

Four signed absolute-coordinate blocks with actual modular balance construct every quotient coordinate and the represented prime-multiple quotient.

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

∀ p. ∀ k. ∀ r. ∀ p0. ∀ p1. ∀ p2. ∀ p3. ∀ n0. ∀ n1. ∀ n2. ∀ n3. ∀ m0. ∀ m1. ∀ m2. ∀ m3. ¬k = 0 → p · k · (k · r) = m0 · m0 + m1 · m1 + m2 · m2 + m3 · m3 → ModEq(k,p0,n0) → p0 = n0 + m0 ∨ n0 = p0 + m0 → ModEq(k,p1,n1) → p1 = n1 + m1 ∨ n1 = p1 + m1 → ModEq(k,p2,n2) → p2 = n2 + m2 ∨ n2 = p2 + m2 → ModEq(k,p3,n3) → p3 = n3 + m3 ∨ n3 = p3 + m3 → ∃ x. ∃ y. ∃ z. ∃ n. p · r = x · x + y · y + z · z + n · n

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

PD0008 ModEq

In local proof propositions

none
Exact expanded first-order statement
forall p k r p0 p1 p2 p3 n0 n1 n2 n3 m0 m1 m2 m3. ~(k = 0) -> (p * k) * (k * r) = (m0 * m0 + m1 * m1 + m2 * m2 + m3 * m3) -> (exists ftcn_left_fsso_balance_0 ftcn_right_fsso_balance_0. (p0) + (k) * ftcn_left_fsso_balance_0 = (n0) + (k) * ftcn_right_fsso_balance_0) -> (((p0) = (n0) + m0) \/ ((n0) = (p0) + m0)) -> (exists ftcn_left_fsso_balance_1 ftcn_right_fsso_balance_1. (p1) + (k) * ftcn_left_fsso_balance_1 = (n1) + (k) * ftcn_right_fsso_balance_1) -> (((p1) = (n1) + m1) \/ ((n1) = (p1) + m1)) -> (exists ftcn_left_fsso_balance_2 ftcn_right_fsso_balance_2. (p2) + (k) * ftcn_left_fsso_balance_2 = (n2) + (k) * ftcn_right_fsso_balance_2) -> (((p2) = (n2) + m2) \/ ((n2) = (p2) + m2)) -> (exists ftcn_left_fsso_balance_3 ftcn_right_fsso_balance_3. (p3) + (k) * ftcn_left_fsso_balance_3 = (n3) + (k) * ftcn_right_fsso_balance_3) -> (((p3) = (n3) + m3) \/ ((n3) = (p3) + m3)) -> (exists fsl_a_fsso_quotient fsl_b_fsso_quotient fsl_c_fsso_quotient fsl_d_fsso_quotient. (p * r) = fsl_a_fsso_quotient * fsl_a_fsso_quotient + fsl_b_fsso_quotient * fsl_b_fsso_quotient + fsl_c_fsso_quotient * fsl_c_fsso_quotient + fsl_d_fsso_quotient * fsl_d_fsso_quotient)

Proof neighborhood

Direct theorem prerequisites

FS0056 four_square_signed_divisible_norm_product_representation FS005E four_square_signed_absolute_congruence_divisible

Direct theorem dependents

FS004Q four_square_signed_orientation_mask_00 FS004R four_square_signed_orientation_mask_01 FS004S four_square_signed_orientation_mask_02 FS004T four_square_signed_orientation_mask_03 FS004U four_square_signed_orientation_mask_04 FS004V four_square_signed_orientation_mask_05 FS004W four_square_signed_orientation_mask_06 FS004X four_square_signed_orientation_mask_07 FS004Y four_square_signed_orientation_mask_08 FS004Z four_square_signed_orientation_mask_09 FS0050 four_square_signed_orientation_mask_10 FS0051 four_square_signed_orientation_mask_11 FS0052 four_square_signed_orientation_mask_12 FS0053 four_square_signed_orientation_mask_13 FS0054 four_square_signed_orientation_mask_14 FS0055 four_square_signed_orientation_mask_15

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

63 script commands · 7 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.

Named ingredients (2)
four square signed divisible norm product representationfour square signed absolute congruence divisible
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro r
  4. L4
    intro p0
  5. L5
    intro p1
  6. L6
    intro p2
  7. L7
    intro p3
  8. L8
    intro n0
  9. L9
    intro n1
  10. L10
    intro n2
02Fix variables and assumptionsL11–20

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

  1. L11
    intro n3
  2. L12
    intro m0
  3. L13
    intro m1
  4. L14
    intro m2
  5. L15
    intro m3
  6. L16
    intro hnonzero
  7. L17
    intro hnorm
  8. L18
    intro hmod0
  9. L19
    intro habs0
  10. L20
    intro hmod1
03Fix variables and assumptionsL21–25

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

  1. L21
    intro habs1
  2. L22
    intro hmod2
  3. L23
    intro habs2
  4. L24
    intro hmod3
  5. L25
    intro habs3
04Use earlier factsL26–35

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

  1. L26
    specialize four_square_signed_divisible_norm_product_representation p
  2. L27
    specialize four_square_signed_divisible_norm_product_representation k
  3. L28
    specialize four_square_signed_divisible_norm_product_representation r
  4. L29
    specialize four_square_signed_divisible_norm_product_representation m0
  5. L30
    specialize four_square_signed_divisible_norm_product_representation m1
  6. L31
    specialize four_square_signed_divisible_norm_product_representation m2
  7. L32
    specialize four_square_signed_divisible_norm_product_representation m3
  8. L33
    apply four_square_signed_divisible_norm_product_representation
  9. L34
    exact hnonzero
  10. L35
    exact hnorm
05Use earlier factsL36–45

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

  1. L36
    specialize four_square_signed_absolute_congruence_divisible k
  2. L37
    specialize four_square_signed_absolute_congruence_divisible p0
  3. L38
    specialize four_square_signed_absolute_congruence_divisible n0
  4. L39
    specialize four_square_signed_absolute_congruence_divisible m0
  5. L40
    apply four_square_signed_absolute_congruence_divisible
  6. L41
    exact hmod0
  7. L42
    exact habs0
  8. L43
    specialize four_square_signed_absolute_congruence_divisible k
  9. L44
    specialize four_square_signed_absolute_congruence_divisible p1
  10. L45
    specialize four_square_signed_absolute_congruence_divisible n1
06Use earlier factsL46–55

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

  1. L46
    specialize four_square_signed_absolute_congruence_divisible m1
  2. L47
    apply four_square_signed_absolute_congruence_divisible
  3. L48
    exact hmod1
  4. L49
    exact habs1
  5. L50
    specialize four_square_signed_absolute_congruence_divisible k
  6. L51
    specialize four_square_signed_absolute_congruence_divisible p2
  7. L52
    specialize four_square_signed_absolute_congruence_divisible n2
  8. L53
    specialize four_square_signed_absolute_congruence_divisible m2
  9. L54
    apply four_square_signed_absolute_congruence_divisible
  10. L55
    exact hmod2
07Use earlier factsL56–63

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

  1. L56
    exact habs2
  2. L57
    specialize four_square_signed_absolute_congruence_divisible k
  3. L58
    specialize four_square_signed_absolute_congruence_divisible p3
  4. L59
    specialize four_square_signed_absolute_congruence_divisible n3
  5. L60
    specialize four_square_signed_absolute_congruence_divisible m3
  6. L61
    apply four_square_signed_absolute_congruence_divisible
  7. L62
    exact hmod3
  8. L63
    exact habs3

Library-wide reading audit

Original defined command ledger · 63 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro r
  4. 0004intro p0
  5. 0005intro p1
  6. 0006intro p2
  7. 0007intro p3
  8. 0008intro n0
  9. 0009intro n1
  10. 0010intro n2
  11. 0011intro n3
  12. 0012intro m0
  13. 0013intro m1
  14. 0014intro m2
  15. 0015intro m3
  16. 0016intro hnonzero
  17. 0017intro hnorm
  18. 0018intro hmod0
  19. 0019intro habs0
  20. 0020intro hmod1
  21. 0021intro habs1
  22. 0022intro hmod2
  23. 0023intro habs2
  24. 0024intro hmod3
  25. 0025intro habs3
  26. 0026specialize four_square_signed_divisible_norm_product_representation p
  27. 0027specialize four_square_signed_divisible_norm_product_representation k
  28. 0028specialize four_square_signed_divisible_norm_product_representation r
  29. 0029specialize four_square_signed_divisible_norm_product_representation m0
  30. 0030specialize four_square_signed_divisible_norm_product_representation m1
  31. 0031specialize four_square_signed_divisible_norm_product_representation m2
  32. 0032specialize four_square_signed_divisible_norm_product_representation m3
  33. 0033apply four_square_signed_divisible_norm_product_representation
  34. 0034exact hnonzero
  35. 0035exact hnorm
  36. 0036specialize four_square_signed_absolute_congruence_divisible k
  37. 0037specialize four_square_signed_absolute_congruence_divisible p0
  38. 0038specialize four_square_signed_absolute_congruence_divisible n0
  39. 0039specialize four_square_signed_absolute_congruence_divisible m0
  40. 0040apply four_square_signed_absolute_congruence_divisible
  41. 0041exact hmod0
  42. 0042exact habs0
  43. 0043specialize four_square_signed_absolute_congruence_divisible k
  44. 0044specialize four_square_signed_absolute_congruence_divisible p1
  45. 0045specialize four_square_signed_absolute_congruence_divisible n1
  46. 0046specialize four_square_signed_absolute_congruence_divisible m1
  47. 0047apply four_square_signed_absolute_congruence_divisible
  48. 0048exact hmod1
  49. 0049exact habs1
  50. 0050specialize four_square_signed_absolute_congruence_divisible k
  51. 0051specialize four_square_signed_absolute_congruence_divisible p2
  52. 0052specialize four_square_signed_absolute_congruence_divisible n2
  53. 0053specialize four_square_signed_absolute_congruence_divisible m2
  54. 0054apply four_square_signed_absolute_congruence_divisible
  55. 0055exact hmod2
  56. 0056exact habs2
  57. 0057specialize four_square_signed_absolute_congruence_divisible k
  58. 0058specialize four_square_signed_absolute_congruence_divisible p3
  59. 0059specialize four_square_signed_absolute_congruence_divisible n3
  60. 0060specialize four_square_signed_absolute_congruence_divisible m3
  61. 0061apply four_square_signed_absolute_congruence_divisible
  62. 0062exact hmod3
  63. 0063exact habs3