PA0034 · theorem

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.

Statement with defined notation

∀ p. ∀ h. ∀ b. ∀ c. ∀ i. ∀ x. p = 2 · h + 1 → Range(b,c,1,h) → Lt(i,h) → BetaAt(b,c,i,x) → UnitResidue(p,x)

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

PD0002 Lt PD0013 BetaAt PD0018 Range PD0030 UnitResidue

4 occurrences

In local proof propositions

PD0001 Le PD0002 Lt

2 occurrences

Exact expanded native-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))

Proof neighborhood

Direct theorem prerequisites

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 theorem dependents

PA0072 gauss_half_range_signed_choices PA007C gauss_signed_half_magnitude_injective PA0083 prime_half_range_product_coprime

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

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.

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 (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
  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
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 defined 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 : Le(x,h)
    Exact native replay linehave hxh : exists k. k + x = h
  42. 0042rewrite hxsi
  43. 0043exact hi
  44. 0044have hhp : Lt(h,p)
    Exact native replay linehave 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