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 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
Every decoded bit recovers its exact threshold semantics.
Direct prerequisites: beta_at_unique. The authored body proceeds by case analysis (2), intermediate claims (2), equality transport (2).
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.
Read the argument
Proof checkpoints
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.
Named ingredients (1)
01Fix variables and assumptionsL1–9
02Use earlier factsL10–10
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L10
specialize hprefix j
03Establish hstoredL11–13
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.
- L11
have 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))))) - L12
apply hprefix - L13
exact hj
04Separate the logical casesL14–15
05Establish heqL16–25
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
06Calculate and transport equalitiesL26–26
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L26
rewrite heq at hstored_witness_right
07Use earlier factsL27–27
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L27
exact hstored_witness_right
Original exact command ledger · 27 lines
- 0001
intro q - 0002
intro b - 0003
intro c - 0004
intro k - 0005
intro j - 0006
intro bit - 0007
intro hprefix - 0008
intro hj - 0009
intro hentry - 0010
specialize hprefix j - 0011
have 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))))) - 0012
apply hprefix - 0013
exact hj - 0014
cases hstored - 0015
cases hstored_witness - 0016
have heq : x = bit - 0017
specialize beta_at_unique b - 0018
specialize beta_at_unique c - 0019
specialize beta_at_unique j - 0020
specialize beta_at_unique x - 0021
specialize beta_at_unique bit - 0022
apply beta_at_unique - 0023
exact hstored_witness_left - 0024
exact hentry - 0025
rewrite heq at hstored_witness_right - 0026
rewrite heq at hstored_witness_right - 0027
exact hstored_witness_right