SL000O · theorem body

quadratic_supplement_two_conditional_on_gauss_count_shape

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

The exact second supplementary law follows constructively once the existing Gauss reflection count is identified with the explicit doubling-count shape.

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. ∀ h. ∀ e. p = 2 · h + 1 → Prime(p) → h = 2 · e ∨ (∃ x. h = 2 · x + 1 ∧ e = S x) → (QRes(p,2) → Even(e)) ∧ (Even(e) → QRes(p,2)) ∧ ((¬QRes(p,2) → Odd(e)) ∧ (Odd(e) → ¬QRes(p,2))) → (QRes(p,2) → (∃ x. p = 8 · x + 1) ∨ (∃ x. p = 8 · x + 7)) ∧ ((∃ x. p = 8 · x + 1) ∨ (∃ x. p = 8 · x + 7) → QRes(p,2)) ∧ ((¬QRes(p,2) → (∃ x. p = 8 · x + 3) ∨ (∃ x. p = 8 · x + 5)) ∧ ((∃ x. p = 8 · x + 3) ∨ (∃ x. p = 8 · x + 5) → ¬QRes(p,2)))

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

PD0004 Prime PD0009 Even PD0010 Odd PD0021 QRes

In local proof propositions

PD0009 Even PD0010 Odd
Exact expanded first-order statement
forall p h e. p = 2 * h + 1 -> ((~(p = 1) /\ forall frm_prime_left_qst_prime frm_prime_right_qst_prime. p = frm_prime_left_qst_prime * frm_prime_right_qst_prime -> frm_prime_left_qst_prime = 1 \/ frm_prime_right_qst_prime = 1)) -> (((h = 2 * e) \/ (exists qst_count_half_shape. h = 2 * qst_count_half_shape + 1 /\ e = S qst_count_half_shape))) -> ((((((exists qst_root_two. exists qst_mod_left_two qst_mod_right_two. qst_root_two * qst_root_two + p * qst_mod_left_two = 2 + p * qst_mod_right_two) -> (exists qst_even_count. e = 2 * qst_even_count)) /\ ((exists qst_even_count. e = 2 * qst_even_count) -> (exists qst_root_two. exists qst_mod_left_two qst_mod_right_two. qst_root_two * qst_root_two + p * qst_mod_left_two = 2 + p * qst_mod_right_two)))) /\ ((((~(exists qst_root_two. exists qst_mod_left_two qst_mod_right_two. qst_root_two * qst_root_two + p * qst_mod_left_two = 2 + p * qst_mod_right_two)) -> (exists qst_odd_count. e = 2 * qst_odd_count + 1)) /\ ((exists qst_odd_count. e = 2 * qst_odd_count + 1) -> (~(exists qst_root_two. exists qst_mod_left_two qst_mod_right_two. qst_root_two * qst_root_two + p * qst_mod_left_two = 2 + p * qst_mod_right_two))))))) -> ((((((exists qst_root_two. exists qst_mod_left_two qst_mod_right_two. qst_root_two * qst_root_two + p * qst_mod_left_two = 2 + p * qst_mod_right_two) -> (((exists qst_mod_eight_modulus_one. p = 8 * qst_mod_eight_modulus_one + 1) \/ (exists qst_mod_eight_modulus_seven. p = 8 * qst_mod_eight_modulus_seven + 7)))) /\ ((((exists qst_mod_eight_modulus_one. p = 8 * qst_mod_eight_modulus_one + 1) \/ (exists qst_mod_eight_modulus_seven. p = 8 * qst_mod_eight_modulus_seven + 7))) -> (exists qst_root_two. exists qst_mod_left_two qst_mod_right_two. qst_root_two * qst_root_two + p * qst_mod_left_two = 2 + p * qst_mod_right_two)))) /\ ((((~(exists qst_root_two. exists qst_mod_left_two qst_mod_right_two. qst_root_two * qst_root_two + p * qst_mod_left_two = 2 + p * qst_mod_right_two)) -> (((exists qst_mod_eight_modulus_three. p = 8 * qst_mod_eight_modulus_three + 3) \/ (exists qst_mod_eight_modulus_five. p = 8 * qst_mod_eight_modulus_five + 5)))) /\ ((((exists qst_mod_eight_modulus_three. p = 8 * qst_mod_eight_modulus_three + 3) \/ (exists qst_mod_eight_modulus_five. p = 8 * qst_mod_eight_modulus_five + 5))) -> (~(exists qst_root_two. exists qst_mod_left_two qst_mod_right_two. qst_root_two * qst_root_two + p * qst_mod_left_two = 2 + p * qst_mod_right_two)))))))

Proof neighborhood

Direct theorem prerequisites

SL000F doubling_gauss_count_parity_mod_eight_complete

Direct theorem dependents

SL000Q quadratic_supplement_two_half_complete

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

41 script commands · 12 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 (1)
doubling gauss count parity mod eight complete
01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro e
  4. L4
    intro hpodd
  5. L5
    intro hprime
  6. L6
    intro hshape
  7. L7
    intro hgauss
02Establish hparityL8–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply doubling gauss count parity mod eight complete.

  1. L8
    have hparity : (Even(e) → (∃ x. p = 8 · x + 1) ∨ (∃ x. p = 8 · x + 7)) ∧ ((∃ x. p = 8 · x + 1) ∨ (∃ x. p = 8 · x + 7) → Even(e)) ∧ ((Odd(e) → (∃ x. p = 8 · x + 3) ∨ (∃ x. p = 8 · x + 5)) ∧ ((∃ x. p = 8 · x + 3) ∨ (∃ x. p = 8 · x + 5) → Odd(e)))Definitions: Even(e)Odd(e)Original native command in the exact edition
  2. L9
    specialize doubling_gauss_count_parity_mod_eight_complete p
  3. L10
    specialize doubling_gauss_count_parity_mod_eight_complete h
  4. L11
    specialize doubling_gauss_count_parity_mod_eight_complete e
  5. L12
    apply doubling_gauss_count_parity_mod_eight_complete
  6. L13
    exact hpodd
  7. L14
    exact hshape
03Separate the logical casesL15–22

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

  1. L15
    cases hgauss
  2. L16
    cases hgauss_left
  3. L17
    cases hgauss_right
  4. L18
    cases hparity
  5. L19
    cases hparity_left
  6. L20
    cases hparity_right
  7. L21
    split
  8. L22
    split
04Fix variables and assumptionsL23–23

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

  1. L23
    intro hresidue
05Use earlier factsL24–26

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

  1. L24
    apply hparity_left_left
  2. L25
    apply hgauss_left_left
  3. L26
    exact hresidue
06Fix variables and assumptionsL27–27

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

  1. L27
    intro hgood
07Use earlier factsL28–30

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

  1. L28
    apply hgauss_left_right
  2. L29
    apply hparity_left_right
  3. L30
    exact hgood
08Separate the logical casesL31–31

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

  1. L31
    split
09Fix variables and assumptionsL32–32

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

  1. L32
    intro hnonresidue
10Use earlier factsL33–35

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

  1. L33
    apply hparity_right_left
  2. L34
    apply hgauss_right_left
  3. L35
    exact hnonresidue
11Fix variables and assumptionsL36–37

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

  1. L36
    intro hbad
  2. L37
    intro hresidue
12Use earlier factsL38–41

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

  1. L38
    apply hgauss_right_right
  2. L39
    apply hparity_right_right
  3. L40
    exact hbad
  4. L41
    exact hresidue

Library-wide reading audit

Original defined command ledger · 41 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro e
  4. 0004intro hpodd
  5. 0005intro hprime
  6. 0006intro hshape
  7. 0007intro hgauss
  8. 0008have hparity : (Even(e) → (∃ x. p = 8 · x + 1) ∨ (∃ x. p = 8 · x + 7)) ∧ ((∃ x. p = 8 · x + 1) ∨ (∃ x. p = 8 · x + 7) → Even(e)) ∧ ((Odd(e) → (∃ x. p = 8 · x + 3) ∨ (∃ x. p = 8 · x + 5)) ∧ ((∃ x. p = 8 · x + 3) ∨ (∃ x. p = 8 · x + 5) → Odd(e)))
    Exact native replay linehave hparity : (((((exists qst_even_count. e = 2 * qst_even_count) -> (((exists qst_mod_eight_modulus_one. p = 8 * qst_mod_eight_modulus_one + 1) \/ (exists qst_mod_eight_modulus_seven. p = 8 * qst_mod_eight_modulus_seven + 7)))) /\ ((((exists qst_mod_eight_modulus_one. p = 8 * qst_mod_eight_modulus_one + 1) \/ (exists qst_mod_eight_modulus_seven. p = 8 * qst_mod_eight_modulus_seven + 7))) -> (exists qst_even_count. e = 2 * qst_even_count)))) /\ ((((exists qst_odd_count. e = 2 * qst_odd_count + 1) -> (((exists qst_mod_eight_modulus_three. p = 8 * qst_mod_eight_modulus_three + 3) \/ (exists qst_mod_eight_modulus_five. p = 8 * qst_mod_eight_modulus_five + 5)))) /\ ((((exists qst_mod_eight_modulus_three. p = 8 * qst_mod_eight_modulus_three + 3) \/ (exists qst_mod_eight_modulus_five. p = 8 * qst_mod_eight_modulus_five + 5))) -> (exists qst_odd_count. e = 2 * qst_odd_count + 1)))))
  9. 0009specialize doubling_gauss_count_parity_mod_eight_complete p
  10. 0010specialize doubling_gauss_count_parity_mod_eight_complete h
  11. 0011specialize doubling_gauss_count_parity_mod_eight_complete e
  12. 0012apply doubling_gauss_count_parity_mod_eight_complete
  13. 0013exact hpodd
  14. 0014exact hshape
  15. 0015cases hgauss
  16. 0016cases hgauss_left
  17. 0017cases hgauss_right
  18. 0018cases hparity
  19. 0019cases hparity_left
  20. 0020cases hparity_right
  21. 0021split
  22. 0022split
  23. 0023intro hresidue
  24. 0024apply hparity_left_left
  25. 0025apply hgauss_left_left
  26. 0026exact hresidue
  27. 0027intro hgood
  28. 0028apply hgauss_left_right
  29. 0029apply hparity_left_right
  30. 0030exact hgood
  31. 0031split
  32. 0032intro hnonresidue
  33. 0033apply hparity_right_left
  34. 0034apply hgauss_right_left
  35. 0035exact hnonresidue
  36. 0036intro hbad
  37. 0037intro hresidue
  38. 0038apply hgauss_right_right
  39. 0039apply hparity_right_right
  40. 0040exact hbad
  41. 0041exact hresidue