TS000C

prime_is_not_natural_square

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

No natural square satisfies the nonunit factor-pair definition of primality.

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 first-order arithmetic statement

forall p s. ((~(p = 1) /\ forall frm_prime_left_ftsp_prime frm_prime_right_ftsp_prime. p = frm_prime_left_ftsp_prime * frm_prime_right_ftsp_prime -> frm_prime_left_ftsp_prime = 1 \/ frm_prime_right_ftsp_prime = 1)) -> ~(p = s * s)

Constructive proof overview

Generated structural guide

No natural square satisfies the nonunit factor-pair definition of primality.

The unchanged tactic script uses 0 declared prerequisites and contains 21 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

none

Direct dependents

TS000E prime_floor_square_strictly_below_prime

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

21 script commands · 8 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.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro p
  2. L2
    intro s
  3. L3
    intro hprime
  4. L4
    intro hsquare
02Separate the logical casesL5–5

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

  1. L5
    cases hprime
03Establish hfactorL6–10

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

  1. L6
    have hfactor : s = 1 \/ s = 1
  2. L7
    specialize hprime_right s
  3. L8
    specialize hprime_right s
  4. L9
    apply hprime_right
  5. L10
    exact hsquare
04Separate the logical casesL11–11

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

  1. L11
    cases hfactor
05Use earlier factsL12–12

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

  1. L12
    apply hprime_left
06Calculate and transport equalitiesL13–16

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L13
    rewrite hsquare
  2. L14
    rewrite hfactor_left
  3. L15
    rewrite hfactor_left
  4. L16
    norm_num
07Use earlier factsL17–17

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

  1. L17
    apply hprime_left
08Calculate and transport equalitiesL18–21

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L18
    rewrite hsquare
  2. L19
    rewrite hfactor_right
  3. L20
    rewrite hfactor_right
  4. L21
    norm_num

Library-wide reading audit

Original exact command ledger · 21 lines
  1. 0001intro p
  2. 0002intro s
  3. 0003intro hprime
  4. 0004intro hsquare
  5. 0005cases hprime
  6. 0006have hfactor : s = 1 \/ s = 1
  7. 0007specialize hprime_right s
  8. 0008specialize hprime_right s
  9. 0009apply hprime_right
  10. 0010exact hsquare
  11. 0011cases hfactor
  12. 0012apply hprime_left
  13. 0013rewrite hsquare
  14. 0014rewrite hfactor_left
  15. 0015rewrite hfactor_left
  16. 0016norm_num
  17. 0017apply hprime_left
  18. 0018rewrite hsquare
  19. 0019rewrite hfactor_right
  20. 0020rewrite hfactor_right
  21. 0021norm_num