PA00AP · theorem

inverse_prefix_last_fixed

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

The last index, representing the predecessor of p, is fixed by the full inverse prefix.

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. ∀ k. ∀ b. ∀ c. p = S n → n = S k → InversePrefix(p,n,b,c,n) → BetaAt(b,c,k,k)

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

PD0013 BetaAt PD0037 InversePrefix

2 occurrences

In local proof propositions

PD0002 Lt PD0031 BalancedInverse PD0035 SuccessorInverse PD0036 InverseIndex

4 occurrences

Exact expanded native-PA statement
forall p n k b c. p = S n -> n = S k -> (forall wip_index_last_prefix. (exists wip_gap_last_prefix_prefix_bound. wip_gap_last_prefix_prefix_bound + S wip_index_last_prefix = n) -> exists wip_mate_last_prefix. ((((exists wip_beta_height_last_prefix_decoded. wip_beta_height_last_prefix_decoded + S (wip_mate_last_prefix) = S ((S (wip_index_last_prefix)) * c)) /\ exists wip_beta_quotient_last_prefix_decoded. b = wip_beta_quotient_last_prefix_decoded * S ((S (wip_index_last_prefix)) * c) + (wip_mate_last_prefix))) /\ ((exists wip_gap_last_prefix_inverse_index_bound. wip_gap_last_prefix_inverse_index_bound + S wip_index_last_prefix = n) /\ ((exists wip_gap_last_prefix_inverse_mate_bound. wip_gap_last_prefix_inverse_mate_bound + S wip_mate_last_prefix = n) /\ (exists wip_mod_left_last_prefix_inverse_mod wip_mod_right_last_prefix_inverse_mod. ((S wip_index_last_prefix) * S wip_mate_last_prefix) + p * wip_mod_left_last_prefix_inverse_mod = 1 + p * wip_mod_right_last_prefix_inverse_mod))))) -> (((exists wip_beta_height_last_result. wip_beta_height_last_result + S (k) = S ((S (k)) * c)) /\ exists wip_beta_quotient_last_result. b = wip_beta_quotient_last_result * S ((S (k)) * c) + (k)))

Proof neighborhood

Direct theorem prerequisites

PA0001 zero_add PA005D predecessor_square_mod_one PA00AM inverse_prefix_extensional

Direct theorem dependents

PA00AQ prime_inverse_prefix_nonendpoint_mate

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

40 script commands · 12 reading checkpoints · 4 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 (3)
zero addpredecessor square mod oneinverse prefix extensional
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro k
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro hpn
  7. L7
    intro hnk
  8. L8
    intro hprefix
02Establish hlast_boundL9–10

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

  1. L9
    have hlast_bound : Lt(k,n)Definitions: Lt(k,n)Original native command in the exact edition
  2. L10
    rewrite hnk
03Construct an explicit witnessL11–11

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

  1. L11
    exists 0
04Use earlier factsL12–13

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

  1. L12
    specialize zero_add (S k)
  2. L13
    exact zero_add
05Establish hpredecessor_modL14–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply predecessor square mod one.

  1. L14
    have hpredecessor_mod : BalancedInverse(p,n,n)Definitions: BalancedInverse(p,n,n)Original native command in the exact edition
  2. L15
    specialize predecessor_square_mod_one p
  3. L16
    specialize predecessor_square_mod_one n
  4. L17
    apply predecessor_square_mod_one
  5. L18
    exact hpn
06Establish hlast_modL19–22

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

  1. L19
    have hlast_mod : SuccessorInverse(p,k,k)Definitions: SuccessorInverse(p,k,k)Original native command in the exact edition
  2. L20
    rewrite <- hnk
  3. L21
    rewrite <- hnk
  4. L22
    exact hpredecessor_mod
07Establish hlast_relationL23–23

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

  1. L23
    have hlast_relation : InverseIndex(p,n,k,k)Definitions: InverseIndex(p,n,k,k)Original native command in the exact edition
08Separate the logical casesL24–24

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

  1. L24
    split
09Use earlier factsL25–25

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

  1. L25
    exact hlast_bound
10Separate the logical casesL26–26

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

  1. L26
    split
11Use earlier factsL27–36

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

  1. L27
    exact hlast_bound
  2. L28
    exact hlast_mod
  3. L29
    specialize inverse_prefix_extensional p
  4. L30
    specialize inverse_prefix_extensional n
  5. L31
    specialize inverse_prefix_extensional b
  6. L32
    specialize inverse_prefix_extensional c
  7. L33
    specialize inverse_prefix_extensional n
  8. L34
    specialize inverse_prefix_extensional k
  9. L35
    specialize inverse_prefix_extensional k
  10. L36
    apply inverse_prefix_extensional
12Use earlier factsL37–40

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

  1. L37
    exact hpn
  2. L38
    exact hprefix
  3. L39
    exact hlast_bound
  4. L40
    exact hlast_relation

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro k
  4. 0004intro b
  5. 0005intro c
  6. 0006intro hpn
  7. 0007intro hnk
  8. 0008intro hprefix
  9. 0009have hlast_bound : Lt(k,n)
    Exact native replay linehave hlast_bound : exists wip_gap_last_bound. wip_gap_last_bound + S k = n
  10. 0010rewrite hnk
  11. 0011exists 0
  12. 0012specialize zero_add (S k)
  13. 0013exact zero_add
  14. 0014have hpredecessor_mod : BalancedInverse(p,n,n)
    Exact native replay linehave hpredecessor_mod : exists wie_mod_left_predecessor wie_mod_right_predecessor. (n * n) + p * wie_mod_left_predecessor = (1) + p * wie_mod_right_predecessor
  15. 0015specialize predecessor_square_mod_one p
  16. 0016specialize predecessor_square_mod_one n
  17. 0017apply predecessor_square_mod_one
  18. 0018exact hpn
  19. 0019have hlast_mod : SuccessorInverse(p,k,k)
    Exact native replay linehave hlast_mod : exists wie_mod_left_last wie_mod_right_last. ((S k) * S k) + p * wie_mod_left_last = (1) + p * wie_mod_right_last
  20. 0020rewrite <- hnk
  21. 0021rewrite <- hnk
  22. 0022exact hpredecessor_mod
  23. 0023have hlast_relation : InverseIndex(p,n,k,k)
    Exact native replay linehave hlast_relation : (exists wip_gap_last_relation_index_bound. wip_gap_last_relation_index_bound + S k = n) /\ ((exists wip_gap_last_relation_mate_bound. wip_gap_last_relation_mate_bound + S k = n) /\ (exists wip_mod_left_last_relation_mod wip_mod_right_last_relation_mod. ((S k) * S k) + p * wip_mod_left_last_relation_mod = 1 + p * wip_mod_right_last_relation_mod))
  24. 0024split
  25. 0025exact hlast_bound
  26. 0026split
  27. 0027exact hlast_bound
  28. 0028exact hlast_mod
  29. 0029specialize inverse_prefix_extensional p
  30. 0030specialize inverse_prefix_extensional n
  31. 0031specialize inverse_prefix_extensional b
  32. 0032specialize inverse_prefix_extensional c
  33. 0033specialize inverse_prefix_extensional n
  34. 0034specialize inverse_prefix_extensional k
  35. 0035specialize inverse_prefix_extensional k
  36. 0036apply inverse_prefix_extensional
  37. 0037exact hpn
  38. 0038exact hprefix
  39. 0039exact hlast_bound
  40. 0040exact hlast_relation