PA0083

prime_half_range_product_coprime

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

The canonical half-range product is coprime to its odd prime modulus.

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 P. p = 2 * h + 1 -> ((~(p = 1) /\ forall frp_prime_left_gauss_composition_prime frp_prime_right_gauss_composition_prime. p = frp_prime_left_gauss_composition_prime * frp_prime_right_gauss_composition_prime -> frp_prime_left_gauss_composition_prime = 1 \/ frp_prime_right_gauss_composition_prime = 1)) -> (forall gsp_range_index_gauss_composition_half_range. (exists gsp_lt_gap_gauss_composition_half_range_range_bound. gsp_lt_gap_gauss_composition_half_range_range_bound + S gsp_range_index_gauss_composition_half_range = h) -> (((exists gsp_beta_height_gauss_composition_half_range_range_entry. gsp_beta_height_gauss_composition_half_range_range_entry + S (1 + gsp_range_index_gauss_composition_half_range) = S ((S (gsp_range_index_gauss_composition_half_range)) * c)) /\ exists gsp_beta_quotient_gauss_composition_half_range_range_entry. b = gsp_beta_quotient_gauss_composition_half_range_range_entry * S ((S (gsp_range_index_gauss_composition_half_range)) * c) + (1 + gsp_range_index_gauss_composition_half_range)))) -> (exists ff_u_gauss_composition_canonical_product ff_v_gauss_composition_canonical_product. ((((exists ff_h_gauss_composition_canonical_product_start. ff_h_gauss_composition_canonical_product_start + S (1) = S ((S (0)) * ff_v_gauss_composition_canonical_product)) /\ exists ff_q_gauss_composition_canonical_product_start. ff_u_gauss_composition_canonical_product = ff_q_gauss_composition_canonical_product_start * S ((S (0)) * ff_v_gauss_composition_canonical_product) + (1))) /\ ((((exists ff_h_gauss_composition_canonical_product_terminal. ff_h_gauss_composition_canonical_product_terminal + S (P) = S ((S (h)) * ff_v_gauss_composition_canonical_product)) /\ exists ff_q_gauss_composition_canonical_product_terminal. ff_u_gauss_composition_canonical_product = ff_q_gauss_composition_canonical_product_terminal * S ((S (h)) * ff_v_gauss_composition_canonical_product) + (P))) /\ forall ff_i_gauss_composition_canonical_product. (exists ff_lt_gauss_composition_canonical_product_bound. ff_lt_gauss_composition_canonical_product_bound + S ff_i_gauss_composition_canonical_product = h) -> exists ff_p_gauss_composition_canonical_product ff_r_gauss_composition_canonical_product ff_s_gauss_composition_canonical_product. ((((exists ff_h_gauss_composition_canonical_product_factor. ff_h_gauss_composition_canonical_product_factor + S (ff_p_gauss_composition_canonical_product) = S ((S (ff_i_gauss_composition_canonical_product)) * c)) /\ exists ff_q_gauss_composition_canonical_product_factor. b = ff_q_gauss_composition_canonical_product_factor * S ((S (ff_i_gauss_composition_canonical_product)) * c) + (ff_p_gauss_composition_canonical_product))) /\ ((((exists ff_h_gauss_composition_canonical_product_partial. ff_h_gauss_composition_canonical_product_partial + S (ff_r_gauss_composition_canonical_product) = S ((S (ff_i_gauss_composition_canonical_product)) * ff_v_gauss_composition_canonical_product)) /\ exists ff_q_gauss_composition_canonical_product_partial. ff_u_gauss_composition_canonical_product = ff_q_gauss_composition_canonical_product_partial * S ((S (ff_i_gauss_composition_canonical_product)) * ff_v_gauss_composition_canonical_product) + (ff_r_gauss_composition_canonical_product))) /\ ((((exists ff_h_gauss_composition_canonical_product_successor. ff_h_gauss_composition_canonical_product_successor + S (ff_s_gauss_composition_canonical_product) = S ((S (S ff_i_gauss_composition_canonical_product)) * ff_v_gauss_composition_canonical_product)) /\ exists ff_q_gauss_composition_canonical_product_successor. ff_u_gauss_composition_canonical_product = ff_q_gauss_composition_canonical_product_successor * S ((S (S ff_i_gauss_composition_canonical_product)) * ff_v_gauss_composition_canonical_product) + (ff_s_gauss_composition_canonical_product))) /\ ff_s_gauss_composition_canonical_product = ff_r_gauss_composition_canonical_product * ff_p_gauss_composition_canonical_product)))))) -> (forall frp_divisor_gauss_composition_canonical_coprime. (exists frp_left_factor_gauss_composition_canonical_coprime. P = frp_divisor_gauss_composition_canonical_coprime * frp_left_factor_gauss_composition_canonical_coprime) -> (exists frp_right_factor_gauss_composition_canonical_coprime. p = frp_divisor_gauss_composition_canonical_coprime * frp_right_factor_gauss_composition_canonical_coprime) -> frp_divisor_gauss_composition_canonical_coprime = 1)

Structural proof guide

Generated structural guide

The canonical half-range product is coprime to its odd prime modulus.

Use the direct prerequisites beta_half_range_entry_bounds, prime_positive_bounded_product_coprime as previously established PA formulas.

The proof proceeds by intermediate claims (1).

Referenced ingredients

PA0034 beta_half_range_entry_bounds PA0082 prime_positive_bounded_product_coprime

Proof neighborhood

Direct dependencies

PA0034 beta_half_range_entry_bounds PA0082 prime_positive_bounded_product_coprime

Direct dependents

PA0084 gauss_signed_products_cancel_mod

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

34 script commands · 4 reading checkpoints · 1 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 (2)
beta half range entry boundsprime positive bounded product coprime

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–9

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 P
  6. L6
    intro hp
  7. L7
    intro hprime
  8. L8
    intro hhalf
  9. L9
    intro hproduct
02Establish hboundsL10–19

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

  1. L10
    have hbounds : ∀ fppc_index_gauss_composition_bounds. ∀ fppc_factor_gauss_composition_bounds. Lt(fppc_index_gauss_composition_bounds,h) → BetaAt(b,c,fppc_index_gauss_composition_bounds,fppc_factor_gauss_composition_bounds) → UnitResidue(p,fppc_factor_gauss_composition_bounds)Definitions: LtBetaAtUnitResidue
  2. L11
    intro i
  3. L12
    intro x
  4. L13
    intro hi
  5. L14
    intro hx
  6. L15
    specialize beta_half_range_entry_bounds p
  7. L16
    specialize beta_half_range_entry_bounds h
  8. L17
    specialize beta_half_range_entry_bounds b
  9. L18
    specialize beta_half_range_entry_bounds c
  10. L19
    specialize beta_half_range_entry_bounds i
03Use earlier factsL20–29

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

  1. L20
    specialize beta_half_range_entry_bounds x
  2. L21
    apply beta_half_range_entry_bounds
  3. L22
    exact hp
  4. L23
    exact hhalf
  5. L24
    exact hi
  6. L25
    exact hx
  7. L26
    specialize prime_positive_bounded_product_coprime p
  8. L27
    specialize prime_positive_bounded_product_coprime b
  9. L28
    specialize prime_positive_bounded_product_coprime c
  10. L29
    specialize prime_positive_bounded_product_coprime h
04Use earlier factsL30–34

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

  1. L30
    specialize prime_positive_bounded_product_coprime P
  2. L31
    apply prime_positive_bounded_product_coprime
  3. L32
    exact hprime
  4. L33
    exact hbounds
  5. L34
    exact hproduct

Library-wide reading audit

Original exact command ledger · 34 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro b
  4. 0004intro c
  5. 0005intro P
  6. 0006intro hp
  7. 0007intro hprime
  8. 0008intro hhalf
  9. 0009intro hproduct
  10. 0010have hbounds : forall fppc_index_gauss_composition_bounds fppc_factor_gauss_composition_bounds. (exists frp_gap_gauss_composition_bounds_index_bound. frp_gap_gauss_composition_bounds_index_bound + S fppc_index_gauss_composition_bounds = h) -> (((exists ff_h_fppc_gauss_composition_bounds_decoded. ff_h_fppc_gauss_composition_bounds_decoded + S (fppc_factor_gauss_composition_bounds) = S ((S (fppc_index_gauss_composition_bounds)) * c)) /\ exists ff_q_fppc_gauss_composition_bounds_decoded. b = ff_q_fppc_gauss_composition_bounds_decoded * S ((S (fppc_index_gauss_composition_bounds)) * c) + (fppc_factor_gauss_composition_bounds))) -> (~(fppc_factor_gauss_composition_bounds = 0) /\ (exists frp_gap_gauss_composition_bounds_factor_bound. frp_gap_gauss_composition_bounds_factor_bound + S fppc_factor_gauss_composition_bounds = p))
  11. 0011intro i
  12. 0012intro x
  13. 0013intro hi
  14. 0014intro hx
  15. 0015specialize beta_half_range_entry_bounds p
  16. 0016specialize beta_half_range_entry_bounds h
  17. 0017specialize beta_half_range_entry_bounds b
  18. 0018specialize beta_half_range_entry_bounds c
  19. 0019specialize beta_half_range_entry_bounds i
  20. 0020specialize beta_half_range_entry_bounds x
  21. 0021apply beta_half_range_entry_bounds
  22. 0022exact hp
  23. 0023exact hhalf
  24. 0024exact hi
  25. 0025exact hx
  26. 0026specialize prime_positive_bounded_product_coprime p
  27. 0027specialize prime_positive_bounded_product_coprime b
  28. 0028specialize prime_positive_bounded_product_coprime c
  29. 0029specialize prime_positive_bounded_product_coprime h
  30. 0030specialize prime_positive_bounded_product_coprime P
  31. 0031apply prime_positive_bounded_product_coprime
  32. 0032exact hprime
  33. 0033exact hbounds
  34. 0034exact hproduct