FS002C

four_square_euler_all_mixed_cancel

Dependency-curried candidate body; not Alpha-enrolled; no checked-use authority

All twelve mixed Hamilton-coordinate products cancel in six separately witnessed coordinate-pair blocks.

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.

Exact expanded first-order arithmetic statement

forall a b c d e f g h. ((((((a * f) * (b * e) = (a * e) * (b * f))) /\ (((a * h) * (b * g) = (a * g) * (b * h))))) /\ ((((((a * f) * (c * h) = (a * h) * (c * f))) /\ (((a * g) * (c * e) = (a * e) * (c * g))))) /\ ((((((a * g) * (d * f) = (a * f) * (d * g))) /\ (((a * h) * (d * e) = (a * e) * (d * h))))) /\ ((((((b * f) * (c * g) = (b * g) * (c * f))) /\ (((b * e) * (c * h) = (b * h) * (c * e))))) /\ ((((((b * f) * (d * h) = (b * h) * (d * f))) /\ (((b * g) * (d * e) = (b * e) * (d * g))))) /\ (((((c * g) * (d * h) = (c * h) * (d * g))) /\ (((c * e) * (d * f) = (c * f) * (d * e))))))))))

Constructive proof overview

Generated structural guide

All twelve mixed Hamilton-coordinate products cancel in six separately witnessed coordinate-pair blocks.

The unchanged tactic script uses 6 declared prerequisites and contains 67 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

FS0026 four_square_euler_mixed_ab FS0027 four_square_euler_mixed_ac FS0028 four_square_euler_mixed_ad FS0029 four_square_euler_mixed_bc FS002A four_square_euler_mixed_bd FS002B four_square_euler_mixed_cd

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This dependency-curried candidate body does not grant checked theorem use or Stable membership.

Read the argument

Proof checkpoints

67 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.

Named ingredients (6)
four square euler mixed abfour square euler mixed acfour square euler mixed adfour square euler mixed bcfour square euler mixed bdfour square euler mixed cd
01Fix variables and assumptionsL1–8

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro f
  7. L7
    intro g
  8. L8
    intro h
02Separate the logical casesL9–9

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

  1. L9
    split
03Use earlier factsL10–18

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

  1. L10
    specialize four_square_euler_mixed_ab a
  2. L11
    specialize four_square_euler_mixed_ab b
  3. L12
    specialize four_square_euler_mixed_ab c
  4. L13
    specialize four_square_euler_mixed_ab d
  5. L14
    specialize four_square_euler_mixed_ab e
  6. L15
    specialize four_square_euler_mixed_ab f
  7. L16
    specialize four_square_euler_mixed_ab g
  8. L17
    specialize four_square_euler_mixed_ab h
  9. L18
    exact four_square_euler_mixed_ab
04Separate the logical casesL19–19

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

  1. L19
    split
05Use earlier factsL20–28

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

  1. L20
    specialize four_square_euler_mixed_ac a
  2. L21
    specialize four_square_euler_mixed_ac b
  3. L22
    specialize four_square_euler_mixed_ac c
  4. L23
    specialize four_square_euler_mixed_ac d
  5. L24
    specialize four_square_euler_mixed_ac e
  6. L25
    specialize four_square_euler_mixed_ac f
  7. L26
    specialize four_square_euler_mixed_ac g
  8. L27
    specialize four_square_euler_mixed_ac h
  9. L28
    exact four_square_euler_mixed_ac
06Separate the logical casesL29–29

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

  1. L29
    split
07Use earlier factsL30–38

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

  1. L30
    specialize four_square_euler_mixed_ad a
  2. L31
    specialize four_square_euler_mixed_ad b
  3. L32
    specialize four_square_euler_mixed_ad c
  4. L33
    specialize four_square_euler_mixed_ad d
  5. L34
    specialize four_square_euler_mixed_ad e
  6. L35
    specialize four_square_euler_mixed_ad f
  7. L36
    specialize four_square_euler_mixed_ad g
  8. L37
    specialize four_square_euler_mixed_ad h
  9. L38
    exact four_square_euler_mixed_ad
08Separate the logical casesL39–39

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

  1. L39
    split
09Use earlier factsL40–48

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

  1. L40
    specialize four_square_euler_mixed_bc a
  2. L41
    specialize four_square_euler_mixed_bc b
  3. L42
    specialize four_square_euler_mixed_bc c
  4. L43
    specialize four_square_euler_mixed_bc d
  5. L44
    specialize four_square_euler_mixed_bc e
  6. L45
    specialize four_square_euler_mixed_bc f
  7. L46
    specialize four_square_euler_mixed_bc g
  8. L47
    specialize four_square_euler_mixed_bc h
  9. L48
    exact four_square_euler_mixed_bc
10Separate the logical casesL49–49

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

  1. L49
    split
11Use earlier factsL50–59

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

  1. L50
    specialize four_square_euler_mixed_bd a
  2. L51
    specialize four_square_euler_mixed_bd b
  3. L52
    specialize four_square_euler_mixed_bd c
  4. L53
    specialize four_square_euler_mixed_bd d
  5. L54
    specialize four_square_euler_mixed_bd e
  6. L55
    specialize four_square_euler_mixed_bd f
  7. L56
    specialize four_square_euler_mixed_bd g
  8. L57
    specialize four_square_euler_mixed_bd h
  9. L58
    exact four_square_euler_mixed_bd
  10. L59
    specialize four_square_euler_mixed_cd a
12Use earlier factsL60–67

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

  1. L60
    specialize four_square_euler_mixed_cd b
  2. L61
    specialize four_square_euler_mixed_cd c
  3. L62
    specialize four_square_euler_mixed_cd d
  4. L63
    specialize four_square_euler_mixed_cd e
  5. L64
    specialize four_square_euler_mixed_cd f
  6. L65
    specialize four_square_euler_mixed_cd g
  7. L66
    specialize four_square_euler_mixed_cd h
  8. L67
    exact four_square_euler_mixed_cd

Library-wide reading audit

Original exact command ledger · 67 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro f
  7. 0007intro g
  8. 0008intro h
  9. 0009split
  10. 0010specialize four_square_euler_mixed_ab a
  11. 0011specialize four_square_euler_mixed_ab b
  12. 0012specialize four_square_euler_mixed_ab c
  13. 0013specialize four_square_euler_mixed_ab d
  14. 0014specialize four_square_euler_mixed_ab e
  15. 0015specialize four_square_euler_mixed_ab f
  16. 0016specialize four_square_euler_mixed_ab g
  17. 0017specialize four_square_euler_mixed_ab h
  18. 0018exact four_square_euler_mixed_ab
  19. 0019split
  20. 0020specialize four_square_euler_mixed_ac a
  21. 0021specialize four_square_euler_mixed_ac b
  22. 0022specialize four_square_euler_mixed_ac c
  23. 0023specialize four_square_euler_mixed_ac d
  24. 0024specialize four_square_euler_mixed_ac e
  25. 0025specialize four_square_euler_mixed_ac f
  26. 0026specialize four_square_euler_mixed_ac g
  27. 0027specialize four_square_euler_mixed_ac h
  28. 0028exact four_square_euler_mixed_ac
  29. 0029split
  30. 0030specialize four_square_euler_mixed_ad a
  31. 0031specialize four_square_euler_mixed_ad b
  32. 0032specialize four_square_euler_mixed_ad c
  33. 0033specialize four_square_euler_mixed_ad d
  34. 0034specialize four_square_euler_mixed_ad e
  35. 0035specialize four_square_euler_mixed_ad f
  36. 0036specialize four_square_euler_mixed_ad g
  37. 0037specialize four_square_euler_mixed_ad h
  38. 0038exact four_square_euler_mixed_ad
  39. 0039split
  40. 0040specialize four_square_euler_mixed_bc a
  41. 0041specialize four_square_euler_mixed_bc b
  42. 0042specialize four_square_euler_mixed_bc c
  43. 0043specialize four_square_euler_mixed_bc d
  44. 0044specialize four_square_euler_mixed_bc e
  45. 0045specialize four_square_euler_mixed_bc f
  46. 0046specialize four_square_euler_mixed_bc g
  47. 0047specialize four_square_euler_mixed_bc h
  48. 0048exact four_square_euler_mixed_bc
  49. 0049split
  50. 0050specialize four_square_euler_mixed_bd a
  51. 0051specialize four_square_euler_mixed_bd b
  52. 0052specialize four_square_euler_mixed_bd c
  53. 0053specialize four_square_euler_mixed_bd d
  54. 0054specialize four_square_euler_mixed_bd e
  55. 0055specialize four_square_euler_mixed_bd f
  56. 0056specialize four_square_euler_mixed_bd g
  57. 0057specialize four_square_euler_mixed_bd h
  58. 0058exact four_square_euler_mixed_bd
  59. 0059specialize four_square_euler_mixed_cd a
  60. 0060specialize four_square_euler_mixed_cd b
  61. 0061specialize four_square_euler_mixed_cd c
  62. 0062specialize four_square_euler_mixed_cd d
  63. 0063specialize four_square_euler_mixed_cd e
  64. 0064specialize four_square_euler_mixed_cd f
  65. 0065specialize four_square_euler_mixed_cd g
  66. 0066specialize four_square_euler_mixed_cd h
  67. 0067exact four_square_euler_mixed_cd