PA00DE · theorem

eisenstein_row_indicator_prefix_all_bits

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

The beta-coded indicator projection contains only zero and one.

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. (∀ 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)))) → AllBits(rb,rc,l)

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 PD0016 AllBits

7 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

11 occurrences

Exact expanded native-PA statement
forall p q i rb rc l. (forall eri_column_row_indicator_bits_prefix. (exists eri_gap_row_indicator_bits_prefix_bound. eri_gap_row_indicator_bits_prefix_bound + S (eri_column_row_indicator_bits_prefix) = l) -> exists eri_bit_row_indicator_bits_prefix. ((((exists ff_h_eri_row_indicator_bits_prefix_decoded. ff_h_eri_row_indicator_bits_prefix_decoded + S (eri_bit_row_indicator_bits_prefix) = S ((S (eri_column_row_indicator_bits_prefix)) * rc)) /\ exists ff_q_eri_row_indicator_bits_prefix_decoded. rb = ff_q_eri_row_indicator_bits_prefix_decoded * S ((S (eri_column_row_indicator_bits_prefix)) * rc) + (eri_bit_row_indicator_bits_prefix))) /\ (((eri_bit_row_indicator_bits_prefix = 0 /\ ((exists eri_gap_row_indicator_bits_prefix_choice_left. eri_gap_row_indicator_bits_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_bits_prefix) /\ ~(exists eri_gap_row_indicator_bits_prefix_choice_right. eri_gap_row_indicator_bits_prefix_choice_right + S (p * S eri_column_row_indicator_bits_prefix) = q * S i))) \/ (eri_bit_row_indicator_bits_prefix = 1 /\ ((exists eri_gap_row_indicator_bits_prefix_choice_right. eri_gap_row_indicator_bits_prefix_choice_right + S (p * S eri_column_row_indicator_bits_prefix) = q * S i) /\ ~(exists eri_gap_row_indicator_bits_prefix_choice_left. eri_gap_row_indicator_bits_prefix_choice_left + S (q * S i) = p * S eri_column_row_indicator_bits_prefix))))))) -> (forall ff_i_row_indicator_all_bits. (exists ff_lt_row_indicator_all_bits_bound. ff_lt_row_indicator_all_bits_bound + S ff_i_row_indicator_all_bits = l) -> exists ff_bit_row_indicator_all_bits. ((((exists ff_h_row_indicator_all_bits_decoded. ff_h_row_indicator_all_bits_decoded + S (ff_bit_row_indicator_all_bits) = S ((S (ff_i_row_indicator_all_bits)) * rc)) /\ exists ff_q_row_indicator_all_bits_decoded. rb = ff_q_row_indicator_all_bits_decoded * S ((S (ff_i_row_indicator_all_bits)) * rc) + (ff_bit_row_indicator_all_bits))) /\ (ff_bit_row_indicator_all_bits = 0 \/ ff_bit_row_indicator_all_bits = 1)))

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

PA00DF distinct_odd_prime_half_row_count_exists

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

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

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 l
  7. L7
    intro hprefix
  8. L8
    intro j
  9. L9
    intro hj
02Establish hentryL10–12

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

  1. L10
    have hentry : ∀ eri_column_row_indicator_bits_entry_source. Lt(eri_column_row_indicator_bits_entry_source,l) → ∃ x. BetaAt(rb,rc,eri_column_row_indicator_bits_entry_source,x) ∧ (x = 0 ∧ (Lt(q · S i,p · S eri_column_row_indicator_bits_entry_source) ∧ ¬Lt(p · S eri_column_row_indicator_bits_entry_source,q · S i)) ∨ x = 1 ∧ (Lt(p · S eri_column_row_indicator_bits_entry_source,q · S i) ∧ ¬Lt(q · S i,p · S eri_column_row_indicator_bits_entry_source)))Definitions: Lt(eri_column_row_indicator_bits_entry_source,l)BetaAt(rb,rc,eri_column_row_indicator_bits_entry_source,x)Lt(q · S i,p · S eri_column_row_indicator_bits_entry_source)Lt(p · S eri_column_row_indicator_bits_entry_source,q · S i)Original native command in the exact edition
  2. L11
    exact hprefix
  3. L12
    specialize hentry j
03Establish hstoredL13–15

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

  1. L13
    have hstored : ∃ bit. 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)))Definitions: BetaAt(rb,rc,j,bit)Lt(q · S i,p · S j)Lt(p · S j,q · S i)Original native command in the exact edition
  2. L14
    apply hentry
  3. 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
05Construct an explicit witnessL18–18

Supply the displayed value, then prove that it has the required property.

  1. L18
    exists x
06Separate the logical casesL19–19

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

  1. L19
    split
07Use earlier factsL20–20

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

  1. L20
    exact hstored_witness_left
08Separate the logical casesL21–23

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

  1. L21
    cases hstored_witness_right
  2. L22
    cases hstored_witness_right_left
  3. L23
    left
09Use earlier factsL24–24

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

  1. L24
    exact hstored_witness_right_left_left
10Separate the logical casesL25–26

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

  1. L25
    cases hstored_witness_right_right
  2. L26
    right
11Use earlier factsL27–27

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

  1. L27
    exact hstored_witness_right_right_left

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro i
  4. 0004intro rb
  5. 0005intro rc
  6. 0006intro l
  7. 0007intro hprefix
  8. 0008intro j
  9. 0009intro hj
  10. 0010have hentry : ∀ eri_column_row_indicator_bits_entry_source. Lt(eri_column_row_indicator_bits_entry_source,l) → ∃ x. BetaAt(rb,rc,eri_column_row_indicator_bits_entry_source,x) ∧ (x = 0 ∧ (Lt(q · S i,p · S eri_column_row_indicator_bits_entry_source) ∧ ¬Lt(p · S eri_column_row_indicator_bits_entry_source,q · S i)) ∨ x = 1 ∧ (Lt(p · S eri_column_row_indicator_bits_entry_source,q · S i) ∧ ¬Lt(q · S i,p · S eri_column_row_indicator_bits_entry_source)))
    Exact native replay linehave hentry : forall eri_column_row_indicator_bits_entry_source. (exists eri_gap_row_indicator_bits_entry_source_bound. eri_gap_row_indicator_bits_entry_source_bound + S (eri_column_row_indicator_bits_entry_source) = l) -> exists eri_bit_row_indicator_bits_entry_source. ((((exists ff_h_eri_row_indicator_bits_entry_source_decoded. ff_h_eri_row_indicator_bits_entry_source_decoded + S (eri_bit_row_indicator_bits_entry_source) = S ((S (eri_column_row_indicator_bits_entry_source)) * rc)) /\ exists ff_q_eri_row_indicator_bits_entry_source_decoded. rb = ff_q_eri_row_indicator_bits_entry_source_decoded * S ((S (eri_column_row_indicator_bits_entry_source)) * rc) + (eri_bit_row_indicator_bits_entry_source))) /\ (((eri_bit_row_indicator_bits_entry_source = 0 /\ ((exists eri_gap_row_indicator_bits_entry_source_choice_left. eri_gap_row_indicator_bits_entry_source_choice_left + S (q * S i) = p * S eri_column_row_indicator_bits_entry_source) /\ ~(exists eri_gap_row_indicator_bits_entry_source_choice_right. eri_gap_row_indicator_bits_entry_source_choice_right + S (p * S eri_column_row_indicator_bits_entry_source) = q * S i))) \/ (eri_bit_row_indicator_bits_entry_source = 1 /\ ((exists eri_gap_row_indicator_bits_entry_source_choice_right. eri_gap_row_indicator_bits_entry_source_choice_right + S (p * S eri_column_row_indicator_bits_entry_source) = q * S i) /\ ~(exists eri_gap_row_indicator_bits_entry_source_choice_left. eri_gap_row_indicator_bits_entry_source_choice_left + S (q * S i) = p * S eri_column_row_indicator_bits_entry_source))))))
  11. 0011exact hprefix
  12. 0012specialize hentry j
  13. 0013have hstored : ∃ bit. 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)))
    Exact native replay linehave hstored : exists bit. ((((exists ff_h_row_indicator_bits_stored. ff_h_row_indicator_bits_stored + S (bit) = S ((S (j)) * rc)) /\ exists ff_q_row_indicator_bits_stored. rb = ff_q_row_indicator_bits_stored * S ((S (j)) * rc) + (bit))) /\ (((bit = 0 /\ ((exists eri_gap_row_indicator_bits_choice_left. eri_gap_row_indicator_bits_choice_left + S (q * S i) = p * S j) /\ ~(exists eri_gap_row_indicator_bits_choice_right. eri_gap_row_indicator_bits_choice_right + S (p * S j) = q * S i))) \/ (bit = 1 /\ ((exists eri_gap_row_indicator_bits_choice_right. eri_gap_row_indicator_bits_choice_right + S (p * S j) = q * S i) /\ ~(exists eri_gap_row_indicator_bits_choice_left. eri_gap_row_indicator_bits_choice_left + S (q * S i) = p * S j))))))
  14. 0014apply hentry
  15. 0015exact hj
  16. 0016cases hstored
  17. 0017cases hstored_witness
  18. 0018exists x
  19. 0019split
  20. 0020exact hstored_witness_left
  21. 0021cases hstored_witness_right
  22. 0022cases hstored_witness_right_left
  23. 0023left
  24. 0024exact hstored_witness_right_left_left
  25. 0025cases hstored_witness_right_right
  26. 0026right
  27. 0027exact hstored_witness_right_right_left