PA0034

beta_half_range_entry_bounds

Stable checked-use theorem · independently closed

Entries 1 through h in an odd half-range are nonzero and below p.

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 b c i x. p = 2 * h + 1 -> (forall gh_i_half. (exists gh_lt_half_bound. gh_lt_half_bound + S gh_i_half = h) -> (((exists gh_h_half. gh_h_half + S (1 + gh_i_half) = S ((S gh_i_half) * c)) /\ exists gh_q_half. b = gh_q_half * S ((S gh_i_half) * c) + (1 + gh_i_half)))) -> (exists gh_lt_half_i. gh_lt_half_i + S i = h) -> (((exists ff_h_half_i. ff_h_half_i + S (x) = S ((S (i)) * c)) /\ exists ff_q_half_i. b = ff_q_half_i * S ((S (i)) * c) + (x))) -> (~(x = 0) /\ (exists gh_lt_half_value. gh_lt_half_value + S x = p))

Structural proof guide

Generated structural guide

Entries 1 through h in an odd half-range are nonzero and below p.

Use the direct prerequisites beta_range_entry_eq, zero_add, add_succ_left, mul_succ_left, mul_zero_left, add_assoc, lt_of_le_of_lt as previously established PA formulas.

The proof proceeds by intermediate claims (5), equality transport (2), certified simplification (1).

Referenced ingredients

PA0032 beta_range_entry_eq PA0001 zero_add PA000E add_succ_left PA000G mul_succ_left PA000D mul_zero_left PA0009 add_assoc PA0033 lt_of_le_of_lt

Proof neighborhood

Direct dependencies

PA0032 beta_range_entry_eq PA0001 zero_add PA000E add_succ_left PA000G mul_succ_left PA000D mul_zero_left PA0009 add_assoc PA0033 lt_of_le_of_lt

Direct dependents

PA0072 gauss_half_range_signed_choices PA007C gauss_signed_half_magnitude_injective PA0083 prime_half_range_product_coprime

Formal native tactic body

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

Read the argument

Proof checkpoints

53 script commands · 15 reading checkpoints · 5 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 (4)
beta range entry eqzero addadd succ leftlt of le of lt
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 b
  4. L4
    intro c
  5. L5
    intro i
  6. L6
    intro x
  7. L7
    intro hp
  8. L8
    intro hrange
  9. L9
    intro hi
  10. L10
    intro hxi
02Establish hxL11–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta range entry eq.

  1. L11
    have hx : x = 1 + i
  2. L12
    specialize beta_range_entry_eq b
  3. L13
    specialize beta_range_entry_eq c
  4. L14
    specialize beta_range_entry_eq 1
  5. L15
    specialize beta_range_entry_eq h
  6. L16
    specialize beta_range_entry_eq i
  7. L17
    specialize beta_range_entry_eq x
  8. L18
    apply beta_range_entry_eq
  9. L19
    exact hrange
  10. L20
    exact hi
03Use earlier factsL21–21

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

  1. L21
    exact hxi
04Establish honeL22–29

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

  1. L22
    have hone : 1 + i = S i
  2. L23
    trans S (0 + i)
  3. L24
    specialize add_succ_left 0
  4. L25
    specialize add_succ_left i
  5. L26
    exact add_succ_left
  6. L27
    congr
  7. L28
    specialize zero_add i
  8. L29
    exact zero_add
05Establish hxsiL30–33

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

  1. L30
    have hxsi : x = S i
  2. L31
    trans 1 + i
  3. L32
    exact hx
  4. L33
    exact hone
06Separate the logical casesL34–34

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

  1. L34
    split
07Fix variables and assumptionsL35–35

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

  1. L35
    intro hx0
08Use earlier factsL36–36

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

  1. L36
    apply PA1
09Calculate and transport equalitiesL37–38

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

  1. L37
    trans x
  2. L38
    symm
10Use earlier factsL39–40

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

  1. L39
    exact hxsi
  2. L40
    exact hx0
11Establish hxhL41–43

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

  1. L41
    have hxh : exists k. k + x = h
  2. L42
    rewrite hxsi
  3. L43
    exact hi
12Establish hhpL44–44

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

  1. L44
    have hhp : exists k. k + S h = p
13Construct an explicit witnessL45–45

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

  1. L45
    exists h
14Calculate and transport equalitiesL46–47

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

  1. L46
    rewrite hp
  2. L47
    simp [mul_succ_left, mul_zero_left, add_succ_left, zero_add, add_assoc]
15Use earlier factsL48–53

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

  1. L48
    specialize lt_of_le_of_lt x
  2. L49
    specialize lt_of_le_of_lt h
  3. L50
    specialize lt_of_le_of_lt p
  4. L51
    apply lt_of_le_of_lt
  5. L52
    exact hxh
  6. L53
    exact hhp

Library-wide reading audit

Original exact command ledger · 53 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro b
  4. 0004intro c
  5. 0005intro i
  6. 0006intro x
  7. 0007intro hp
  8. 0008intro hrange
  9. 0009intro hi
  10. 0010intro hxi
  11. 0011have hx : x = 1 + i
  12. 0012specialize beta_range_entry_eq b
  13. 0013specialize beta_range_entry_eq c
  14. 0014specialize beta_range_entry_eq 1
  15. 0015specialize beta_range_entry_eq h
  16. 0016specialize beta_range_entry_eq i
  17. 0017specialize beta_range_entry_eq x
  18. 0018apply beta_range_entry_eq
  19. 0019exact hrange
  20. 0020exact hi
  21. 0021exact hxi
  22. 0022have hone : 1 + i = S i
  23. 0023trans S (0 + i)
  24. 0024specialize add_succ_left 0
  25. 0025specialize add_succ_left i
  26. 0026exact add_succ_left
  27. 0027congr
  28. 0028specialize zero_add i
  29. 0029exact zero_add
  30. 0030have hxsi : x = S i
  31. 0031trans 1 + i
  32. 0032exact hx
  33. 0033exact hone
  34. 0034split
  35. 0035intro hx0
  36. 0036apply PA1
  37. 0037trans x
  38. 0038symm
  39. 0039exact hxsi
  40. 0040exact hx0
  41. 0041have hxh : exists k. k + x = h
  42. 0042rewrite hxsi
  43. 0043exact hi
  44. 0044have hhp : exists k. k + S h = p
  45. 0045exists h
  46. 0046rewrite hp
  47. 0047simp [mul_succ_left, mul_zero_left, add_succ_left, zero_add, add_assoc]
  48. 0048specialize lt_of_le_of_lt x
  49. 0049specialize lt_of_le_of_lt h
  50. 0050specialize lt_of_le_of_lt p
  51. 0051apply lt_of_le_of_lt
  52. 0052exact hxh
  53. 0053exact hhp