PA00DV

eisenstein_initial_segment_decoded_choice

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

Every decoded bit recovers its exact threshold semantics.

Exact expanded PA statement

forall q b c k j bit. (forall eis_index_initial_segment_semantic_source. (exists eis_lt_gap_initial_segment_semantic_source_bound. eis_lt_gap_initial_segment_semantic_source_bound + S (eis_index_initial_segment_semantic_source) = k) -> exists eis_bit_initial_segment_semantic_source. ((((exists ff_h_eis_initial_segment_semantic_source_decoded. ff_h_eis_initial_segment_semantic_source_decoded + S (eis_bit_initial_segment_semantic_source) = S ((S (eis_index_initial_segment_semantic_source)) * c)) /\ exists ff_q_eis_initial_segment_semantic_source_decoded. b = ff_q_eis_initial_segment_semantic_source_decoded * S ((S (eis_index_initial_segment_semantic_source)) * c) + (eis_bit_initial_segment_semantic_source))) /\ (((eis_bit_initial_segment_semantic_source = 1 /\ (exists eis_le_gap_initial_segment_semantic_source_choice_inside. eis_le_gap_initial_segment_semantic_source_choice_inside + (S eis_index_initial_segment_semantic_source) = q)) \/ (eis_bit_initial_segment_semantic_source = 0 /\ (exists eis_lt_gap_initial_segment_semantic_source_choice_outside. eis_lt_gap_initial_segment_semantic_source_choice_outside + S (q) = S eis_index_initial_segment_semantic_source)))))) -> (exists eis_lt_gap_initial_segment_semantic_bound. eis_lt_gap_initial_segment_semantic_bound + S (j) = k) -> (((exists ff_h_initial_segment_semantic_entry. ff_h_initial_segment_semantic_entry + S (bit) = S ((S (j)) * c)) /\ exists ff_q_initial_segment_semantic_entry. b = ff_q_initial_segment_semantic_entry * S ((S (j)) * c) + (bit))) -> (((bit = 1 /\ (exists eis_le_gap_initial_segment_semantic_result_inside. eis_le_gap_initial_segment_semantic_result_inside + (S j) = q)) \/ (bit = 0 /\ (exists eis_lt_gap_initial_segment_semantic_result_outside. eis_lt_gap_initial_segment_semantic_result_outside + S (q) = S j))))

Structural proof guide

Generated structural guide

Every decoded bit recovers its exact threshold semantics.

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

PA00DX eisenstein_initial_segment_bit_count_functional

Formal native tactic body

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

  1. 0001intro q
  2. 0002intro b
  3. 0003intro c
  4. 0004intro k
  5. 0005intro j
  6. 0006intro bit
  7. 0007intro hprefix
  8. 0008intro hj
  9. 0009intro hentry
  10. 0010specialize hprefix j
  11. 0011have hstored : exists stored. ((((exists ff_h_initial_segment_semantic_stored. ff_h_initial_segment_semantic_stored + S (stored) = S ((S (j)) * c)) /\ exists ff_q_initial_segment_semantic_stored. b = ff_q_initial_segment_semantic_stored * S ((S (j)) * c) + (stored))) /\ (((stored = 1 /\ (exists eis_le_gap_initial_segment_semantic_stored_choice_inside. eis_le_gap_initial_segment_semantic_stored_choice_inside + (S j) = q)) \/ (stored = 0 /\ (exists eis_lt_gap_initial_segment_semantic_stored_choice_outside. eis_lt_gap_initial_segment_semantic_stored_choice_outside + S (q) = S j)))))
  12. 0012apply hprefix
  13. 0013exact hj
  14. 0014cases hstored
  15. 0015cases hstored_witness
  16. 0016have heq : x = bit
  17. 0017specialize beta_at_unique b
  18. 0018specialize beta_at_unique c
  19. 0019specialize beta_at_unique j
  20. 0020specialize beta_at_unique x
  21. 0021specialize beta_at_unique bit
  22. 0022apply beta_at_unique
  23. 0023exact hstored_witness_left
  24. 0024exact hentry
  25. 0025rewrite heq at hstored_witness_right
  26. 0026rewrite heq at hstored_witness_right
  27. 0027exact hstored_witness_right