PA00AI · theorem

prime_inverse_prefix_nonendpoint_not_fixed

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

A decoded inverse entry from a nonendpoint source is not fixed.

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. ∀ n. ∀ b. ∀ c. ∀ i. ∀ j. p = S n → Prime(p) → InversePrefix(p,n,b,c,n) → Lt(i,n) → BetaAt(b,c,i,j) → ¬i = 0 ∧ ¬S i = n → ¬i = j

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 PD0037 InversePrefix

4 occurrences

In local proof propositions

PD0013 BetaAt

1 occurrences

Exact expanded native-PA statement
forall p n b c i j. p = S n -> ((~(p = 1) /\ forall wip_prime_left_orbit_prime wip_prime_right_orbit_prime. p = wip_prime_left_orbit_prime * wip_prime_right_orbit_prime -> wip_prime_left_orbit_prime = 1 \/ wip_prime_right_orbit_prime = 1)) -> (forall wip_index_orbit_prefix. (exists wip_gap_orbit_prefix_prefix_bound. wip_gap_orbit_prefix_prefix_bound + S wip_index_orbit_prefix = n) -> exists wip_mate_orbit_prefix. ((((exists wip_beta_height_orbit_prefix_decoded. wip_beta_height_orbit_prefix_decoded + S (wip_mate_orbit_prefix) = S ((S (wip_index_orbit_prefix)) * c)) /\ exists wip_beta_quotient_orbit_prefix_decoded. b = wip_beta_quotient_orbit_prefix_decoded * S ((S (wip_index_orbit_prefix)) * c) + (wip_mate_orbit_prefix))) /\ ((exists wip_gap_orbit_prefix_inverse_index_bound. wip_gap_orbit_prefix_inverse_index_bound + S wip_index_orbit_prefix = n) /\ ((exists wip_gap_orbit_prefix_inverse_mate_bound. wip_gap_orbit_prefix_inverse_mate_bound + S wip_mate_orbit_prefix = n) /\ (exists wip_mod_left_orbit_prefix_inverse_mod wip_mod_right_orbit_prefix_inverse_mod. ((S wip_index_orbit_prefix) * S wip_mate_orbit_prefix) + p * wip_mod_left_orbit_prefix_inverse_mod = 1 + p * wip_mod_right_orbit_prefix_inverse_mod))))) -> (exists wip_gap_orbit_source_bound. wip_gap_orbit_source_bound + S i = n) -> (((exists wip_beta_height_orbit_source_entry. wip_beta_height_orbit_source_entry + S (j) = S ((S (i)) * c)) /\ exists wip_beta_quotient_orbit_source_entry. b = wip_beta_quotient_orbit_source_entry * S ((S (i)) * c) + (j))) -> ((~(i = 0) /\ ~((S i) = n))) -> ~(i = j)

Proof neighborhood

Direct theorem prerequisites

PA00AH prime_inverse_prefix_fixed_cases

Direct theorem dependents

PA00AQ prime_inverse_prefix_nonendpoint_mate PA00AR prime_choose_unused_nonendpoint_orbit

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

35 script commands · 9 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 (1)
prime inverse prefix fixed cases
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro i
  6. L6
    intro j
  7. L7
    intro hpn
  8. L8
    intro hp
  9. L9
    intro hprefix
  10. L10
    intro hi
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hat
  2. L12
    intro hnonendpoint
03Separate the logical casesL13–13

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

  1. L13
    cases hnonendpoint
04Fix variables and assumptionsL14–14

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

  1. L14
    intro heq
05Establish hfixedL15–18

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

  1. L15
    have hfixed : BetaAt(b,c,i,i)Definitions: BetaAt(b,c,i,i)Original native command in the exact edition
  2. L16
    rewrite <- heq at hat
  3. L17
    rewrite <- heq at hat
  4. L18
    exact hat
06Establish hcasesL19–28

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

  1. L19
    have hcases : i = 0 \/ S i = n
  2. L20
    specialize prime_inverse_prefix_fixed_cases p
  3. L21
    specialize prime_inverse_prefix_fixed_cases n
  4. L22
    specialize prime_inverse_prefix_fixed_cases b
  5. L23
    specialize prime_inverse_prefix_fixed_cases c
  6. L24
    specialize prime_inverse_prefix_fixed_cases i
  7. L25
    apply prime_inverse_prefix_fixed_cases
  8. L26
    exact hpn
  9. L27
    exact hp
  10. L28
    exact hprefix
07Use earlier factsL29–30

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

  1. L29
    exact hi
  2. L30
    exact hfixed
08Separate the logical casesL31–31

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

  1. L31
    cases hcases
09Use earlier factsL32–35

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

  1. L32
    apply hnonendpoint_left
  2. L33
    exact hcases_left
  3. L34
    apply hnonendpoint_right
  4. L35
    exact hcases_right

Library-wide reading audit

Original defined command ledger · 35 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro b
  4. 0004intro c
  5. 0005intro i
  6. 0006intro j
  7. 0007intro hpn
  8. 0008intro hp
  9. 0009intro hprefix
  10. 0010intro hi
  11. 0011intro hat
  12. 0012intro hnonendpoint
  13. 0013cases hnonendpoint
  14. 0014intro heq
  15. 0015have hfixed : BetaAt(b,c,i,i)
    Exact native replay linehave hfixed : ((exists wip_beta_height_orbit_source_fixed. wip_beta_height_orbit_source_fixed + S (i) = S ((S (i)) * c)) /\ exists wip_beta_quotient_orbit_source_fixed. b = wip_beta_quotient_orbit_source_fixed * S ((S (i)) * c) + (i))
  16. 0016rewrite <- heq at hat
  17. 0017rewrite <- heq at hat
  18. 0018exact hat
  19. 0019have hcases : i = 0 \/ S i = n
  20. 0020specialize prime_inverse_prefix_fixed_cases p
  21. 0021specialize prime_inverse_prefix_fixed_cases n
  22. 0022specialize prime_inverse_prefix_fixed_cases b
  23. 0023specialize prime_inverse_prefix_fixed_cases c
  24. 0024specialize prime_inverse_prefix_fixed_cases i
  25. 0025apply prime_inverse_prefix_fixed_cases
  26. 0026exact hpn
  27. 0027exact hp
  28. 0028exact hprefix
  29. 0029exact hi
  30. 0030exact hfixed
  31. 0031cases hcases
  32. 0032apply hnonendpoint_left
  33. 0033exact hcases_left
  34. 0034apply hnonendpoint_right
  35. 0035exact hcases_right