PA00C0

prime_scaled_half_division_prefix_exists

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

An odd-prime half range has exact scaled quotient/remainder codes.

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 b c. p = 2 * h + 1 -> ((~(p = 1) /\ forall frp_prime_left_eisenstein_division_prime frp_prime_right_eisenstein_division_prime. p = frp_prime_left_eisenstein_division_prime * frp_prime_right_eisenstein_division_prime -> frp_prime_left_eisenstein_division_prime = 1 \/ frp_prime_right_eisenstein_division_prime = 1)) -> (forall gsp_range_index_eisenstein_scaled_half_range. (exists gsp_lt_gap_eisenstein_scaled_half_range_range_bound. gsp_lt_gap_eisenstein_scaled_half_range_range_bound + S gsp_range_index_eisenstein_scaled_half_range = h) -> (((exists gsp_beta_height_eisenstein_scaled_half_range_range_entry. gsp_beta_height_eisenstein_scaled_half_range_range_entry + S (1 + gsp_range_index_eisenstein_scaled_half_range) = S ((S (gsp_range_index_eisenstein_scaled_half_range)) * c)) /\ exists gsp_beta_quotient_eisenstein_scaled_half_range_range_entry. b = gsp_beta_quotient_eisenstein_scaled_half_range_range_entry * S ((S (gsp_range_index_eisenstein_scaled_half_range)) * c) + (1 + gsp_range_index_eisenstein_scaled_half_range)))) -> (exists tb tc qb qc rb rc. ((forall esd_index_eisenstein_scaled_exact esd_value_eisenstein_scaled_exact. (exists esd_gap_eisenstein_scaled_exact. esd_gap_eisenstein_scaled_exact + S esd_index_eisenstein_scaled_exact = h) -> (((exists ff_h_esd_eisenstein_scaled_exact_decoded. ff_h_esd_eisenstein_scaled_exact_decoded + S (esd_value_eisenstein_scaled_exact) = S ((S (esd_index_eisenstein_scaled_exact)) * tc)) /\ exists ff_q_esd_eisenstein_scaled_exact_decoded. tb = ff_q_esd_eisenstein_scaled_exact_decoded * S ((S (esd_index_eisenstein_scaled_exact)) * tc) + (esd_value_eisenstein_scaled_exact))) -> esd_value_eisenstein_scaled_exact = a * (1 + esd_index_eisenstein_scaled_exact)) /\ (forall fdp_index_eisenstein_division_prefix. (exists gsp_lt_gap_eisenstein_division_prefix_index_bound. gsp_lt_gap_eisenstein_division_prefix_index_bound + S fdp_index_eisenstein_division_prefix = h) -> exists fdp_value_eisenstein_division_prefix fdp_quotient_eisenstein_division_prefix fdp_remainder_eisenstein_division_prefix. (((exists ff_h_fdp_eisenstein_division_prefix_source. ff_h_fdp_eisenstein_division_prefix_source + S (fdp_value_eisenstein_division_prefix) = S ((S (fdp_index_eisenstein_division_prefix)) * tc)) /\ exists ff_q_fdp_eisenstein_division_prefix_source. tb = ff_q_fdp_eisenstein_division_prefix_source * S ((S (fdp_index_eisenstein_division_prefix)) * tc) + (fdp_value_eisenstein_division_prefix))) /\ ((((exists ff_h_fdp_eisenstein_division_prefix_quotient_entry. ff_h_fdp_eisenstein_division_prefix_quotient_entry + S (fdp_quotient_eisenstein_division_prefix) = S ((S (fdp_index_eisenstein_division_prefix)) * qc)) /\ exists ff_q_fdp_eisenstein_division_prefix_quotient_entry. qb = ff_q_fdp_eisenstein_division_prefix_quotient_entry * S ((S (fdp_index_eisenstein_division_prefix)) * qc) + (fdp_quotient_eisenstein_division_prefix))) /\ ((((exists ff_h_fdp_eisenstein_division_prefix_remainder_entry. ff_h_fdp_eisenstein_division_prefix_remainder_entry + S (fdp_remainder_eisenstein_division_prefix) = S ((S (fdp_index_eisenstein_division_prefix)) * rc)) /\ exists ff_q_fdp_eisenstein_division_prefix_remainder_entry. rb = ff_q_fdp_eisenstein_division_prefix_remainder_entry * S ((S (fdp_index_eisenstein_division_prefix)) * rc) + (fdp_remainder_eisenstein_division_prefix))) /\ (fdp_value_eisenstein_division_prefix = p * fdp_quotient_eisenstein_division_prefix + fdp_remainder_eisenstein_division_prefix /\ (exists gsp_lt_gap_eisenstein_division_prefix_remainder_bound. gsp_lt_gap_eisenstein_division_prefix_remainder_bound + S fdp_remainder_eisenstein_division_prefix = p)))))))

Structural proof guide

Generated structural guide

An odd-prime half range has exact scaled quotient/remainder codes.

Use the direct prerequisites beta_repeat_exists, beta_pointwise_mul_prefix_exists, beta_scaled_successor_prefix_from_pointwise, prime_nonzero, beta_division_prefix_exists as previously established PA formulas.

The proof proceeds by case analysis (8), intermediate claims (5).

Referenced ingredients

PA0045 beta_repeat_exists PA007L beta_pointwise_mul_prefix_exists PA00BW beta_scaled_successor_prefix_from_pointwise PA0031 prime_nonzero PA00BY beta_division_prefix_exists

Proof neighborhood

Direct dependencies

PA0045 beta_repeat_exists PA007L beta_pointwise_mul_prefix_exists PA00BW beta_scaled_successor_prefix_from_pointwise PA0031 prime_nonzero PA00BY beta_division_prefix_exists

Direct dependents

PA00C1 prime_scaled_half_quotient_sum_exists

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

62 script commands · 13 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 (5)
beta repeat existsbeta pointwise mul prefix existsbeta scaled successor prefix from pointwiseprime nonzerobeta division prefix exists

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–8

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 b
  5. L5
    intro c
  6. L6
    intro hpodd
  7. L7
    intro hprime
  8. L8
    intro hhalf
02Establish hrepeat_existsL9–12

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

  1. L9
    have hrepeat_exists : exists ab ac. (forall ff_i_eisenstein_repeat_exists. (exists ff_lt_eisenstein_repeat_exists_bound. ff_lt_eisenstein_repeat_exists_bound + S ff_i_eisenstein_repeat_exists = h) -> (((exists ff_h_eisenstein_repeat_exists_decoded. ff_h_eisenstein_repeat_exists_decoded + S (a) = S ((S (ff_i_eisenstein_repeat_exists)) * ac)) /\ exists ff_q_eisenstein_repeat_exists_decoded. ab = ff_q_eisenstein_repeat_exists_decoded * S ((S (ff_i_eisenstein_repeat_exists)) * ac) + (a))))
  2. L10
    specialize beta_repeat_exists a
  3. L11
    specialize beta_repeat_exists h
  4. L12
    exact beta_repeat_exists
03Separate the logical casesL13–14

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

  1. L13
    cases hrepeat_exists
  2. L14
    cases hrepeat_exists_witness
04Establish hpointwise_existsL15–21

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

  1. L15
    have hpointwise_exists : ∃ tb. ∃ tc. ∀ y. ∀ z. ∀ n. ∀ m. Lt(y,h) → BetaAt(x,x1,y,z) → BetaAt(b,c,y,n) → BetaAt(tb,tc,y,m) → m = z · nDefinitions: LtBetaAt
  2. L16
    specialize beta_pointwise_mul_prefix_exists x
  3. L17
    specialize beta_pointwise_mul_prefix_exists x1
  4. L18
    specialize beta_pointwise_mul_prefix_exists b
  5. L19
    specialize beta_pointwise_mul_prefix_exists c
  6. L20
    specialize beta_pointwise_mul_prefix_exists h
  7. L21
    exact beta_pointwise_mul_prefix_exists
05Separate the logical casesL22–23

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

  1. L22
    cases hpointwise_exists
  2. L23
    cases hpointwise_exists_witness
06Establish hscaledL24–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta scaled successor prefix from pointwise.

  1. L24
    have hscaled : ∀ esd_index_eisenstein_local_exact. ∀ esd_value_eisenstein_local_exact. Lt(esd_index_eisenstein_local_exact,h) → BetaAt(x2,x3,esd_index_eisenstein_local_exact,esd_value_eisenstein_local_exact) → esd_value_eisenstein_local_exact = a · (1 + esd_index_eisenstein_local_exact)Definitions: LtBetaAt
  2. L25
    specialize beta_scaled_successor_prefix_from_pointwise a
  3. L26
    specialize beta_scaled_successor_prefix_from_pointwise b
  4. L27
    specialize beta_scaled_successor_prefix_from_pointwise c
  5. L28
    specialize beta_scaled_successor_prefix_from_pointwise x
  6. L29
    specialize beta_scaled_successor_prefix_from_pointwise x1
  7. L30
    specialize beta_scaled_successor_prefix_from_pointwise x2
  8. L31
    specialize beta_scaled_successor_prefix_from_pointwise x3
  9. L32
    specialize beta_scaled_successor_prefix_from_pointwise h
  10. L33
    apply beta_scaled_successor_prefix_from_pointwise
07Use earlier factsL34–36

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

  1. L34
    exact hhalf
  2. L35
    exact hrepeat_exists_witness_witness
  3. L36
    exact hpointwise_exists_witness_witness
08Establish hp0L37–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime nonzero.

  1. L37
    have hp0 : ~(p = 0)
  2. L38
    intro hpzero
  3. L39
    specialize prime_nonzero p
  4. L40
    apply prime_nonzero
  5. L41
    exact hprime
  6. L42
    exact hpzero
09Establish hdivision_existsL43–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta division prefix exists.

  1. L43
    have hdivision_exists : ∃ qb. ∃ qc. ∃ rb. ∃ rc. DivisionPrefix(p,x2,x3,qb,qc,rb,rc,h)Definitions: DivisionPrefix
  2. L44
    specialize beta_division_prefix_exists p
  3. L45
    specialize beta_division_prefix_exists x2
  4. L46
    specialize beta_division_prefix_exists x3
  5. L47
    specialize beta_division_prefix_exists h
  6. L48
    apply beta_division_prefix_exists
  7. L49
    exact hp0
10Separate the logical casesL50–53

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

  1. L50
    cases hdivision_exists
  2. L51
    cases hdivision_exists_witness
  3. L52
    cases hdivision_exists_witness_witness
  4. L53
    cases hdivision_exists_witness_witness_witness
11Construct an explicit witnessL54–59

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

  1. L54
    exists x2
  2. L55
    exists x3
  3. L56
    exists x4
  4. L57
    exists x5
  5. L58
    exists x6
  6. L59
    exists x7
12Separate the logical casesL60–60

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

  1. L60
    split
13Use earlier factsL61–62

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

  1. L61
    exact hscaled
  2. L62
    exact hdivision_exists_witness_witness_witness_witness

Library-wide reading audit

Original exact command ledger · 62 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro hpodd
  7. 0007intro hprime
  8. 0008intro hhalf
  9. 0009have hrepeat_exists : exists ab ac. (forall ff_i_eisenstein_repeat_exists. (exists ff_lt_eisenstein_repeat_exists_bound. ff_lt_eisenstein_repeat_exists_bound + S ff_i_eisenstein_repeat_exists = h) -> (((exists ff_h_eisenstein_repeat_exists_decoded. ff_h_eisenstein_repeat_exists_decoded + S (a) = S ((S (ff_i_eisenstein_repeat_exists)) * ac)) /\ exists ff_q_eisenstein_repeat_exists_decoded. ab = ff_q_eisenstein_repeat_exists_decoded * S ((S (ff_i_eisenstein_repeat_exists)) * ac) + (a))))
  10. 0010specialize beta_repeat_exists a
  11. 0011specialize beta_repeat_exists h
  12. 0012exact beta_repeat_exists
  13. 0013cases hrepeat_exists
  14. 0014cases hrepeat_exists_witness
  15. 0015have hpointwise_exists : exists tb tc. (forall fpmp_index_eisenstein_pointwise_exists fpmp_left_eisenstein_pointwise_exists fpmp_right_eisenstein_pointwise_exists fpmp_target_eisenstein_pointwise_exists. (exists fpmp_gap_eisenstein_pointwise_exists. fpmp_gap_eisenstein_pointwise_exists + S fpmp_index_eisenstein_pointwise_exists = h) -> (((exists ff_h_fpmp_eisenstein_pointwise_exists_left. ff_h_fpmp_eisenstein_pointwise_exists_left + S (fpmp_left_eisenstein_pointwise_exists) = S ((S (fpmp_index_eisenstein_pointwise_exists)) * x1)) /\ exists ff_q_fpmp_eisenstein_pointwise_exists_left. x = ff_q_fpmp_eisenstein_pointwise_exists_left * S ((S (fpmp_index_eisenstein_pointwise_exists)) * x1) + (fpmp_left_eisenstein_pointwise_exists))) -> (((exists ff_h_fpmp_eisenstein_pointwise_exists_right. ff_h_fpmp_eisenstein_pointwise_exists_right + S (fpmp_right_eisenstein_pointwise_exists) = S ((S (fpmp_index_eisenstein_pointwise_exists)) * c)) /\ exists ff_q_fpmp_eisenstein_pointwise_exists_right. b = ff_q_fpmp_eisenstein_pointwise_exists_right * S ((S (fpmp_index_eisenstein_pointwise_exists)) * c) + (fpmp_right_eisenstein_pointwise_exists))) -> (((exists ff_h_fpmp_eisenstein_pointwise_exists_target. ff_h_fpmp_eisenstein_pointwise_exists_target + S (fpmp_target_eisenstein_pointwise_exists) = S ((S (fpmp_index_eisenstein_pointwise_exists)) * tc)) /\ exists ff_q_fpmp_eisenstein_pointwise_exists_target. tb = ff_q_fpmp_eisenstein_pointwise_exists_target * S ((S (fpmp_index_eisenstein_pointwise_exists)) * tc) + (fpmp_target_eisenstein_pointwise_exists))) -> fpmp_target_eisenstein_pointwise_exists = fpmp_left_eisenstein_pointwise_exists * fpmp_right_eisenstein_pointwise_exists)
  16. 0016specialize beta_pointwise_mul_prefix_exists x
  17. 0017specialize beta_pointwise_mul_prefix_exists x1
  18. 0018specialize beta_pointwise_mul_prefix_exists b
  19. 0019specialize beta_pointwise_mul_prefix_exists c
  20. 0020specialize beta_pointwise_mul_prefix_exists h
  21. 0021exact beta_pointwise_mul_prefix_exists
  22. 0022cases hpointwise_exists
  23. 0023cases hpointwise_exists_witness
  24. 0024have hscaled : forall esd_index_eisenstein_local_exact esd_value_eisenstein_local_exact. (exists esd_gap_eisenstein_local_exact. esd_gap_eisenstein_local_exact + S esd_index_eisenstein_local_exact = h) -> (((exists ff_h_esd_eisenstein_local_exact_decoded. ff_h_esd_eisenstein_local_exact_decoded + S (esd_value_eisenstein_local_exact) = S ((S (esd_index_eisenstein_local_exact)) * x3)) /\ exists ff_q_esd_eisenstein_local_exact_decoded. x2 = ff_q_esd_eisenstein_local_exact_decoded * S ((S (esd_index_eisenstein_local_exact)) * x3) + (esd_value_eisenstein_local_exact))) -> esd_value_eisenstein_local_exact = a * (1 + esd_index_eisenstein_local_exact)
  25. 0025specialize beta_scaled_successor_prefix_from_pointwise a
  26. 0026specialize beta_scaled_successor_prefix_from_pointwise b
  27. 0027specialize beta_scaled_successor_prefix_from_pointwise c
  28. 0028specialize beta_scaled_successor_prefix_from_pointwise x
  29. 0029specialize beta_scaled_successor_prefix_from_pointwise x1
  30. 0030specialize beta_scaled_successor_prefix_from_pointwise x2
  31. 0031specialize beta_scaled_successor_prefix_from_pointwise x3
  32. 0032specialize beta_scaled_successor_prefix_from_pointwise h
  33. 0033apply beta_scaled_successor_prefix_from_pointwise
  34. 0034exact hhalf
  35. 0035exact hrepeat_exists_witness_witness
  36. 0036exact hpointwise_exists_witness_witness
  37. 0037have hp0 : ~(p = 0)
  38. 0038intro hpzero
  39. 0039specialize prime_nonzero p
  40. 0040apply prime_nonzero
  41. 0041exact hprime
  42. 0042exact hpzero
  43. 0043have hdivision_exists : exists qb qc rb rc. (forall fdp_index_eisenstein_division_exists. (exists gsp_lt_gap_eisenstein_division_exists_index_bound. gsp_lt_gap_eisenstein_division_exists_index_bound + S fdp_index_eisenstein_division_exists = h) -> exists fdp_value_eisenstein_division_exists fdp_quotient_eisenstein_division_exists fdp_remainder_eisenstein_division_exists. (((exists ff_h_fdp_eisenstein_division_exists_source. ff_h_fdp_eisenstein_division_exists_source + S (fdp_value_eisenstein_division_exists) = S ((S (fdp_index_eisenstein_division_exists)) * x3)) /\ exists ff_q_fdp_eisenstein_division_exists_source. x2 = ff_q_fdp_eisenstein_division_exists_source * S ((S (fdp_index_eisenstein_division_exists)) * x3) + (fdp_value_eisenstein_division_exists))) /\ ((((exists ff_h_fdp_eisenstein_division_exists_quotient_entry. ff_h_fdp_eisenstein_division_exists_quotient_entry + S (fdp_quotient_eisenstein_division_exists) = S ((S (fdp_index_eisenstein_division_exists)) * qc)) /\ exists ff_q_fdp_eisenstein_division_exists_quotient_entry. qb = ff_q_fdp_eisenstein_division_exists_quotient_entry * S ((S (fdp_index_eisenstein_division_exists)) * qc) + (fdp_quotient_eisenstein_division_exists))) /\ ((((exists ff_h_fdp_eisenstein_division_exists_remainder_entry. ff_h_fdp_eisenstein_division_exists_remainder_entry + S (fdp_remainder_eisenstein_division_exists) = S ((S (fdp_index_eisenstein_division_exists)) * rc)) /\ exists ff_q_fdp_eisenstein_division_exists_remainder_entry. rb = ff_q_fdp_eisenstein_division_exists_remainder_entry * S ((S (fdp_index_eisenstein_division_exists)) * rc) + (fdp_remainder_eisenstein_division_exists))) /\ (fdp_value_eisenstein_division_exists = p * fdp_quotient_eisenstein_division_exists + fdp_remainder_eisenstein_division_exists /\ (exists gsp_lt_gap_eisenstein_division_exists_remainder_bound. gsp_lt_gap_eisenstein_division_exists_remainder_bound + S fdp_remainder_eisenstein_division_exists = p)))))
  44. 0044specialize beta_division_prefix_exists p
  45. 0045specialize beta_division_prefix_exists x2
  46. 0046specialize beta_division_prefix_exists x3
  47. 0047specialize beta_division_prefix_exists h
  48. 0048apply beta_division_prefix_exists
  49. 0049exact hp0
  50. 0050cases hdivision_exists
  51. 0051cases hdivision_exists_witness
  52. 0052cases hdivision_exists_witness_witness
  53. 0053cases hdivision_exists_witness_witness_witness
  54. 0054exists x2
  55. 0055exists x3
  56. 0056exists x4
  57. 0057exists x5
  58. 0058exists x6
  59. 0059exists x7
  60. 0060split
  61. 0061exact hscaled
  62. 0062exact hdivision_exists_witness_witness_witness_witness