PG0006

polynomial_zero_extended_shift_reverse

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

Conversely every zero-extended value of an actual shift is the original zero-extended value; this is not formal polynomial equality.

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

forall b c L d e i a. (((forall mdr_i_pfp_shift_pad_reverse_relationprefix mdr_a_pfp_shift_pad_reverse_relationprefix. (exists mdr_gap_pfp_shift_pad_reverse_relationprefixb. mdr_gap_pfp_shift_pad_reverse_relationprefixb + S (mdr_i_pfp_shift_pad_reverse_relationprefix) = (L)) -> (((exists ff_h_mdr_pfp_shift_pad_reverse_relationprefixo. ff_h_mdr_pfp_shift_pad_reverse_relationprefixo + S (mdr_a_pfp_shift_pad_reverse_relationprefix) = S ((S (mdr_i_pfp_shift_pad_reverse_relationprefix)) * c)) /\ exists ff_q_mdr_pfp_shift_pad_reverse_relationprefixo. b = ff_q_mdr_pfp_shift_pad_reverse_relationprefixo * S ((S (mdr_i_pfp_shift_pad_reverse_relationprefix)) * c) + (mdr_a_pfp_shift_pad_reverse_relationprefix))) -> (((exists ff_h_mdr_pfp_shift_pad_reverse_relationprefixn. ff_h_mdr_pfp_shift_pad_reverse_relationprefixn + S (mdr_a_pfp_shift_pad_reverse_relationprefix) = S ((S (mdr_i_pfp_shift_pad_reverse_relationprefix)) * e)) /\ exists ff_q_mdr_pfp_shift_pad_reverse_relationprefixn. d = ff_q_mdr_pfp_shift_pad_reverse_relationprefixn * S ((S (mdr_i_pfp_shift_pad_reverse_relationprefix)) * e) + (mdr_a_pfp_shift_pad_reverse_relationprefix)))) /\ ((((exists ff_h_pfp_shift_pad_reverse_relationlast. ff_h_pfp_shift_pad_reverse_relationlast + S (0) = S ((S (L)) * e)) /\ exists ff_q_pfp_shift_pad_reverse_relationlast. d = ff_q_pfp_shift_pad_reverse_relationlast * S ((S (L)) * e) + (0)))))) -> ((((exists pfa_gap_shift_pad_reverse_sourceinside. pfa_gap_shift_pad_reverse_sourceinside + S (i) = (S L)) /\ ((((exists ff_h_pfp_shift_pad_reverse_sourceentry. ff_h_pfp_shift_pad_reverse_sourceentry + S (a) = S ((S (i)) * e)) /\ exists ff_q_pfp_shift_pad_reverse_sourceentry. d = ff_q_pfp_shift_pad_reverse_sourceentry * S ((S (i)) * e) + (a)))))) \/ (((exists pfc_gap_shift_pad_reverse_sourceoutside. pfc_gap_shift_pad_reverse_sourceoutside+(S L)=(i)) /\ (((a)=0))))) -> ((((exists pfa_gap_shift_pad_reverse_resultinside. pfa_gap_shift_pad_reverse_resultinside + S (i) = (L)) /\ ((((exists ff_h_pfp_shift_pad_reverse_resultentry. ff_h_pfp_shift_pad_reverse_resultentry + S (a) = S ((S (i)) * c)) /\ exists ff_q_pfp_shift_pad_reverse_resultentry. b = ff_q_pfp_shift_pad_reverse_resultentry * S ((S (i)) * c) + (a)))))) \/ (((exists pfc_gap_shift_pad_reverse_resultoutside. pfc_gap_shift_pad_reverse_resultoutside+(L)=(i)) /\ (((a)=0)))))

Constructive proof overview

Generated structural guide

Conversely every zero-extended value of an actual shift is the original zero-extended value; this is not formal polynomial equality.

The unchanged tactic script uses 3 declared prerequisites and contains 39 exact native proof lines.

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

Proof neighborhood

Direct dependencies

polynomial_zero_extended_entry_exists Alpha theorem; checked-use authorized polynomial_zero_extended_entry_functional Alpha theorem; checked-use authorized PG0005 polynomial_zero_extended_shift_forward

Direct dependents

PG0007 polynomial_diagonal_term_shift_right_iff

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

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

Named ingredients (1)
polynomial zero extended shift forward
01Fix variables and assumptionsL1–9

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro L
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro i
  7. L7
    intro a
  8. L8
    intro hs
  9. L9
    intro ha
02Establish hxL10–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial zero extended entry exists.

  1. L10
    have hx : exists x. ((((exists pfa_gap_shift_pad_reverse_choseninside. pfa_gap_shift_pad_reverse_choseninside + S (i) = (L)) /\ ((((exists ff_h_pfp_shift_pad_reverse_chosenentry. ff_h_pfp_shift_pad_reverse_chosenentry + S (x) = S ((S (i)) * c)) /\ exists ff_q_pfp_shift_pad_reverse_chosenentry. b = ff_q_pfp_shift_pad_reverse_chosenentry * S ((S (i)) * c) + (x)))))) \/ (((exists pfc_gap_shift_pad_reverse_chosenoutside. pfc_gap_shift_pad_reverse_chosenoutside+(L)=(i)) /\ (((x)=0)))))
  2. L11
    specialize polynomial_zero_extended_entry_exists (b)
  3. L12
    specialize polynomial_zero_extended_entry_exists (c)
  4. L13
    specialize polynomial_zero_extended_entry_exists (L)
  5. L14
    specialize polynomial_zero_extended_entry_exists (i)
  6. L15
    apply polynomial_zero_extended_entry_exists
03Separate the logical casesL16–16

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

  1. L16
    cases hx
04Establish heqL17–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial zero extended entry functional.

  1. L17
    have heq : a=x
  2. L18
    specialize polynomial_zero_extended_entry_functional (d)
  3. L19
    specialize polynomial_zero_extended_entry_functional (e)
  4. L20
    specialize polynomial_zero_extended_entry_functional (S L)
  5. L21
    specialize polynomial_zero_extended_entry_functional (i)
  6. L22
    specialize polynomial_zero_extended_entry_functional (a)
  7. L23
    specialize polynomial_zero_extended_entry_functional (x)
  8. L24
    apply polynomial_zero_extended_entry_functional
  9. L25
    exact ha
  10. L26
    specialize polynomial_zero_extended_shift_forward (b)
05Use earlier factsL27–35

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

  1. L27
    specialize polynomial_zero_extended_shift_forward (c)
  2. L28
    specialize polynomial_zero_extended_shift_forward (L)
  3. L29
    specialize polynomial_zero_extended_shift_forward (d)
  4. L30
    specialize polynomial_zero_extended_shift_forward (e)
  5. L31
    specialize polynomial_zero_extended_shift_forward (i)
  6. L32
    specialize polynomial_zero_extended_shift_forward (x)
  7. L33
    apply polynomial_zero_extended_shift_forward
  8. L34
    exact hs
  9. L35
    exact hx_witness
06Calculate and transport equalitiesL36–38

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

  1. L36
    rewrite heq
  2. L37
    rewrite heq
  3. L38
    rewrite heq
07Use earlier factsL39–39

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

  1. L39
    exact hx_witness

Library-wide reading audit

Original exact command ledger · 39 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro L
  4. 0004intro d
  5. 0005intro e
  6. 0006intro i
  7. 0007intro a
  8. 0008intro hs
  9. 0009intro ha
  10. 0010have hx : exists x. ((((exists pfa_gap_shift_pad_reverse_choseninside. pfa_gap_shift_pad_reverse_choseninside + S (i) = (L)) /\ ((((exists ff_h_pfp_shift_pad_reverse_chosenentry. ff_h_pfp_shift_pad_reverse_chosenentry + S (x) = S ((S (i)) * c)) /\ exists ff_q_pfp_shift_pad_reverse_chosenentry. b = ff_q_pfp_shift_pad_reverse_chosenentry * S ((S (i)) * c) + (x)))))) \/ (((exists pfc_gap_shift_pad_reverse_chosenoutside. pfc_gap_shift_pad_reverse_chosenoutside+(L)=(i)) /\ (((x)=0)))))
  11. 0011specialize polynomial_zero_extended_entry_exists (b)
  12. 0012specialize polynomial_zero_extended_entry_exists (c)
  13. 0013specialize polynomial_zero_extended_entry_exists (L)
  14. 0014specialize polynomial_zero_extended_entry_exists (i)
  15. 0015apply polynomial_zero_extended_entry_exists
  16. 0016cases hx
  17. 0017have heq : a=x
  18. 0018specialize polynomial_zero_extended_entry_functional (d)
  19. 0019specialize polynomial_zero_extended_entry_functional (e)
  20. 0020specialize polynomial_zero_extended_entry_functional (S L)
  21. 0021specialize polynomial_zero_extended_entry_functional (i)
  22. 0022specialize polynomial_zero_extended_entry_functional (a)
  23. 0023specialize polynomial_zero_extended_entry_functional (x)
  24. 0024apply polynomial_zero_extended_entry_functional
  25. 0025exact ha
  26. 0026specialize polynomial_zero_extended_shift_forward (b)
  27. 0027specialize polynomial_zero_extended_shift_forward (c)
  28. 0028specialize polynomial_zero_extended_shift_forward (L)
  29. 0029specialize polynomial_zero_extended_shift_forward (d)
  30. 0030specialize polynomial_zero_extended_shift_forward (e)
  31. 0031specialize polynomial_zero_extended_shift_forward (i)
  32. 0032specialize polynomial_zero_extended_shift_forward (x)
  33. 0033apply polynomial_zero_extended_shift_forward
  34. 0034exact hs
  35. 0035exact hx_witness
  36. 0036rewrite heq
  37. 0037rewrite heq
  38. 0038rewrite heq
  39. 0039exact hx_witness