PA00C1 · theorem

prime_scaled_half_quotient_sum_exists

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

The quotient code additionally carries its native finite floor sum.

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. ∀ a. ∀ b. ∀ c. p = 2 · h + 1 → Prime(p) → Range(b,c,1,h) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. (∀ j. ∀ u. Lt(j,h) → BetaAt(x,y,j,u) → u = a · (1 + j)) ∧ (DivisionPrefix(p,x,y,z,n,m,k,h) ∧ Sum(z,n,h,i))

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 PD0004 Prime PD0013 BetaAt PD0015 Sum PD0018 Range PD0040 DivisionPrefix

6 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0015 Sum PD0040 DivisionPrefix

4 occurrences

Exact expanded native-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 Q. ((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))))) /\ (exists ff_u_eisenstein_quotient_sum ff_v_eisenstein_quotient_sum. ((((exists ff_h_eisenstein_quotient_sum_start. ff_h_eisenstein_quotient_sum_start + S (0) = S ((S (0)) * ff_v_eisenstein_quotient_sum)) /\ exists ff_q_eisenstein_quotient_sum_start. ff_u_eisenstein_quotient_sum = ff_q_eisenstein_quotient_sum_start * S ((S (0)) * ff_v_eisenstein_quotient_sum) + (0))) /\ ((((exists ff_h_eisenstein_quotient_sum_terminal. ff_h_eisenstein_quotient_sum_terminal + S (Q) = S ((S (h)) * ff_v_eisenstein_quotient_sum)) /\ exists ff_q_eisenstein_quotient_sum_terminal. ff_u_eisenstein_quotient_sum = ff_q_eisenstein_quotient_sum_terminal * S ((S (h)) * ff_v_eisenstein_quotient_sum) + (Q))) /\ forall ff_i_eisenstein_quotient_sum. (exists ff_lt_eisenstein_quotient_sum_bound. ff_lt_eisenstein_quotient_sum_bound + S ff_i_eisenstein_quotient_sum = h) -> exists ff_a_eisenstein_quotient_sum ff_r_eisenstein_quotient_sum ff_s_eisenstein_quotient_sum. ((((exists ff_h_eisenstein_quotient_sum_summand. ff_h_eisenstein_quotient_sum_summand + S (ff_a_eisenstein_quotient_sum) = S ((S (ff_i_eisenstein_quotient_sum)) * qc)) /\ exists ff_q_eisenstein_quotient_sum_summand. qb = ff_q_eisenstein_quotient_sum_summand * S ((S (ff_i_eisenstein_quotient_sum)) * qc) + (ff_a_eisenstein_quotient_sum))) /\ ((((exists ff_h_eisenstein_quotient_sum_partial. ff_h_eisenstein_quotient_sum_partial + S (ff_r_eisenstein_quotient_sum) = S ((S (ff_i_eisenstein_quotient_sum)) * ff_v_eisenstein_quotient_sum)) /\ exists ff_q_eisenstein_quotient_sum_partial. ff_u_eisenstein_quotient_sum = ff_q_eisenstein_quotient_sum_partial * S ((S (ff_i_eisenstein_quotient_sum)) * ff_v_eisenstein_quotient_sum) + (ff_r_eisenstein_quotient_sum))) /\ ((((exists ff_h_eisenstein_quotient_sum_successor. ff_h_eisenstein_quotient_sum_successor + S (ff_s_eisenstein_quotient_sum) = S ((S (S ff_i_eisenstein_quotient_sum)) * ff_v_eisenstein_quotient_sum)) /\ exists ff_q_eisenstein_quotient_sum_successor. ff_u_eisenstein_quotient_sum = ff_q_eisenstein_quotient_sum_successor * S ((S (S ff_i_eisenstein_quotient_sum)) * ff_v_eisenstein_quotient_sum) + (ff_s_eisenstein_quotient_sum))) /\ ff_s_eisenstein_quotient_sum = ff_r_eisenstein_quotient_sum + ff_a_eisenstein_quotient_sum)))))))))

Proof neighborhood

Direct theorem prerequisites

PA00C0 prime_scaled_half_division_prefix_exists PA003H beta_sum_exists

Direct theorem dependents

PA00D7 odd_prime_gauss_eisenstein_orientation_data_exists

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

43 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.

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 (2)
prime scaled half division prefix existsbeta sum exists
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 hdivisionL9–18

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

  1. L9
    have hdivision : ∃ tb. ∃ tc. ∃ qb. ∃ qc. ∃ rb. ∃ rc. (∀ x. ∀ y. Lt(x,h) → BetaAt(tb,tc,x,y) → y = a · (1 + x)) ∧ DivisionPrefix(p,tb,tc,qb,qc,rb,rc,h)Definitions: Lt(x,h)BetaAt(tb,tc,x,y)DivisionPrefix(p,tb,tc,qb,qc,rb,rc,h)Original native command in the exact edition
  2. L10
    specialize prime_scaled_half_division_prefix_exists p
  3. L11
    specialize prime_scaled_half_division_prefix_exists h
  4. L12
    specialize prime_scaled_half_division_prefix_exists a
  5. L13
    specialize prime_scaled_half_division_prefix_exists b
  6. L14
    specialize prime_scaled_half_division_prefix_exists c
  7. L15
    apply prime_scaled_half_division_prefix_exists
  8. L16
    exact hpodd
  9. L17
    exact hprime
  10. L18
    exact hhalf
03Separate the logical casesL19–25

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

  1. L19
    cases hdivision
  2. L20
    cases hdivision_witness
  3. L21
    cases hdivision_witness_witness
  4. L22
    cases hdivision_witness_witness_witness
  5. L23
    cases hdivision_witness_witness_witness_witness
  6. L24
    cases hdivision_witness_witness_witness_witness_witness
  7. L25
    cases hdivision_witness_witness_witness_witness_witness_witness
04Establish hsum_existsL26–30

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

  1. L26
    have hsum_exists : ∃ Q. Sum(x2,x3,h,Q)Definitions: Sum(x2,x3,h,Q)Original native command in the exact edition
  2. L27
    specialize beta_sum_exists x2
  3. L28
    specialize beta_sum_exists x3
  4. L29
    specialize beta_sum_exists h
  5. L30
    exact beta_sum_exists
05Separate the logical casesL31–31

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

  1. L31
    cases hsum_exists
06Construct an explicit witnessL32–38

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

  1. L32
    exists x
  2. L33
    exists x1
  3. L34
    exists x2
  4. L35
    exists x3
  5. L36
    exists x4
  6. L37
    exists x5
  7. L38
    exists x6
07Separate the logical casesL39–39

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

  1. L39
    split
08Use earlier factsL40–40

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

  1. L40
    exact hdivision_witness_witness_witness_witness_witness_witness_left
09Separate the logical casesL41–41

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

  1. L41
    split
10Use earlier factsL42–43

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

  1. L42
    exact hdivision_witness_witness_witness_witness_witness_witness_right
  2. L43
    exact hsum_exists_witness

Library-wide reading audit

Original defined command ledger · 43 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 hdivision : ∃ tb. ∃ tc. ∃ qb. ∃ qc. ∃ rb. ∃ rc. (∀ x. ∀ y. Lt(x,h) → BetaAt(tb,tc,x,y) → y = a · (1 + x)) ∧ DivisionPrefix(p,tb,tc,qb,qc,rb,rc,h)
    Exact native replay linehave hdivision : exists tb tc qb qc rb rc. ((forall esd_index_eisenstein_local_package_scaled esd_value_eisenstein_local_package_scaled. (exists esd_gap_eisenstein_local_package_scaled. esd_gap_eisenstein_local_package_scaled + S esd_index_eisenstein_local_package_scaled = h) -> (((exists ff_h_esd_eisenstein_local_package_scaled_decoded. ff_h_esd_eisenstein_local_package_scaled_decoded + S (esd_value_eisenstein_local_package_scaled) = S ((S (esd_index_eisenstein_local_package_scaled)) * tc)) /\ exists ff_q_esd_eisenstein_local_package_scaled_decoded. tb = ff_q_esd_eisenstein_local_package_scaled_decoded * S ((S (esd_index_eisenstein_local_package_scaled)) * tc) + (esd_value_eisenstein_local_package_scaled))) -> esd_value_eisenstein_local_package_scaled = a * (1 + esd_index_eisenstein_local_package_scaled)) /\ (forall fdp_index_eisenstein_local_package_division. (exists gsp_lt_gap_eisenstein_local_package_division_index_bound. gsp_lt_gap_eisenstein_local_package_division_index_bound + S fdp_index_eisenstein_local_package_division = h) -> exists fdp_value_eisenstein_local_package_division fdp_quotient_eisenstein_local_package_division fdp_remainder_eisenstein_local_package_division. (((exists ff_h_fdp_eisenstein_local_package_division_source. ff_h_fdp_eisenstein_local_package_division_source + S (fdp_value_eisenstein_local_package_division) = S ((S (fdp_index_eisenstein_local_package_division)) * tc)) /\ exists ff_q_fdp_eisenstein_local_package_division_source. tb = ff_q_fdp_eisenstein_local_package_division_source * S ((S (fdp_index_eisenstein_local_package_division)) * tc) + (fdp_value_eisenstein_local_package_division))) /\ ((((exists ff_h_fdp_eisenstein_local_package_division_quotient_entry. ff_h_fdp_eisenstein_local_package_division_quotient_entry + S (fdp_quotient_eisenstein_local_package_division) = S ((S (fdp_index_eisenstein_local_package_division)) * qc)) /\ exists ff_q_fdp_eisenstein_local_package_division_quotient_entry. qb = ff_q_fdp_eisenstein_local_package_division_quotient_entry * S ((S (fdp_index_eisenstein_local_package_division)) * qc) + (fdp_quotient_eisenstein_local_package_division))) /\ ((((exists ff_h_fdp_eisenstein_local_package_division_remainder_entry. ff_h_fdp_eisenstein_local_package_division_remainder_entry + S (fdp_remainder_eisenstein_local_package_division) = S ((S (fdp_index_eisenstein_local_package_division)) * rc)) /\ exists ff_q_fdp_eisenstein_local_package_division_remainder_entry. rb = ff_q_fdp_eisenstein_local_package_division_remainder_entry * S ((S (fdp_index_eisenstein_local_package_division)) * rc) + (fdp_remainder_eisenstein_local_package_division))) /\ (fdp_value_eisenstein_local_package_division = p * fdp_quotient_eisenstein_local_package_division + fdp_remainder_eisenstein_local_package_division /\ (exists gsp_lt_gap_eisenstein_local_package_division_remainder_bound. gsp_lt_gap_eisenstein_local_package_division_remainder_bound + S fdp_remainder_eisenstein_local_package_division = p))))))
  10. 0010specialize prime_scaled_half_division_prefix_exists p
  11. 0011specialize prime_scaled_half_division_prefix_exists h
  12. 0012specialize prime_scaled_half_division_prefix_exists a
  13. 0013specialize prime_scaled_half_division_prefix_exists b
  14. 0014specialize prime_scaled_half_division_prefix_exists c
  15. 0015apply prime_scaled_half_division_prefix_exists
  16. 0016exact hpodd
  17. 0017exact hprime
  18. 0018exact hhalf
  19. 0019cases hdivision
  20. 0020cases hdivision_witness
  21. 0021cases hdivision_witness_witness
  22. 0022cases hdivision_witness_witness_witness
  23. 0023cases hdivision_witness_witness_witness_witness
  24. 0024cases hdivision_witness_witness_witness_witness_witness
  25. 0025cases hdivision_witness_witness_witness_witness_witness_witness
  26. 0026have hsum_exists : ∃ Q. Sum(x2,x3,h,Q)
    Exact native replay linehave hsum_exists : exists Q. (exists ff_u_eisenstein_local_sum_exists ff_v_eisenstein_local_sum_exists. ((((exists ff_h_eisenstein_local_sum_exists_start. ff_h_eisenstein_local_sum_exists_start + S (0) = S ((S (0)) * ff_v_eisenstein_local_sum_exists)) /\ exists ff_q_eisenstein_local_sum_exists_start. ff_u_eisenstein_local_sum_exists = ff_q_eisenstein_local_sum_exists_start * S ((S (0)) * ff_v_eisenstein_local_sum_exists) + (0))) /\ ((((exists ff_h_eisenstein_local_sum_exists_terminal. ff_h_eisenstein_local_sum_exists_terminal + S (Q) = S ((S (h)) * ff_v_eisenstein_local_sum_exists)) /\ exists ff_q_eisenstein_local_sum_exists_terminal. ff_u_eisenstein_local_sum_exists = ff_q_eisenstein_local_sum_exists_terminal * S ((S (h)) * ff_v_eisenstein_local_sum_exists) + (Q))) /\ forall ff_i_eisenstein_local_sum_exists. (exists ff_lt_eisenstein_local_sum_exists_bound. ff_lt_eisenstein_local_sum_exists_bound + S ff_i_eisenstein_local_sum_exists = h) -> exists ff_a_eisenstein_local_sum_exists ff_r_eisenstein_local_sum_exists ff_s_eisenstein_local_sum_exists. ((((exists ff_h_eisenstein_local_sum_exists_summand. ff_h_eisenstein_local_sum_exists_summand + S (ff_a_eisenstein_local_sum_exists) = S ((S (ff_i_eisenstein_local_sum_exists)) * x3)) /\ exists ff_q_eisenstein_local_sum_exists_summand. x2 = ff_q_eisenstein_local_sum_exists_summand * S ((S (ff_i_eisenstein_local_sum_exists)) * x3) + (ff_a_eisenstein_local_sum_exists))) /\ ((((exists ff_h_eisenstein_local_sum_exists_partial. ff_h_eisenstein_local_sum_exists_partial + S (ff_r_eisenstein_local_sum_exists) = S ((S (ff_i_eisenstein_local_sum_exists)) * ff_v_eisenstein_local_sum_exists)) /\ exists ff_q_eisenstein_local_sum_exists_partial. ff_u_eisenstein_local_sum_exists = ff_q_eisenstein_local_sum_exists_partial * S ((S (ff_i_eisenstein_local_sum_exists)) * ff_v_eisenstein_local_sum_exists) + (ff_r_eisenstein_local_sum_exists))) /\ ((((exists ff_h_eisenstein_local_sum_exists_successor. ff_h_eisenstein_local_sum_exists_successor + S (ff_s_eisenstein_local_sum_exists) = S ((S (S ff_i_eisenstein_local_sum_exists)) * ff_v_eisenstein_local_sum_exists)) /\ exists ff_q_eisenstein_local_sum_exists_successor. ff_u_eisenstein_local_sum_exists = ff_q_eisenstein_local_sum_exists_successor * S ((S (S ff_i_eisenstein_local_sum_exists)) * ff_v_eisenstein_local_sum_exists) + (ff_s_eisenstein_local_sum_exists))) /\ ff_s_eisenstein_local_sum_exists = ff_r_eisenstein_local_sum_exists + ff_a_eisenstein_local_sum_exists))))))
  27. 0027specialize beta_sum_exists x2
  28. 0028specialize beta_sum_exists x3
  29. 0029specialize beta_sum_exists h
  30. 0030exact beta_sum_exists
  31. 0031cases hsum_exists
  32. 0032exists x
  33. 0033exists x1
  34. 0034exists x2
  35. 0035exists x3
  36. 0036exists x4
  37. 0037exists x5
  38. 0038exists x6
  39. 0039split
  40. 0040exact hdivision_witness_witness_witness_witness_witness_witness_left
  41. 0041split
  42. 0042exact hdivision_witness_witness_witness_witness_witness_witness_right
  43. 0043exact hsum_exists_witness