BT00SD

eisenstein_initial_segment_indicator_choice

Alpha body-checked · checked-use disabled

Every position has a constructive exact threshold-indicator bit.

Exact expanded PA statement

forall q j. exists bit. (((bit = 1 /\ (exists eis_le_gap_initial_segment_point_inside. eis_le_gap_initial_segment_point_inside + (S j) = q)) \/ (bit = 0 /\ (exists eis_lt_gap_initial_segment_point_outside. eis_lt_gap_initial_segment_point_outside + S (q) = S j))))

Structural proof guide

Every position has a constructive exact threshold-indicator bit.

Direct prerequisites: le_or_lt. The authored body proceeds by case analysis (1).

Proof neighborhood

Direct dependencies

BT001G le_or_lt

Direct dependents

BT00SF eisenstein_initial_segment_prefix_exists

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro q
  2. 0002intro j
  3. 0003specialize le_or_lt (S j)
  4. 0004specialize le_or_lt q
  5. 0005cases le_or_lt
  6. 0006exists 1
  7. 0007left
  8. 0008split
  9. 0009refl
  10. 0010exact le_or_lt_left
  11. 0011exists 0
  12. 0012right
  13. 0013split
  14. 0014refl
  15. 0015exact le_or_lt_right