TS001W · theorem body

brahmagupta_fibonacci_two_square_identity

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

Brahmagupta–Fibonacci: the product of two witnessed norms is the norm of ac+bd and the natural magnitude of ad−bc.

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

forall a b c d m. (((a * d) = (b * c) + (m) \/ (b * c) = (a * d) + (m))) -> (a * a + b * b) * (c * c + d * d) = (a * c + b * d) * (a * c + b * d) + m * m

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

none

In local proof propositions

none
Exact expanded first-order statement
forall a b c d m. (((a * d) = (b * c) + (m) \/ (b * c) = (a * d) + (m))) -> (a * a + b * b) * (c * c + d * d) = (a * c + b * d) * (a * c + b * d) + m * m

Proof neighborhood

Direct theorem prerequisites

TS001U two_square_product_norm_blocks TS001R two_square_absolute_difference_square_balance TS001V two_square_sum_square_blocks TS001S two_square_cross_product_interchange add_comm · Stable closed add_assoc · Stable closed

Direct theorem dependents

TS001X two_square_representation_multiplicatively_closed

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

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

Named ingredients (4)
two square product norm blockstwo square absolute difference square balancetwo square sum square blockstwo square cross product interchange
01Fix variables and assumptionsL1–6

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 m
  6. L6
    intro hdifference
02Establish hgapL7–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply two square absolute difference square balance.

  1. L7
    have hgap : m * m + ((a * d) * (b * c) + (a * d) * (b * c)) = (a * d) * (a * d) + (b * c) * (b * c)
  2. L8
    specialize two_square_absolute_difference_square_balance (a * d)
  3. L9
    specialize two_square_absolute_difference_square_balance (b * c)
  4. L10
    specialize two_square_absolute_difference_square_balance m
  5. L11
    apply two_square_absolute_difference_square_balance
  6. L12
    exact hdifference
03Establish hcrossL13–18

Establish this local claim before using it. It is not an additional assumption.

  1. L13
    have hcross : (a * c) * (b * d) = (a * d) * (b * c)
  2. L14
    specialize two_square_cross_product_interchange a
  3. L15
    specialize two_square_cross_product_interchange b
  4. L16
    specialize two_square_cross_product_interchange c
  5. L17
    specialize two_square_cross_product_interchange d
  6. L18
    exact two_square_cross_product_interchange
04Establish hsquareL19–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply two square product norm blocks.

  1. L19
    have hsquare : (a * c + b * d) * (a * c + b * d) = ((a * c) * (a * c) + (b * d) * (b * d)) + ((a * c) * (b * d) + (a * c) * (b * d))
  2. L20
    specialize two_square_sum_square_blocks (a * c)
  3. L21
    specialize two_square_sum_square_blocks (b * d)
  4. L22
    exact two_square_sum_square_blocks
  5. L23
    rewrite hcross at hsquare
  6. L24
    rewrite hcross at hsquare
  7. L25
    trans ((a * c) * (a * c) + (b * d) * (b * d)) + ((a * d) * (a * d) + (b * c) * (b * c))
  8. L26
    apply two_square_product_norm_blocks
  9. L27
    rewrite <- hgap
  10. L28
    rewrite hsquare
05Calculate and transport equalitiesL29–31

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

  1. L29
    trans ((a * c) * (a * c) + (b * d) * (b * d)) + (((a * d) * (b * c) + (a * d) * (b * c)) + m * m)
  2. L30
    congr
  3. L31
    refl
06Use earlier factsL32–32

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

  1. L32
    apply add_comm
07Calculate and transport equalitiesL33–33

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

  1. L33
    symm
08Use earlier factsL34–34

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

  1. L34
    apply add_assoc

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro m
  6. 0006intro hdifference
  7. 0007have hgap : m * m + ((a * d) * (b * c) + (a * d) * (b * c)) = (a * d) * (a * d) + (b * c) * (b * c)
  8. 0008specialize two_square_absolute_difference_square_balance (a * d)
  9. 0009specialize two_square_absolute_difference_square_balance (b * c)
  10. 0010specialize two_square_absolute_difference_square_balance m
  11. 0011apply two_square_absolute_difference_square_balance
  12. 0012exact hdifference
  13. 0013have hcross : (a * c) * (b * d) = (a * d) * (b * c)
  14. 0014specialize two_square_cross_product_interchange a
  15. 0015specialize two_square_cross_product_interchange b
  16. 0016specialize two_square_cross_product_interchange c
  17. 0017specialize two_square_cross_product_interchange d
  18. 0018exact two_square_cross_product_interchange
  19. 0019have hsquare : (a * c + b * d) * (a * c + b * d) = ((a * c) * (a * c) + (b * d) * (b * d)) + ((a * c) * (b * d) + (a * c) * (b * d))
  20. 0020specialize two_square_sum_square_blocks (a * c)
  21. 0021specialize two_square_sum_square_blocks (b * d)
  22. 0022exact two_square_sum_square_blocks
  23. 0023rewrite hcross at hsquare
  24. 0024rewrite hcross at hsquare
  25. 0025trans ((a * c) * (a * c) + (b * d) * (b * d)) + ((a * d) * (a * d) + (b * c) * (b * c))
  26. 0026apply two_square_product_norm_blocks
  27. 0027rewrite <- hgap
  28. 0028rewrite hsquare
  29. 0029trans ((a * c) * (a * c) + (b * d) * (b * d)) + (((a * d) * (b * c) + (a * d) * (b * c)) + m * m)
  30. 0030congr
  31. 0031refl
  32. 0032apply add_comm
  33. 0033symm
  34. 0034apply add_assoc