PA00CO

odd_signed_division_congruence_mod_two

Alpha v34 checked-use theorem · independently closed; not Stable

Exact signed division data gives the Gauss--Eisenstein modulo-two relation.

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 PA statement

forall p h a x n q r m s. p = 2 * h + 1 -> (exists sdp_odd_gep_scale. a = 2 * sdp_odd_gep_scale + 1) -> n = a * x -> n = p * q + r -> (exists gsp_lt_gap_gep_r_below. gsp_lt_gap_gep_r_below + S r = p) -> (exists gsp_lt_gap_gep_m_positive. gsp_lt_gap_gep_m_positive + S 0 = m) -> (exists gsp_le_gap_gep_m_bounded. gsp_le_gap_gep_m_bounded + m = h) -> (((s = 0 /\ (exists wpp_mod_left_gep_n_mod_m wpp_mod_right_gep_n_mod_m. (n) + p * wpp_mod_left_gep_n_mod_m = (m) + p * wpp_mod_right_gep_n_mod_m)) \/ (s = 1 /\ (exists wpp_mod_left_gep_n_mod_reflected wpp_mod_right_gep_n_mod_reflected. (n) + p * wpp_mod_left_gep_n_mod_reflected = ((2 * h) * m) + p * wpp_mod_right_gep_n_mod_reflected)))) -> (exists sdp_u_gep_generic_result sdp_v_gep_generic_result. (x) + 2 * sdp_u_gep_generic_result = (q + m + s) + 2 * sdp_v_gep_generic_result)

Structural proof guide

Generated structural guide

Exact signed division data gives the Gauss--Eisenstein modulo-two relation.

Use the direct prerequisites odd_signed_division_branch_exact, odd_scaled_division_signed_mod_two as previously established PA formulas.

The proof proceeds by intermediate claims (2).

Referenced ingredients

PA00C6 odd_signed_division_branch_exact PA00CN odd_scaled_division_signed_mod_two

Proof neighborhood

Direct dependencies

PA00C6 odd_signed_division_branch_exact PA00CN odd_scaled_division_signed_mod_two

Direct dependents

PA00CP gauss_eisenstein_prefix_pointwise_mod_two

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

50 script commands · 10 reading checkpoints · 2 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)
odd signed division branch exactodd scaled division signed mod two
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro a
  4. L4
    intro x
  5. L5
    intro n
  6. L6
    intro q
  7. L7
    intro r
  8. L8
    intro m
  9. L9
    intro s
  10. L10
    intro hp
02Fix variables and assumptionsL11–17

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

  1. L11
    intro ha
  2. L12
    intro hnscale
  3. L13
    intro hdivision
  4. L14
    intro hrbelow
  5. L15
    intro hmpositive
  6. L16
    intro hmbounded
  7. L17
    intro hsigned
03Establish hexactL18–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd signed division branch exact.

  1. L18
    have hexact : ((s = 0 /\ r = m) \/ (s = 1 /\ r + m = p))
  2. L19
    specialize odd_signed_division_branch_exact p
  3. L20
    specialize odd_signed_division_branch_exact h
  4. L21
    specialize odd_signed_division_branch_exact n
  5. L22
    specialize odd_signed_division_branch_exact q
  6. L23
    specialize odd_signed_division_branch_exact r
  7. L24
    specialize odd_signed_division_branch_exact m
  8. L25
    specialize odd_signed_division_branch_exact s
  9. L26
    apply odd_signed_division_branch_exact
  10. L27
    exact hp
04Use earlier factsL28–32

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

  1. L28
    exact hdivision
  2. L29
    exact hrbelow
  3. L30
    exact hmpositive
  4. L31
    exact hmbounded
  5. L32
    exact hsigned
05Establish hpoddL33–33

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

  1. L33
    have hpodd : exists sdp_odd_gep_modulus. p = 2 * sdp_odd_gep_modulus + 1
06Construct an explicit witnessL34–34

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

  1. L34
    exists h
07Use earlier factsL35–44

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

  1. L35
    exact hp
  2. L36
    specialize odd_scaled_division_signed_mod_two p
  3. L37
    specialize odd_scaled_division_signed_mod_two a
  4. L38
    specialize odd_scaled_division_signed_mod_two x
  5. L39
    specialize odd_scaled_division_signed_mod_two q
  6. L40
    specialize odd_scaled_division_signed_mod_two r
  7. L41
    specialize odd_scaled_division_signed_mod_two m
  8. L42
    specialize odd_scaled_division_signed_mod_two s
  9. L43
    apply odd_scaled_division_signed_mod_two
  10. L44
    exact hpodd
08Use earlier factsL45–45

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

  1. L45
    exact ha
09Calculate and transport equalitiesL46–47

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

  1. L46
    trans n
  2. L47
    symm
10Use earlier factsL48–50

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

  1. L48
    exact hnscale
  2. L49
    exact hdivision
  3. L50
    exact hexact

Library-wide reading audit

Original exact command ledger · 50 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro x
  5. 0005intro n
  6. 0006intro q
  7. 0007intro r
  8. 0008intro m
  9. 0009intro s
  10. 0010intro hp
  11. 0011intro ha
  12. 0012intro hnscale
  13. 0013intro hdivision
  14. 0014intro hrbelow
  15. 0015intro hmpositive
  16. 0016intro hmbounded
  17. 0017intro hsigned
  18. 0018have hexact : ((s = 0 /\ r = m) \/ (s = 1 /\ r + m = p))
  19. 0019specialize odd_signed_division_branch_exact p
  20. 0020specialize odd_signed_division_branch_exact h
  21. 0021specialize odd_signed_division_branch_exact n
  22. 0022specialize odd_signed_division_branch_exact q
  23. 0023specialize odd_signed_division_branch_exact r
  24. 0024specialize odd_signed_division_branch_exact m
  25. 0025specialize odd_signed_division_branch_exact s
  26. 0026apply odd_signed_division_branch_exact
  27. 0027exact hp
  28. 0028exact hdivision
  29. 0029exact hrbelow
  30. 0030exact hmpositive
  31. 0031exact hmbounded
  32. 0032exact hsigned
  33. 0033have hpodd : exists sdp_odd_gep_modulus. p = 2 * sdp_odd_gep_modulus + 1
  34. 0034exists h
  35. 0035exact hp
  36. 0036specialize odd_scaled_division_signed_mod_two p
  37. 0037specialize odd_scaled_division_signed_mod_two a
  38. 0038specialize odd_scaled_division_signed_mod_two x
  39. 0039specialize odd_scaled_division_signed_mod_two q
  40. 0040specialize odd_scaled_division_signed_mod_two r
  41. 0041specialize odd_scaled_division_signed_mod_two m
  42. 0042specialize odd_scaled_division_signed_mod_two s
  43. 0043apply odd_scaled_division_signed_mod_two
  44. 0044exact hpodd
  45. 0045exact ha
  46. 0046trans n
  47. 0047symm
  48. 0048exact hnscale
  49. 0049exact hdivision
  50. 0050exact hexact