PA00EA · theorem

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.

Statement with defined notation

∀ p. ∀ q. ∀ i. ∀ rb. ∀ rc. ∀ l. ∀ j. ∀ bit. (∀ x. Lt(x,l) → ∃ y. BetaAt(rb,rc,x,y) ∧ (y = 0 ∧ (Lt(q · S i,p · S x) ∧ ¬Lt(p · S x,q · S i)) ∨ y = 1 ∧ (Lt(p · S x,q · S i) ∧ ¬Lt(q · S i,p · S x)))) → Lt(j,l) → BetaAt(rb,rc,j,bit) → bit = 0 ∧ (Lt(q · S i,p · S j) ∧ ¬Lt(p · S j,q · S i)) ∨ bit = 1 ∧ (Lt(p · S j,q · S i) ∧ ¬Lt(q · S i,p · S j))

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

PD0002 Lt PD0013 BetaAt

12 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

5 occurrences

Exact expanded native-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)))))

Proof neighborhood

Direct theorem prerequisites

PA002F beta_at_unique

Direct theorem 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

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

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.

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 (1)
beta at unique
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: BetaAt(rb,rc,j,stored)Lt(q · S i,p · S j)Lt(p · S j,q · S i)Original native command in the exact edition
  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 defined 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 : ∃ 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)))
    Exact native replay linehave 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