TS001X · theorem body

two_square_representation_multiplicatively_closed

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

Two explicit natural two-square representations compose into an explicit representation of their product.

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 u v. (exists ftsc_first_product_left ftsc_second_product_left. (u) = ftsc_first_product_left * ftsc_first_product_left + ftsc_second_product_left * ftsc_second_product_left) -> (exists ftsc_first_product_right ftsc_second_product_right. (v) = ftsc_first_product_right * ftsc_first_product_right + ftsc_second_product_right * ftsc_second_product_right) -> (exists ftsc_first_product_result ftsc_second_product_result. (u * v) = ftsc_first_product_result * ftsc_first_product_result + ftsc_second_product_result * ftsc_second_product_result)

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 u v. (exists ftsc_first_product_left ftsc_second_product_left. (u) = ftsc_first_product_left * ftsc_first_product_left + ftsc_second_product_left * ftsc_second_product_left) -> (exists ftsc_first_product_right ftsc_second_product_right. (v) = ftsc_first_product_right * ftsc_first_product_right + ftsc_second_product_right * ftsc_second_product_right) -> (exists ftsc_first_product_result ftsc_second_product_result. (u * v) = ftsc_first_product_result * ftsc_first_product_result + ftsc_second_product_result * ftsc_second_product_result)

Proof neighborhood

Direct theorem prerequisites

TS001A natural_absolute_difference_exists TS001W brahmagupta_fibonacci_two_square_identity

Direct theorem dependents

TS002M beta_two_square_represented_factor_product TS002R represented_factor_product_times_square_is_two_square TS003C all_bad_prime_even_two_square_sufficiency_bounded TS003M two_square_representation_preserved_by_square_factor

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

24 script commands · 7 reading checkpoints · 1 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)
natural absolute difference existsbrahmagupta fibonacci two square identity
01Fix variables and assumptionsL1–4

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

  1. L1
    intro u
  2. L2
    intro v
  3. L3
    intro hleft
  4. L4
    intro hright
02Separate the logical casesL5–8

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

  1. L5
    cases hleft
  2. L6
    cases hleft_witness
  3. L7
    cases hright
  4. L8
    cases hright_witness
03Establish hdifferenceL9–12

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

  1. L9
    have hdifference : exists m. (x * x3 = x1 * x2 + m \/ x1 * x2 = x * x3 + m)
  2. L10
    specialize natural_absolute_difference_exists (x * x3)
  3. L11
    specialize natural_absolute_difference_exists (x1 * x2)
  4. L12
    exact natural_absolute_difference_exists
04Separate the logical casesL13–13

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

  1. L13
    cases hdifference
05Construct an explicit witnessL14–15

Supply the displayed value, then prove that it has the required property.

  1. L14
    exists x * x2 + x1 * x3
  2. L15
    exists x4
06Calculate and transport equalitiesL16–17

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

  1. L16
    rewrite hleft_witness_witness
  2. L17
    rewrite hright_witness_witness
07Use earlier factsL18–24

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

  1. L18
    specialize brahmagupta_fibonacci_two_square_identity x
  2. L19
    specialize brahmagupta_fibonacci_two_square_identity x1
  3. L20
    specialize brahmagupta_fibonacci_two_square_identity x2
  4. L21
    specialize brahmagupta_fibonacci_two_square_identity x3
  5. L22
    specialize brahmagupta_fibonacci_two_square_identity x4
  6. L23
    apply brahmagupta_fibonacci_two_square_identity
  7. L24
    exact hdifference_witness

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro u
  2. 0002intro v
  3. 0003intro hleft
  4. 0004intro hright
  5. 0005cases hleft
  6. 0006cases hleft_witness
  7. 0007cases hright
  8. 0008cases hright_witness
  9. 0009have hdifference : exists m. (x * x3 = x1 * x2 + m \/ x1 * x2 = x * x3 + m)
  10. 0010specialize natural_absolute_difference_exists (x * x3)
  11. 0011specialize natural_absolute_difference_exists (x1 * x2)
  12. 0012exact natural_absolute_difference_exists
  13. 0013cases hdifference
  14. 0014exists x * x2 + x1 * x3
  15. 0015exists x4
  16. 0016rewrite hleft_witness_witness
  17. 0017rewrite hright_witness_witness
  18. 0018specialize brahmagupta_fibonacci_two_square_identity x
  19. 0019specialize brahmagupta_fibonacci_two_square_identity x1
  20. 0020specialize brahmagupta_fibonacci_two_square_identity x2
  21. 0021specialize brahmagupta_fibonacci_two_square_identity x3
  22. 0022specialize brahmagupta_fibonacci_two_square_identity x4
  23. 0023apply brahmagupta_fibonacci_two_square_identity
  24. 0024exact hdifference_witness