TS001X

two_square_representation_multiplicatively_closed

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

Exact expanded first-order arithmetic 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)

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 24 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

TS001A natural_absolute_difference_exists TS001W brahmagupta_fibonacci_two_square_identity

Direct 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

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 exact 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