PA00EA

eisenstein_row_indicator_decoded_choice

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

Every decoded row bit recovers its exact strict-orientation meaning.

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 l j bit. (forall eri_column_row_indicator_projection_prefix. (exists eri_gap_row_indicator_projection_prefix_bound. eri_gap_row_indicator_projection_prefix_bound + S (eri_column_row_indicator_projection_prefix) = l) -> exists eri_bit_row_indicator_projection_prefix. ((((exists ff_h_eri_row_indicator_projection_prefix_decoded. ff_h_eri_row_indicator_projection_prefix_decoded + S (eri_bit_row_indicator_projection_prefix) = S ((S (eri_column_row_indicator_projection_prefix)) * rc)) /\ exists ff_q_eri_row_indicator_projection_prefix_decoded. rb = ff_q_eri_row_indicator_projection_prefix_decoded * S ((S (eri_column_row_indicator_projection_prefix)) * rc) + (eri_bit_row_indicator_projection_prefix))) /\ (((eri_bit_row_indicator_projection_prefix = 0 /\ ((exists eri_gap_row_indicator_projection_prefix_choice_left. eri_gap_row_indicator_projection_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_projection_prefix) /\ ~(exists eri_gap_row_indicator_projection_prefix_choice_right. eri_gap_row_indicator_projection_prefix_choice_right + S (p * S eri_column_row_indicator_projection_prefix) = q * S i))) \/ (eri_bit_row_indicator_projection_prefix = 1 /\ ((exists eri_gap_row_indicator_projection_prefix_choice_right. eri_gap_row_indicator_projection_prefix_choice_right + S (p * S eri_column_row_indicator_projection_prefix) = q * S i) /\ ~(exists eri_gap_row_indicator_projection_prefix_choice_left. eri_gap_row_indicator_projection_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_projection_prefix))))))) -> (exists eri_gap_row_indicator_projection_bound. eri_gap_row_indicator_projection_bound + S (j) = l) -> (((exists ff_h_row_indicator_projection_entry. ff_h_row_indicator_projection_entry + S (bit) = S ((S (j)) * rc)) /\ exists ff_q_row_indicator_projection_entry. rb = ff_q_row_indicator_projection_entry * S ((S (j)) * rc) + (bit))) -> (((bit = 0 /\ ((exists eri_gap_row_indicator_projection_choice_left. eri_gap_row_indicator_projection_choice_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_row_indicator_projection_choice_right. eri_gap_row_indicator_projection_choice_right + S (p * S j) = q * S i))) \/ (bit = 1 /\ ((exists eri_gap_row_indicator_projection_choice_right. eri_gap_row_indicator_projection_choice_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_row_indicator_projection_choice_left. eri_gap_row_indicator_projection_choice_left + S (q * S i) = p * S j)))))

Structural proof guide

Generated structural guide

Every decoded row bit recovers its exact strict-orientation meaning.

Use the direct prerequisites beta_at_unique as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (2), equality transport (2).

Referenced ingredients

PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA002F beta_at_unique

Direct dependents

PA00EB eisenstein_transposed_column_prefix_all_bits PA00EC eisenstein_transposed_decoded_cell_bits_complementary PA00F4 eisenstein_transposed_column_decoded_choice PA00F9 eisenstein_successor_terminal_bit_matches_last_column

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

29 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)
beta at unique

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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 l
  7. L7
    intro j
  8. L8
    intro bit
  9. L9
    intro hprefix
  10. L10
    intro hj
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hentry
03Establish hstoredL12–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.

  1. L12
    have hstored : ∃ stored. BetaAt(rb,rc,j,stored) ∧ (stored = 0 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i)) ∨ stored = 1 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j)))Definitions: LtBetaAt
  2. L13
    specialize hprefix j
  3. L14
    apply hprefix
  4. L15
    exact hj
04Separate the logical casesL16–17

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

  1. L16
    cases hstored
  2. L17
    cases hstored_witness
05Establish heqL18–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L18
    have heq : x = bit
  2. L19
    specialize beta_at_unique rb
  3. L20
    specialize beta_at_unique rc
  4. L21
    specialize beta_at_unique j
  5. L22
    specialize beta_at_unique x
  6. L23
    specialize beta_at_unique bit
  7. L24
    apply beta_at_unique
  8. L25
    exact hstored_witness_left
  9. L26
    exact hentry
  10. L27
    rewrite heq at hstored_witness_right
06Calculate and transport equalitiesL28–28

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

  1. L28
    rewrite heq at hstored_witness_right
07Use earlier factsL29–29

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

  1. L29
    exact hstored_witness_right

Library-wide reading audit

Original exact command ledger · 29 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro i
  4. 0004intro rb
  5. 0005intro rc
  6. 0006intro l
  7. 0007intro j
  8. 0008intro bit
  9. 0009intro hprefix
  10. 0010intro hj
  11. 0011intro hentry
  12. 0012have hstored : exists stored. ((((exists ff_h_row_indicator_projection_stored. ff_h_row_indicator_projection_stored + S (stored) = S ((S (j)) * rc)) /\ exists ff_q_row_indicator_projection_stored. rb = ff_q_row_indicator_projection_stored * S ((S (j)) * rc) + (stored))) /\ (((stored = 0 /\ ((exists eri_gap_row_indicator_projection_stored_choice_left. eri_gap_row_indicator_projection_stored_choice_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_row_indicator_projection_stored_choice_right. eri_gap_row_indicator_projection_stored_choice_right + S (p * S j) = q * S i))) \/ (stored = 1 /\ ((exists eri_gap_row_indicator_projection_stored_choice_right. eri_gap_row_indicator_projection_stored_choice_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_row_indicator_projection_stored_choice_left. eri_gap_row_indicator_projection_stored_choice_left + S (q * S i) = p * S j))))))
  13. 0013specialize hprefix j
  14. 0014apply hprefix
  15. 0015exact hj
  16. 0016cases hstored
  17. 0017cases hstored_witness
  18. 0018have heq : x = bit
  19. 0019specialize beta_at_unique rb
  20. 0020specialize beta_at_unique rc
  21. 0021specialize beta_at_unique j
  22. 0022specialize beta_at_unique x
  23. 0023specialize beta_at_unique bit
  24. 0024apply beta_at_unique
  25. 0025exact hstored_witness_left
  26. 0026exact hentry
  27. 0027rewrite heq at hstored_witness_right
  28. 0028rewrite heq at hstored_witness_right
  29. 0029exact hstored_witness_right