PA00ET

eisenstein_row_indicator_prefix_succ_restrict

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

A successor indicator row restricts to the same code's predecessor 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.

Exact expanded PA statement

forall p q i rb rc h sh. sh = S h -> (forall eri_column_fubini_row_restrict_source. (exists eri_gap_fubini_row_restrict_source_bound. eri_gap_fubini_row_restrict_source_bound + S (eri_column_fubini_row_restrict_source) = sh) -> exists eri_bit_fubini_row_restrict_source. ((((exists ff_h_eri_fubini_row_restrict_source_decoded. ff_h_eri_fubini_row_restrict_source_decoded + S (eri_bit_fubini_row_restrict_source) = S ((S (eri_column_fubini_row_restrict_source)) * rc)) /\ exists ff_q_eri_fubini_row_restrict_source_decoded. rb = ff_q_eri_fubini_row_restrict_source_decoded * S ((S (eri_column_fubini_row_restrict_source)) * rc) + (eri_bit_fubini_row_restrict_source))) /\ (((eri_bit_fubini_row_restrict_source = 0 /\ ((exists eri_gap_fubini_row_restrict_source_choice_left. eri_gap_fubini_row_restrict_source_choice_left + S (q * S i) = p * S eri_column_fubini_row_restrict_source) /\ ~(exists eri_gap_fubini_row_restrict_source_choice_right. eri_gap_fubini_row_restrict_source_choice_right + S (p * S eri_column_fubini_row_restrict_source) = q * S i))) \/ (eri_bit_fubini_row_restrict_source = 1 /\ ((exists eri_gap_fubini_row_restrict_source_choice_right. eri_gap_fubini_row_restrict_source_choice_right + S (p * S eri_column_fubini_row_restrict_source) = q * S i) /\ ~(exists eri_gap_fubini_row_restrict_source_choice_left. eri_gap_fubini_row_restrict_source_choice_left + S (q * S i) = p * S eri_column_fubini_row_restrict_source))))))) -> (forall eri_column_fubini_row_restrict_target. (exists eri_gap_fubini_row_restrict_target_bound. eri_gap_fubini_row_restrict_target_bound + S (eri_column_fubini_row_restrict_target) = h) -> exists eri_bit_fubini_row_restrict_target. ((((exists ff_h_eri_fubini_row_restrict_target_decoded. ff_h_eri_fubini_row_restrict_target_decoded + S (eri_bit_fubini_row_restrict_target) = S ((S (eri_column_fubini_row_restrict_target)) * rc)) /\ exists ff_q_eri_fubini_row_restrict_target_decoded. rb = ff_q_eri_fubini_row_restrict_target_decoded * S ((S (eri_column_fubini_row_restrict_target)) * rc) + (eri_bit_fubini_row_restrict_target))) /\ (((eri_bit_fubini_row_restrict_target = 0 /\ ((exists eri_gap_fubini_row_restrict_target_choice_left. eri_gap_fubini_row_restrict_target_choice_left + S (q * S i) = p * S eri_column_fubini_row_restrict_target) /\ ~(exists eri_gap_fubini_row_restrict_target_choice_right. eri_gap_fubini_row_restrict_target_choice_right + S (p * S eri_column_fubini_row_restrict_target) = q * S i))) \/ (eri_bit_fubini_row_restrict_target = 1 /\ ((exists eri_gap_fubini_row_restrict_target_choice_right. eri_gap_fubini_row_restrict_target_choice_right + S (p * S eri_column_fubini_row_restrict_target) = q * S i) /\ ~(exists eri_gap_fubini_row_restrict_target_choice_left. eri_gap_fubini_row_restrict_target_choice_left + S (q * S i) = p * S eri_column_fubini_row_restrict_target)))))))

Structural proof guide

Generated structural guide

A successor indicator row restricts to the same code's predecessor prefix.

Use the direct prerequisites le_succ as previously established PA formulas.

The proof proceeds by equality transport (1).

Referenced ingredients

PA002O le_succ

Proof neighborhood

Direct dependencies

PA002O le_succ

Direct dependents

PA00EU eisenstein_successor_row_count_decompose

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

18 script commands · 4 reading checkpoints · 0 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)
le succ
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro i
  4. L4
    intro rb
  5. L5
    intro rc
  6. L6
    intro h
  7. L7
    intro sh
  8. L8
    intro hsh
  9. L9
    intro hprefix
02Calculate and transport equalitiesL10–10

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

  1. L10
    rewrite hsh at hprefix
03Fix variables and assumptionsL11–12

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

  1. L11
    intro j
  2. L12
    intro hj
04Use earlier factsL13–18

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

  1. L13
    specialize hprefix j
  2. L14
    apply hprefix
  3. L15
    specialize le_succ (S j)
  4. L16
    specialize le_succ h
  5. L17
    apply le_succ
  6. L18
    exact hj

Library-wide reading audit

Original exact command ledger · 18 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro i
  4. 0004intro rb
  5. 0005intro rc
  6. 0006intro h
  7. 0007intro sh
  8. 0008intro hsh
  9. 0009intro hprefix
  10. 0010rewrite hsh at hprefix
  11. 0011intro j
  12. 0012intro hj
  13. 0013specialize hprefix j
  14. 0014apply hprefix
  15. 0015specialize le_succ (S j)
  16. 0016specialize le_succ h
  17. 0017apply le_succ
  18. 0018exact hj