PA00CN · theorem

odd_scaled_division_signed_mod_two

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

The generic Gauss-Eisenstein pointwise join: x == q+m+s modulo two.

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. ∀ a. ∀ x. ∀ q. ∀ r. ∀ m. ∀ s. Odd(p) → Odd(a) → a · x = p · q + r → s = 0 ∧ r = m ∨ s = 1 ∧ r + m = p → ModEq(2,x,q + m + s)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0008 ModEq PD0010 Odd

3 occurrences

In local proof propositions

PD0008 ModEq

2 occurrences

Exact expanded native-PA statement
forall p a x q r m s. (exists sdp_odd_prime_like_modulus. p = 2 * sdp_odd_prime_like_modulus + 1) -> (exists sdp_odd_scale. a = 2 * sdp_odd_scale + 1) -> a * x = p * q + r -> (((s = 0 /\ r = m) \/ (s = 1 /\ r + m = p))) -> (exists sdp_u_signed_final_result sdp_v_signed_final_result. (x) + 2 * sdp_u_signed_final_result = (q + m + s) + 2 * sdp_v_signed_final_result)

Proof neighborhood

Direct theorem prerequisites

PA00CK odd_product_division_mod_two PA00CM signed_remainder_sum_mod_two PA0024 mod_eq_trans

Direct theorem dependents

PA00CO odd_signed_division_congruence_mod_two

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

37 script commands · 5 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.

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 (3)
odd product division mod twosigned remainder sum mod twomod eq trans
01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro hbranch
03Establish hxqrL12–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd product division mod two.

  1. L12
    have hxqr : ModEq(2,x,q + r)Definitions: ModEq(2,x,q + r)Original native command in the exact edition
  2. L13
    specialize odd_product_division_mod_two p
  3. L14
    specialize odd_product_division_mod_two a
  4. L15
    specialize odd_product_division_mod_two x
  5. L16
    specialize odd_product_division_mod_two q
  6. L17
    specialize odd_product_division_mod_two r
  7. L18
    apply odd_product_division_mod_two
  8. L19
    exact hp
  9. L20
    exact ha
  10. L21
    exact hdivision
04Establish hqrsignedL22–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed remainder sum mod two.

  1. L22
    have hqrsigned : ModEq(2,q + r,q + m + s)Definitions: ModEq(2,q + r,q + m + s)Original native command in the exact edition
  2. L23
    specialize signed_remainder_sum_mod_two p
  3. L24
    specialize signed_remainder_sum_mod_two q
  4. L25
    specialize signed_remainder_sum_mod_two r
  5. L26
    specialize signed_remainder_sum_mod_two m
  6. L27
    specialize signed_remainder_sum_mod_two s
  7. L28
    apply signed_remainder_sum_mod_two
  8. L29
    exact hp
  9. L30
    exact hbranch
  10. L31
    specialize mod_eq_trans 2
05Use earlier factsL32–37

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

  1. L32
    specialize mod_eq_trans x
  2. L33
    specialize mod_eq_trans (q + r)
  3. L34
    specialize mod_eq_trans (q + m + s)
  4. L35
    apply mod_eq_trans
  5. L36
    exact hxqr
  6. L37
    exact hqrsigned

Library-wide reading audit

Original defined command ledger · 37 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro x
  4. 0004intro q
  5. 0005intro r
  6. 0006intro m
  7. 0007intro s
  8. 0008intro hp
  9. 0009intro ha
  10. 0010intro hdivision
  11. 0011intro hbranch
  12. 0012have hxqr : ModEq(2,x,q + r)
    Exact native replay linehave hxqr : exists sdp_u_proof_final_x_qr sdp_v_proof_final_x_qr. (x) + 2 * sdp_u_proof_final_x_qr = (q + r) + 2 * sdp_v_proof_final_x_qr
  13. 0013specialize odd_product_division_mod_two p
  14. 0014specialize odd_product_division_mod_two a
  15. 0015specialize odd_product_division_mod_two x
  16. 0016specialize odd_product_division_mod_two q
  17. 0017specialize odd_product_division_mod_two r
  18. 0018apply odd_product_division_mod_two
  19. 0019exact hp
  20. 0020exact ha
  21. 0021exact hdivision
  22. 0022have hqrsigned : ModEq(2,q + r,q + m + s)
    Exact native replay linehave hqrsigned : exists sdp_u_proof_final_qr_signed sdp_v_proof_final_qr_signed. (q + r) + 2 * sdp_u_proof_final_qr_signed = (q + m + s) + 2 * sdp_v_proof_final_qr_signed
  23. 0023specialize signed_remainder_sum_mod_two p
  24. 0024specialize signed_remainder_sum_mod_two q
  25. 0025specialize signed_remainder_sum_mod_two r
  26. 0026specialize signed_remainder_sum_mod_two m
  27. 0027specialize signed_remainder_sum_mod_two s
  28. 0028apply signed_remainder_sum_mod_two
  29. 0029exact hp
  30. 0030exact hbranch
  31. 0031specialize mod_eq_trans 2
  32. 0032specialize mod_eq_trans x
  33. 0033specialize mod_eq_trans (q + r)
  34. 0034specialize mod_eq_trans (q + m + s)
  35. 0035apply mod_eq_trans
  36. 0036exact hxqr
  37. 0037exact hqrsigned