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. ∀ a. ∀ n. ∀ u. ∀ v. ∀ b. ∀ c. ∀ f. ∀ g. ∀ h. n = h + h → ScaledInversePrefix(p,a,n,u,v,n) → (∀ x. Lt(x,h + h) → ∃ y. BetaAt(b,c,x,y) ∧ Lt(y,n)) → (∀ x. Lt(x,h) → ∃ y. ∃ z. BetaAt(b,c,x + x,y) ∧ (BetaAt(b,c,S (x + x),z) ∧ BetaAt(u,v,y,S z))) → (∀ x. ∀ y. Lt(x,n) → BetaAt(b,c,x,y) → BetaAt(f,g,x,S y)) → ∀ x. ∀ y. ∀ z. Lt(x,h) → BetaAt(f,g,x + x,y) → BetaAt(f,g,S (x + x),z) → ModEq(p,y · z,a)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
15 occurrences
In local proof propositions
14 occurrences
Exact expanded native-PA statement
forall p a n u v b c f g h. n = h + h -> (forall esip_index_enr_prefix. (exists esip_gap_enr_prefix_prefix_bound. esip_gap_enr_prefix_prefix_bound + S (esip_index_enr_prefix) = n) -> exists esip_mate_enr_prefix. ((((exists ff_h_esip_enr_prefix_entry. ff_h_esip_enr_prefix_entry + S (esip_mate_enr_prefix) = S ((S (esip_index_enr_prefix)) * v)) /\ exists ff_q_esip_enr_prefix_entry. u = ff_q_esip_enr_prefix_entry * S ((S (esip_index_enr_prefix)) * v) + (esip_mate_enr_prefix))) /\ ((exists esip_gap_enr_prefix_relation_index_bound. esip_gap_enr_prefix_relation_index_bound + S (esip_index_enr_prefix) = n) /\ ((((~((S esip_index_enr_prefix) = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_left_bound. esip_gap_enr_prefix_relation_scaled_left_bound + S (S esip_index_enr_prefix) = p))) /\ (((~(esip_mate_enr_prefix = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_right_bound. esip_gap_enr_prefix_relation_scaled_right_bound + S (esip_mate_enr_prefix) = p))) /\ (exists esi_mod_left_enr_prefix_relation_scaled_mod esi_mod_right_enr_prefix_relation_scaled_mod. ((S esip_index_enr_prefix) * esip_mate_enr_prefix) + p * esi_mod_left_enr_prefix_relation_scaled_mod = (a) + p * esi_mod_right_enr_prefix_relation_scaled_mod))))))) -> (forall fom_index_enr_raw_bounded. (exists fom_gap_enr_raw_bounded_index_bound. fom_gap_enr_raw_bounded_index_bound + S (fom_index_enr_raw_bounded) = h + h) -> exists fom_value_enr_raw_bounded. ((((exists fom_beta_height_enr_raw_bounded_entry. fom_beta_height_enr_raw_bounded_entry + S (fom_value_enr_raw_bounded) = S ((S (fom_index_enr_raw_bounded)) * c)) /\ exists fom_beta_quotient_enr_raw_bounded_entry. b = fom_beta_quotient_enr_raw_bounded_entry * S ((S (fom_index_enr_raw_bounded)) * c) + (fom_value_enr_raw_bounded))) /\ (exists fom_gap_enr_raw_bounded_value_bound. fom_gap_enr_raw_bounded_value_bound + S (fom_value_enr_raw_bounded) = n))) -> (forall espi_pair_enr_history. (exists wpo_gap_enr_history_pair_bound. wpo_gap_enr_history_pair_bound + S (espi_pair_enr_history) = h) -> exists espi_left_enr_history espi_right_enr_history. (((((exists wpo_beta_height_enr_history_left_entry. wpo_beta_height_enr_history_left_entry + S (espi_left_enr_history) = S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c)) /\ exists wpo_beta_quotient_enr_history_left_entry. b = wpo_beta_quotient_enr_history_left_entry * S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c) + (espi_left_enr_history))) /\ (((((exists wpo_beta_height_enr_history_right_entry. wpo_beta_height_enr_history_right_entry + S (espi_right_enr_history) = S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c)) /\ exists wpo_beta_quotient_enr_history_right_entry. b = wpo_beta_quotient_enr_history_right_entry * S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c) + (espi_right_enr_history))) /\ (((exists wpo_beta_height_enr_history_scaled_edge. wpo_beta_height_enr_history_scaled_edge + S (S espi_right_enr_history) = S ((S (espi_left_enr_history)) * v)) /\ exists wpo_beta_quotient_enr_history_scaled_edge. u = wpo_beta_quotient_enr_history_scaled_edge * S ((S (espi_left_enr_history)) * v) + (S espi_right_enr_history)))))))) -> (forall wsl_index_enr_lift_n wsl_value_enr_lift_n. (exists wpo_gap_enr_lift_n_bound. wpo_gap_enr_lift_n_bound + S (wsl_index_enr_lift_n) = n) -> (((exists wpo_beta_height_enr_lift_n_source. wpo_beta_height_enr_lift_n_source + S (wsl_value_enr_lift_n) = S ((S (wsl_index_enr_lift_n)) * c)) /\ exists wpo_beta_quotient_enr_lift_n_source. b = wpo_beta_quotient_enr_lift_n_source * S ((S (wsl_index_enr_lift_n)) * c) + (wsl_value_enr_lift_n))) -> (((exists wpo_beta_height_enr_lift_n_target. wpo_beta_height_enr_lift_n_target + S (S wsl_value_enr_lift_n) = S ((S (wsl_index_enr_lift_n)) * g)) /\ exists wpo_beta_quotient_enr_lift_n_target. f = wpo_beta_quotient_enr_lift_n_target * S ((S (wsl_index_enr_lift_n)) * g) + (S wsl_value_enr_lift_n)))) -> (forall wpp_pair_enr_target_pairs wpp_left_enr_target_pairs wpp_right_enr_target_pairs. (exists wpp_gap_enr_target_pairs_pair_bound. wpp_gap_enr_target_pairs_pair_bound + S (wpp_pair_enr_target_pairs) = h) -> (((exists wpp_beta_height_enr_target_pairs_left_entry. wpp_beta_height_enr_target_pairs_left_entry + S (wpp_left_enr_target_pairs) = S ((S ((wpp_pair_enr_target_pairs + wpp_pair_enr_target_pairs))) * g)) /\ exists wpp_beta_quotient_enr_target_pairs_left_entry. f = wpp_beta_quotient_enr_target_pairs_left_entry * S ((S ((wpp_pair_enr_target_pairs + wpp_pair_enr_target_pairs))) * g) + (wpp_left_enr_target_pairs))) -> (((exists wpp_beta_height_enr_target_pairs_right_entry. wpp_beta_height_enr_target_pairs_right_entry + S (wpp_right_enr_target_pairs) = S ((S (S (wpp_pair_enr_target_pairs + wpp_pair_enr_target_pairs))) * g)) /\ exists wpp_beta_quotient_enr_target_pairs_right_entry. f = wpp_beta_quotient_enr_target_pairs_right_entry * S ((S (S (wpp_pair_enr_target_pairs + wpp_pair_enr_target_pairs))) * g) + (wpp_right_enr_target_pairs))) -> (exists wpp_mod_left_enr_target_pairs_pair_mod wpp_mod_right_enr_target_pairs_pair_mod. (wpp_left_enr_target_pairs * wpp_right_enr_target_pairs) + p * wpp_mod_left_enr_target_pairs_pair_mod = (a) + p * wpp_mod_right_enr_target_pairs_pair_mod))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
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
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 (3)
01Fix variables and assumptionsL1–10
02Fix variables and assumptionsL11–20
03Fix variables and assumptionsL21–21
Work with arbitrary variables or the premises of the current implication.
- L21
intro hright
04Establish horbitL22–25
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hhistory.
- L22
have horbit : ∃ i. ∃ j. BetaAt(b,c,t + t,i) ∧ (BetaAt(b,c,S (t + t),j) ∧ BetaAt(u,v,i,S j))Definitions: BetaAt(b,c,t + t,i)BetaAt(b,c,S (t + t),j)BetaAt(u,v,i,S j)Original native command in the exact edition - L23
specialize hhistory t - L24
apply hhistory - L25
exact ht
05Separate the logical casesL26–29
06Establish heven_rawL30–34
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair index left below double.
- L30
have heven_raw : Lt(t + t,h + h)Definitions: Lt(t + t,h + h)Original native command in the exact edition - L31
specialize pair_index_left_below_double t - L32
specialize pair_index_left_below_double h - L33
apply pair_index_left_below_double - L34
exact ht
07Establish hodd_rawL35–39
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair index right below double.
- L35
have hodd_raw : Lt(S (t + t),h + h)Definitions: Lt(S (t + t),h + h)Original native command in the exact edition - L36
specialize pair_index_right_below_double t - L37
specialize pair_index_right_below_double h - L38
apply pair_index_right_below_double - L39
exact ht
08Establish heven_nL40–42
Establish this local claim before using it. It is not an additional assumption.
09Establish hodd_nL43–45
Establish this local claim before using it. It is not an additional assumption.
- L43
have hodd_n : Lt(S (t + t),n)Definitions: Lt(S (t + t),n)Original native command in the exact edition - L44
rewrite heven - L45
exact hodd_raw
10Establish hlift_leftL46–51
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hlift.
- L46
have hlift_left : BetaAt(f,g,t + t,S x)Definitions: BetaAt(f,g,t + t,S x)Original native command in the exact edition - L47
specialize hlift (t + t) - L48
specialize hlift x - L49
apply hlift - L50
exact heven_n - L51
exact horbit_witness_witness_left
11Establish hlift_rightL52–57
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hlift.
- L52
have hlift_right : BetaAt(f,g,S (t + t),S x1)Definitions: BetaAt(f,g,S (t + t),S x1)Original native command in the exact edition - L53
specialize hlift (S (t + t)) - L54
specialize hlift x1 - L55
apply hlift - L56
exact hodd_n - L57
exact horbit_witness_witness_right_left
12Establish hleft_eqL58–66
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
13Establish hright_eqL67–75
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
14Establish hbounded_evenL76–79
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hbounded.
- L76
have hbounded_even : ∃ w. BetaAt(b,c,t + t,w) ∧ Lt(w,n)Definitions: BetaAt(b,c,t + t,w)Lt(w,n)Original native command in the exact edition - L77
specialize hbounded (t + t) - L78
apply hbounded - L79
exact heven_raw
15Separate the logical casesL80–81
16Establish hsource_eqL82–90
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
17Establish hsource_boundL91–93
Establish this local claim before using it. It is not an additional assumption.
18Establish hprefix_dataL94–97
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprefix.
- L94
have hprefix_data : ∃ y. BetaAt(u,v,x,y) ∧ ScaledInverseIndex(p,a,n,x,y)Definitions: BetaAt(u,v,x,y)ScaledInverseIndex(p,a,n,x,y)Original native command in the exact edition - L95
specialize hprefix x - L96
apply hprefix - L97
exact hsource_bound
19Separate the logical casesL98–102
20Establish hmate_eqL103–112
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.
- L103
have hmate_eq : x3 = S x1 - L104
specialize beta_at_unique u - L105
specialize beta_at_unique v - L106
specialize beta_at_unique x - L107
specialize beta_at_unique x3 - L108
specialize beta_at_unique (S x1) - L109
apply beta_at_unique - L110
exact hprefix_data_witness_left - L111
exact horbit_witness_witness_right_right - L112
rewrite hleft_eq
21Calculate and transport equalitiesL113–114
22Use earlier factsL115–115
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L115
exact hprefix_data_witness_right_right_right_right
Original defined command ledger · 115 lines
- 0001
intro p - 0002
intro a - 0003
intro n - 0004
intro u - 0005
intro v - 0006
intro b - 0007
intro c - 0008
intro f - 0009
intro g - 0010
intro h - 0011
intro heven - 0012
intro hprefix - 0013
intro hbounded - 0014
intro hhistory - 0015
intro hlift - 0016
intro t - 0017
intro left - 0018
intro right - 0019
intro ht - 0020
intro hleft - 0021
intro hright - 0022
have horbit : ∃ i. ∃ j. BetaAt(b,c,t + t,i) ∧ (BetaAt(b,c,S (t + t),j) ∧ BetaAt(u,v,i,S j))Exact native replay line
have horbit : exists i j. (((exists ff_h_enr_history_left. ff_h_enr_history_left + S (i) = S ((S (t + t)) * c)) /\ exists ff_q_enr_history_left. b = ff_q_enr_history_left * S ((S (t + t)) * c) + (i))) /\ ((((exists ff_h_enr_history_right. ff_h_enr_history_right + S (j) = S ((S (S (t + t))) * c)) /\ exists ff_q_enr_history_right. b = ff_q_enr_history_right * S ((S (S (t + t))) * c) + (j))) /\ (((exists ff_h_enr_history_scaled. ff_h_enr_history_scaled + S (S j) = S ((S (i)) * v)) /\ exists ff_q_enr_history_scaled. u = ff_q_enr_history_scaled * S ((S (i)) * v) + (S j)))) - 0023
specialize hhistory t - 0024
apply hhistory - 0025
exact ht - 0026
cases horbit - 0027
cases horbit_witness - 0028
cases horbit_witness_witness - 0029
cases horbit_witness_witness_right - 0030
have heven_raw : Lt(t + t,h + h)Exact native replay line
have heven_raw : exists wpo_gap_enr_even_bound_raw. wpo_gap_enr_even_bound_raw + S (t + t) = h + h - 0031
specialize pair_index_left_below_double t - 0032
specialize pair_index_left_below_double h - 0033
apply pair_index_left_below_double - 0034
exact ht - 0035
have hodd_raw : Lt(S (t + t),h + h)Exact native replay line
have hodd_raw : exists wpo_gap_enr_odd_bound_raw. wpo_gap_enr_odd_bound_raw + S (S (t + t)) = h + h - 0036
specialize pair_index_right_below_double t - 0037
specialize pair_index_right_below_double h - 0038
apply pair_index_right_below_double - 0039
exact ht - 0040
have heven_n : Lt(t + t,n)Exact native replay line
have heven_n : exists wpo_gap_enr_even_bound_n. wpo_gap_enr_even_bound_n + S (t + t) = n - 0041
rewrite heven - 0042
exact heven_raw - 0043
have hodd_n : Lt(S (t + t),n)Exact native replay line
have hodd_n : exists wpo_gap_enr_odd_bound_n. wpo_gap_enr_odd_bound_n + S (S (t + t)) = n - 0044
rewrite heven - 0045
exact hodd_raw - 0046
have hlift_left : BetaAt(f,g,t + t,S x)Exact native replay line
have hlift_left : ((exists ff_h_enr_lifted_left. ff_h_enr_lifted_left + S (S x) = S ((S (t + t)) * g)) /\ exists ff_q_enr_lifted_left. f = ff_q_enr_lifted_left * S ((S (t + t)) * g) + (S x)) - 0047
specialize hlift (t + t) - 0048
specialize hlift x - 0049
apply hlift - 0050
exact heven_n - 0051
exact horbit_witness_witness_left - 0052
have hlift_right : BetaAt(f,g,S (t + t),S x1)Exact native replay line
have hlift_right : ((exists ff_h_enr_lifted_right. ff_h_enr_lifted_right + S (S x1) = S ((S (S (t + t))) * g)) /\ exists ff_q_enr_lifted_right. f = ff_q_enr_lifted_right * S ((S (S (t + t))) * g) + (S x1)) - 0053
specialize hlift (S (t + t)) - 0054
specialize hlift x1 - 0055
apply hlift - 0056
exact hodd_n - 0057
exact horbit_witness_witness_right_left - 0058
have hleft_eq : left = S x - 0059
specialize beta_at_unique f - 0060
specialize beta_at_unique g - 0061
specialize beta_at_unique (t + t) - 0062
specialize beta_at_unique left - 0063
specialize beta_at_unique (S x) - 0064
apply beta_at_unique - 0065
exact hleft - 0066
exact hlift_left - 0067
have hright_eq : right = S x1 - 0068
specialize beta_at_unique f - 0069
specialize beta_at_unique g - 0070
specialize beta_at_unique (S (t + t)) - 0071
specialize beta_at_unique right - 0072
specialize beta_at_unique (S x1) - 0073
apply beta_at_unique - 0074
exact hright - 0075
exact hlift_right - 0076
have hbounded_even : ∃ w. BetaAt(b,c,t + t,w) ∧ Lt(w,n)Exact native replay line
have hbounded_even : exists w. (((exists ff_h_enr_bounded_even_entry. ff_h_enr_bounded_even_entry + S (w) = S ((S (t + t)) * c)) /\ exists ff_q_enr_bounded_even_entry. b = ff_q_enr_bounded_even_entry * S ((S (t + t)) * c) + (w))) /\ (exists wpo_gap_enr_bounded_even_value. wpo_gap_enr_bounded_even_value + S (w) = n) - 0077
specialize hbounded (t + t) - 0078
apply hbounded - 0079
exact heven_raw - 0080
cases hbounded_even - 0081
cases hbounded_even_witness - 0082
have hsource_eq : x = x2 - 0083
specialize beta_at_unique b - 0084
specialize beta_at_unique c - 0085
specialize beta_at_unique (t + t) - 0086
specialize beta_at_unique x - 0087
specialize beta_at_unique x2 - 0088
apply beta_at_unique - 0089
exact horbit_witness_witness_left - 0090
exact hbounded_even_witness_left - 0091
have hsource_bound : Lt(x,n)Exact native replay line
have hsource_bound : exists gap. gap + S x = n - 0092
rewrite hsource_eq - 0093
exact hbounded_even_witness_right - 0094
have hprefix_data : ∃ y. BetaAt(u,v,x,y) ∧ ScaledInverseIndex(p,a,n,x,y)Exact native replay line
have hprefix_data : exists y. (((exists ff_h_enr_prefix_at_x_entry. ff_h_enr_prefix_at_x_entry + S (y) = S ((S (x)) * v)) /\ exists ff_q_enr_prefix_at_x_entry. u = ff_q_enr_prefix_at_x_entry * S ((S (x)) * v) + (y))) /\ ((exists esip_gap_enr_prefix_at_x_relation_index_bound. esip_gap_enr_prefix_at_x_relation_index_bound + S (x) = n) /\ ((((~((S x) = 0) /\ (exists esip_gap_enr_prefix_at_x_relation_scaled_left_bound. esip_gap_enr_prefix_at_x_relation_scaled_left_bound + S (S x) = p))) /\ (((~(y = 0) /\ (exists esip_gap_enr_prefix_at_x_relation_scaled_right_bound. esip_gap_enr_prefix_at_x_relation_scaled_right_bound + S (y) = p))) /\ (exists esi_mod_left_enr_prefix_at_x_relation_scaled_mod esi_mod_right_enr_prefix_at_x_relation_scaled_mod. ((S x) * y) + p * esi_mod_left_enr_prefix_at_x_relation_scaled_mod = (a) + p * esi_mod_right_enr_prefix_at_x_relation_scaled_mod))))) - 0095
specialize hprefix x - 0096
apply hprefix - 0097
exact hsource_bound - 0098
cases hprefix_data - 0099
cases hprefix_data_witness - 0100
cases hprefix_data_witness_right - 0101
cases hprefix_data_witness_right_right - 0102
cases hprefix_data_witness_right_right_right - 0103
have hmate_eq : x3 = S x1 - 0104
specialize beta_at_unique u - 0105
specialize beta_at_unique v - 0106
specialize beta_at_unique x - 0107
specialize beta_at_unique x3 - 0108
specialize beta_at_unique (S x1) - 0109
apply beta_at_unique - 0110
exact hprefix_data_witness_left - 0111
exact horbit_witness_witness_right_right - 0112
rewrite hleft_eq - 0113
rewrite hright_eq - 0114
rewrite <- hmate_eq - 0115
exact hprefix_data_witness_right_right_right_right