PA00DE

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.

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

Structural proof guide

Generated structural guide

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

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

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

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA00DF distinct_odd_prime_half_row_count_exists

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

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.

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–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: LtBetaAt
  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: LtBetaAt
  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 exact 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 : 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 : 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