PA00AO · theorem

inverse_prefix_zero_fixed

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

The zero index, representing residue one, 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,0,0)

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 PD0008 ModEq 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_zero_prefix. (exists wip_gap_zero_prefix_prefix_bound. wip_gap_zero_prefix_prefix_bound + S wip_index_zero_prefix = n) -> exists wip_mate_zero_prefix. ((((exists wip_beta_height_zero_prefix_decoded. wip_beta_height_zero_prefix_decoded + S (wip_mate_zero_prefix) = S ((S (wip_index_zero_prefix)) * c)) /\ exists wip_beta_quotient_zero_prefix_decoded. b = wip_beta_quotient_zero_prefix_decoded * S ((S (wip_index_zero_prefix)) * c) + (wip_mate_zero_prefix))) /\ ((exists wip_gap_zero_prefix_inverse_index_bound. wip_gap_zero_prefix_inverse_index_bound + S wip_index_zero_prefix = n) /\ ((exists wip_gap_zero_prefix_inverse_mate_bound. wip_gap_zero_prefix_inverse_mate_bound + S wip_mate_zero_prefix = n) /\ (exists wip_mod_left_zero_prefix_inverse_mod wip_mod_right_zero_prefix_inverse_mod. ((S wip_index_zero_prefix) * S wip_mate_zero_prefix) + p * wip_mod_left_zero_prefix_inverse_mod = 1 + p * wip_mod_right_zero_prefix_inverse_mod))))) -> (((exists wie_beta_height_zero_result. wie_beta_height_zero_result + S (0) = S ((S (0)) * c)) /\ exists wie_beta_quotient_zero_result. b = wie_beta_quotient_zero_result * S ((S (0)) * c) + (0)))

Proof neighborhood

Direct theorem prerequisites

PA0023 mod_eq_refl PA000M one_mul 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)
mod eq reflone mulinverse 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 hzero_boundL9–10

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

  1. L9
    have hzero_bound : Lt(0,n)Definitions: Lt(0,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 k
04Calculate and transport equalitiesL12–14

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

  1. L12
    rewrite PA4
  2. L13
    rewrite PA3
  3. L14
    refl
05Establish hzero_reflL15–18

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

  1. L15
    have hzero_refl : ModEq(p,1,1)Definitions: ModEq(p,1,1)Original native command in the exact edition
  2. L16
    specialize mod_eq_refl p
  3. L17
    specialize mod_eq_refl 1
  4. L18
    exact mod_eq_refl
06Establish hzero_modL19–22

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

  1. L19
    have hzero_mod : SuccessorInverse(p,0,0)Definitions: SuccessorInverse(p,0,0)Original native command in the exact edition
  2. L20
    specialize one_mul 1
  3. L21
    rewrite one_mul
  4. L22
    exact hzero_refl
07Establish hzero_relationL23–23

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

  1. L23
    have hzero_relation : InverseIndex(p,n,0,0)Definitions: InverseIndex(p,n,0,0)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 hzero_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 hzero_bound
  2. L28
    exact hzero_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 0
  9. L35
    specialize inverse_prefix_extensional 0
  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 hzero_bound
  4. L40
    exact hzero_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 hzero_bound : Lt(0,n)
    Exact native replay linehave hzero_bound : exists wie_strict_gap_zero_bound. wie_strict_gap_zero_bound + S 0 = n
  10. 0010rewrite hnk
  11. 0011exists k
  12. 0012rewrite PA4
  13. 0013rewrite PA3
  14. 0014refl
  15. 0015have hzero_refl : ModEq(p,1,1)
    Exact native replay linehave hzero_refl : exists wie_mod_left_zero_refl wie_mod_right_zero_refl. (1) + p * wie_mod_left_zero_refl = (1) + p * wie_mod_right_zero_refl
  16. 0016specialize mod_eq_refl p
  17. 0017specialize mod_eq_refl 1
  18. 0018exact mod_eq_refl
  19. 0019have hzero_mod : SuccessorInverse(p,0,0)
    Exact native replay linehave hzero_mod : exists wie_mod_left_zero wie_mod_right_zero. ((S 0) * S 0) + p * wie_mod_left_zero = (1) + p * wie_mod_right_zero
  20. 0020specialize one_mul 1
  21. 0021rewrite one_mul
  22. 0022exact hzero_refl
  23. 0023have hzero_relation : InverseIndex(p,n,0,0)
    Exact native replay linehave hzero_relation : (exists wie_strict_gap_zero_relation_index_bound. wie_strict_gap_zero_relation_index_bound + S 0 = n) /\ ((exists wie_strict_gap_zero_relation_mate_bound. wie_strict_gap_zero_relation_mate_bound + S 0 = n) /\ (exists wie_mod_left_zero_relation_mod wie_mod_right_zero_relation_mod. ((S 0) * S 0) + p * wie_mod_left_zero_relation_mod = (1) + p * wie_mod_right_zero_relation_mod))
  24. 0024split
  25. 0025exact hzero_bound
  26. 0026split
  27. 0027exact hzero_bound
  28. 0028exact hzero_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 0
  35. 0035specialize inverse_prefix_extensional 0
  36. 0036apply inverse_prefix_extensional
  37. 0037exact hpn
  38. 0038exact hprefix
  39. 0039exact hzero_bound
  40. 0040exact hzero_relation