BT00YH

floor_sqrt_above_root_power_two_strict

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

A prime above a floor root has square strictly above the value.

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 x s p t. (((exists bcs_sqrt_lower_gap_bfsarpts_source. bcs_sqrt_lower_gap_bfsarpts_source + (s) * (s) = (x)) /\ exists bcs_sqrt_upper_gap_bfsarpts_source. bcs_sqrt_upper_gap_bfsarpts_source + S (x) = S (s) * S (s))) -> (exists bcf_lt_gap_bfsarpts_above. bcf_lt_gap_bfsarpts_above + S (s) = p) -> (exists bpvi_b_bfsarpts_power bpvi_c_bfsarpts_power. ((forall bpvi_i_bfsarpts_power. (exists bpvi_repeat_gap_bfsarpts_power. bpvi_repeat_gap_bfsarpts_power + S bpvi_i_bfsarpts_power = 2) -> (((exists bpvi_h_bfsarpts_power_repeat. bpvi_h_bfsarpts_power_repeat + S (p) = S ((S (bpvi_i_bfsarpts_power)) * bpvi_c_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_repeat. bpvi_b_bfsarpts_power = bpvi_q_bfsarpts_power_repeat * S ((S (bpvi_i_bfsarpts_power)) * bpvi_c_bfsarpts_power) + (p)))) /\ (exists bpvi_u_bfsarpts_power bpvi_v_bfsarpts_power. ((((exists bpvi_h_bfsarpts_power_start. bpvi_h_bfsarpts_power_start + S (1) = S ((S (0)) * bpvi_v_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_start. bpvi_u_bfsarpts_power = bpvi_q_bfsarpts_power_start * S ((S (0)) * bpvi_v_bfsarpts_power) + (1))) /\ ((((exists bpvi_h_bfsarpts_power_terminal. bpvi_h_bfsarpts_power_terminal + S (t) = S ((S (2)) * bpvi_v_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_terminal. bpvi_u_bfsarpts_power = bpvi_q_bfsarpts_power_terminal * S ((S (2)) * bpvi_v_bfsarpts_power) + (t))) /\ forall bpvi_j_bfsarpts_power. (exists bpvi_product_gap_bfsarpts_power. bpvi_product_gap_bfsarpts_power + S bpvi_j_bfsarpts_power = 2) -> exists bpvi_factor_bfsarpts_power bpvi_partial_bfsarpts_power bpvi_successor_bfsarpts_power. ((((exists bpvi_h_bfsarpts_power_factor. bpvi_h_bfsarpts_power_factor + S (bpvi_factor_bfsarpts_power) = S ((S (bpvi_j_bfsarpts_power)) * bpvi_c_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_factor. bpvi_b_bfsarpts_power = bpvi_q_bfsarpts_power_factor * S ((S (bpvi_j_bfsarpts_power)) * bpvi_c_bfsarpts_power) + (bpvi_factor_bfsarpts_power))) /\ ((((exists bpvi_h_bfsarpts_power_partial. bpvi_h_bfsarpts_power_partial + S (bpvi_partial_bfsarpts_power) = S ((S (bpvi_j_bfsarpts_power)) * bpvi_v_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_partial. bpvi_u_bfsarpts_power = bpvi_q_bfsarpts_power_partial * S ((S (bpvi_j_bfsarpts_power)) * bpvi_v_bfsarpts_power) + (bpvi_partial_bfsarpts_power))) /\ ((((exists bpvi_h_bfsarpts_power_successor. bpvi_h_bfsarpts_power_successor + S (bpvi_successor_bfsarpts_power) = S ((S (S bpvi_j_bfsarpts_power)) * bpvi_v_bfsarpts_power)) /\ exists bpvi_q_bfsarpts_power_successor. bpvi_u_bfsarpts_power = bpvi_q_bfsarpts_power_successor * S ((S (S bpvi_j_bfsarpts_power)) * bpvi_v_bfsarpts_power) + (bpvi_successor_bfsarpts_power))) /\ bpvi_successor_bfsarpts_power = bpvi_partial_bfsarpts_power * bpvi_factor_bfsarpts_power)))))))) -> (exists bcf_lt_gap_bfsarpts_result. bcf_lt_gap_bfsarpts_result + S (x) = t)

Structural proof guide

A prime above a floor root has square strictly above the value.

Direct prerequisites: mul_le_mul_right, mul_le_mul_left, le_trans, lt_of_lt_of_le, pow_two. The authored body proceeds by case analysis (1), intermediate claims (5), equality transport (1).

Proof neighborhood

Direct dependencies

BT001M mul_le_mul_right BT001L mul_le_mul_left BT000F le_trans BT001D lt_of_lt_of_le BT009W pow_two

Direct dependents

BT00YI central_binom_prime_above_floor_sqrt_valuation_le_one

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

43 script commands · 7 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)
mul le mul rightmul le mul leftle translt of lt of lepow two
01Fix variables and assumptionsL1–7

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

  1. L1
    intro x
  2. L2
    intro s
  3. L3
    intro p
  4. L4
    intro t
  5. L5
    intro hfloor
  6. L6
    intro habove
  7. L7
    intro hpower
02Separate the logical casesL8–8

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

  1. L8
    cases hfloor
03Establish hfirstL9–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul right.

  1. L9
    have hfirst : exists bcf_le_gap_bfsarpts_first. bcf_le_gap_bfsarpts_first + (S s * S s) = p * S s
  2. L10
    specialize mul_le_mul_right (S s)
  3. L11
    specialize mul_le_mul_right p
  4. L12
    specialize mul_le_mul_right (S s)
  5. L13
    apply mul_le_mul_right
  6. L14
    exact habove
04Establish hsecondL15–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul left.

  1. L15
    have hsecond : exists bcf_le_gap_bfsarpts_second. bcf_le_gap_bfsarpts_second + (p * S s) = p * p
  2. L16
    specialize mul_le_mul_left (S s)
  3. L17
    specialize mul_le_mul_left p
  4. L18
    specialize mul_le_mul_left p
  5. L19
    apply mul_le_mul_left
  6. L20
    exact habove
05Establish hsquareL21–27

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

  1. L21
    have hsquare : exists bcf_le_gap_bfsarpts_square. bcf_le_gap_bfsarpts_square + (S s * S s) = p * p
  2. L22
    specialize le_trans (S s * S s)
  3. L23
    specialize le_trans (p * S s)
  4. L24
    specialize le_trans (p * p)
  5. L25
    apply le_trans
  6. L26
    exact hfirst
  7. L27
    exact hsecond
06Establish hrawL28–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply lt of lt of le.

  1. L28
    have hraw : exists bcf_lt_gap_bfsarpts_raw_result. bcf_lt_gap_bfsarpts_raw_result + S (x) = p * p
  2. L29
    specialize lt_of_lt_of_le x
  3. L30
    specialize lt_of_lt_of_le (S s * S s)
  4. L31
    specialize lt_of_lt_of_le (p * p)
  5. L32
    apply lt_of_lt_of_le
  6. L33
    exact hfloor_right
  7. L34
    exact hsquare
07Establish hvalueL35–43

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

  1. L35
    have hvalue : t = p * p
  2. L36
    specialize pow_two p
  3. L37
    specialize pow_two 2
  4. L38
    specialize pow_two t
  5. L39
    apply pow_two
  6. L40
    refl
  7. L41
    exact hpower
  8. L42
    rewrite hvalue
  9. L43
    exact hraw

Library-wide reading audit

Original exact command ledger · 43 lines
  1. 0001intro x
  2. 0002intro s
  3. 0003intro p
  4. 0004intro t
  5. 0005intro hfloor
  6. 0006intro habove
  7. 0007intro hpower
  8. 0008cases hfloor
  9. 0009have hfirst : exists bcf_le_gap_bfsarpts_first. bcf_le_gap_bfsarpts_first + (S s * S s) = p * S s
  10. 0010specialize mul_le_mul_right (S s)
  11. 0011specialize mul_le_mul_right p
  12. 0012specialize mul_le_mul_right (S s)
  13. 0013apply mul_le_mul_right
  14. 0014exact habove
  15. 0015have hsecond : exists bcf_le_gap_bfsarpts_second. bcf_le_gap_bfsarpts_second + (p * S s) = p * p
  16. 0016specialize mul_le_mul_left (S s)
  17. 0017specialize mul_le_mul_left p
  18. 0018specialize mul_le_mul_left p
  19. 0019apply mul_le_mul_left
  20. 0020exact habove
  21. 0021have hsquare : exists bcf_le_gap_bfsarpts_square. bcf_le_gap_bfsarpts_square + (S s * S s) = p * p
  22. 0022specialize le_trans (S s * S s)
  23. 0023specialize le_trans (p * S s)
  24. 0024specialize le_trans (p * p)
  25. 0025apply le_trans
  26. 0026exact hfirst
  27. 0027exact hsecond
  28. 0028have hraw : exists bcf_lt_gap_bfsarpts_raw_result. bcf_lt_gap_bfsarpts_raw_result + S (x) = p * p
  29. 0029specialize lt_of_lt_of_le x
  30. 0030specialize lt_of_lt_of_le (S s * S s)
  31. 0031specialize lt_of_lt_of_le (p * p)
  32. 0032apply lt_of_lt_of_le
  33. 0033exact hfloor_right
  34. 0034exact hsquare
  35. 0035have hvalue : t = p * p
  36. 0036specialize pow_two p
  37. 0037specialize pow_two 2
  38. 0038specialize pow_two t
  39. 0039apply pow_two
  40. 0040refl
  41. 0041exact hpower
  42. 0042rewrite hvalue
  43. 0043exact hraw