HD000F

beta_horner_derivative_linear

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

A genuine two-coefficient polynomial a*t+k has the exact decoded formal derivative a.

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 first-order arithmetic statement

forall b c t n z. (exists ff_u_hd_linear ff_v_hd_linear ff_d_hd_linear ff_e_hd_linear. ((((((exists fs_h_ph_hd_linear_body_value_start. fs_h_ph_hd_linear_body_value_start + S (0) = S ((S (0)) * ff_v_hd_linear)) /\ exists fs_q_ph_hd_linear_body_value_start. ff_u_hd_linear = fs_q_ph_hd_linear_body_value_start * S ((S (0)) * ff_v_hd_linear) + (0))) /\ ((((exists fs_h_ph_hd_linear_body_value_terminal. fs_h_ph_hd_linear_body_value_terminal + S (n) = S ((S (S S 0)) * ff_v_hd_linear)) /\ exists fs_q_ph_hd_linear_body_value_terminal. ff_u_hd_linear = fs_q_ph_hd_linear_body_value_terminal * S ((S (S S 0)) * ff_v_hd_linear) + (n))) /\ forall ff_i_ph_hd_linear_body_value_steps. (exists ph_bound_hd_linear_body_value_steps. ph_bound_hd_linear_body_value_steps + S ff_i_ph_hd_linear_body_value_steps = S S 0) -> exists ff_coefficient_ph_hd_linear_body_value_steps ff_previous_ph_hd_linear_body_value_steps ff_current_ph_hd_linear_body_value_steps. ((((exists fs_h_ph_hd_linear_body_value_steps_coefficient. fs_h_ph_hd_linear_body_value_steps_coefficient + S (ff_coefficient_ph_hd_linear_body_value_steps) = S ((S (ff_i_ph_hd_linear_body_value_steps)) * c)) /\ exists fs_q_ph_hd_linear_body_value_steps_coefficient. b = fs_q_ph_hd_linear_body_value_steps_coefficient * S ((S (ff_i_ph_hd_linear_body_value_steps)) * c) + (ff_coefficient_ph_hd_linear_body_value_steps))) /\ ((((exists fs_h_ph_hd_linear_body_value_steps_before. fs_h_ph_hd_linear_body_value_steps_before + S (ff_previous_ph_hd_linear_body_value_steps) = S ((S (ff_i_ph_hd_linear_body_value_steps)) * ff_v_hd_linear)) /\ exists fs_q_ph_hd_linear_body_value_steps_before. ff_u_hd_linear = fs_q_ph_hd_linear_body_value_steps_before * S ((S (ff_i_ph_hd_linear_body_value_steps)) * ff_v_hd_linear) + (ff_previous_ph_hd_linear_body_value_steps))) /\ ((((exists fs_h_ph_hd_linear_body_value_steps_after. fs_h_ph_hd_linear_body_value_steps_after + S (ff_current_ph_hd_linear_body_value_steps) = S ((S (S ff_i_ph_hd_linear_body_value_steps)) * ff_v_hd_linear)) /\ exists fs_q_ph_hd_linear_body_value_steps_after. ff_u_hd_linear = fs_q_ph_hd_linear_body_value_steps_after * S ((S (S ff_i_ph_hd_linear_body_value_steps)) * ff_v_hd_linear) + (ff_current_ph_hd_linear_body_value_steps))) /\ ff_current_ph_hd_linear_body_value_steps = ff_previous_ph_hd_linear_body_value_steps * t + ff_coefficient_ph_hd_linear_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_linear_body_derivative_start. fs_h_ph_hd_linear_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_linear)) /\ exists fs_q_ph_hd_linear_body_derivative_start. ff_d_hd_linear = fs_q_ph_hd_linear_body_derivative_start * S ((S (0)) * ff_e_hd_linear) + (0))) /\ ((((exists fs_h_ph_hd_linear_body_derivative_terminal. fs_h_ph_hd_linear_body_derivative_terminal + S (z) = S ((S (S S 0)) * ff_e_hd_linear)) /\ exists fs_q_ph_hd_linear_body_derivative_terminal. ff_d_hd_linear = fs_q_ph_hd_linear_body_derivative_terminal * S ((S (S S 0)) * ff_e_hd_linear) + (z))) /\ forall ff_i_ph_hd_linear_body_derivative_steps. (exists ph_bound_hd_linear_body_derivative_steps. ph_bound_hd_linear_body_derivative_steps + S ff_i_ph_hd_linear_body_derivative_steps = S S 0) -> exists ff_coefficient_ph_hd_linear_body_derivative_steps ff_previous_ph_hd_linear_body_derivative_steps ff_current_ph_hd_linear_body_derivative_steps. ((((exists fs_h_ph_hd_linear_body_derivative_steps_coefficient. fs_h_ph_hd_linear_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_linear_body_derivative_steps) = S ((S (ff_i_ph_hd_linear_body_derivative_steps)) * ff_v_hd_linear)) /\ exists fs_q_ph_hd_linear_body_derivative_steps_coefficient. ff_u_hd_linear = fs_q_ph_hd_linear_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_linear_body_derivative_steps)) * ff_v_hd_linear) + (ff_coefficient_ph_hd_linear_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_linear_body_derivative_steps_before. fs_h_ph_hd_linear_body_derivative_steps_before + S (ff_previous_ph_hd_linear_body_derivative_steps) = S ((S (ff_i_ph_hd_linear_body_derivative_steps)) * ff_e_hd_linear)) /\ exists fs_q_ph_hd_linear_body_derivative_steps_before. ff_d_hd_linear = fs_q_ph_hd_linear_body_derivative_steps_before * S ((S (ff_i_ph_hd_linear_body_derivative_steps)) * ff_e_hd_linear) + (ff_previous_ph_hd_linear_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_linear_body_derivative_steps_after. fs_h_ph_hd_linear_body_derivative_steps_after + S (ff_current_ph_hd_linear_body_derivative_steps) = S ((S (S ff_i_ph_hd_linear_body_derivative_steps)) * ff_e_hd_linear)) /\ exists fs_q_ph_hd_linear_body_derivative_steps_after. ff_d_hd_linear = fs_q_ph_hd_linear_body_derivative_steps_after * S ((S (S ff_i_ph_hd_linear_body_derivative_steps)) * ff_e_hd_linear) + (ff_current_ph_hd_linear_body_derivative_steps))) /\ ff_current_ph_hd_linear_body_derivative_steps = ff_previous_ph_hd_linear_body_derivative_steps * t + ff_coefficient_ph_hd_linear_body_derivative_steps)))))))) -> exists a k. ((((exists fs_h_hd_linear_leading. fs_h_hd_linear_leading + S (a) = S ((S (0)) * c)) /\ exists fs_q_hd_linear_leading. b = fs_q_hd_linear_leading * S ((S (0)) * c) + (a))) /\ ((((exists fs_h_hd_linear_constant. fs_h_hd_linear_constant + S (k) = S ((S (S 0)) * c)) /\ exists fs_q_hd_linear_constant. b = fs_q_hd_linear_constant * S ((S (S 0)) * c) + (k))) /\ ((n = a * t + k) /\ z = a)))

Constructive proof overview

Generated structural guide

A genuine two-coefficient polynomial a*t+k has the exact decoded formal derivative a.

The unchanged tactic script uses 4 declared prerequisites and contains 51 exact native proof lines.

Alpha v34 checked-use · first admitted v24 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

HD0008 beta_horner_derivative_successor_decompose HD000E beta_horner_derivative_constant mul_zero_left Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

51 script commands · 19 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.

Named ingredients (2)
beta horner derivative successor decomposebeta horner derivative constant

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–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro t
  4. L4
    intro n
  5. L5
    intro z
  6. L6
    intro hpair
02Establish hdecompositionL7–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner derivative successor decompose.

  1. L7
    have hdecomposition : ∃ a. ∃ r. ∃ q. Beta(b,c,1,a) ∧ (HornerDerivative(b,c,t,1,r,q) ∧ (n = r · t + a ∧ z = q · t + r))Definitions: BetaHornerDerivative
  2. L8
    specialize beta_horner_derivative_successor_decompose b
  3. L9
    specialize beta_horner_derivative_successor_decompose c
  4. L10
    specialize beta_horner_derivative_successor_decompose t
  5. L11
    specialize beta_horner_derivative_successor_decompose (S 0)
  6. L12
    specialize beta_horner_derivative_successor_decompose n
  7. L13
    specialize beta_horner_derivative_successor_decompose z
  8. L14
    apply beta_horner_derivative_successor_decompose
  9. L15
    exact hpair
03Separate the logical casesL16–21

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L16
    cases hdecomposition
  2. L17
    cases hdecomposition_witness
  3. L18
    cases hdecomposition_witness_witness
  4. L19
    cases hdecomposition_witness_witness_witness
  5. L20
    cases hdecomposition_witness_witness_witness_right
  6. L21
    cases hdecomposition_witness_witness_witness_right_right
04Establish hconstantL22–29

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner derivative constant.

  1. L22
    have hconstant : exists a. ((((exists fs_h_hd_linear_prefix_coefficient. fs_h_hd_linear_prefix_coefficient + S (a) = S ((S (0)) * c)) /\ exists fs_q_hd_linear_prefix_coefficient. b = fs_q_hd_linear_prefix_coefficient * S ((S (0)) * c) + (a))) /\ ((x1 = a) /\ x2 = 0))
  2. L23
    specialize beta_horner_derivative_constant b
  3. L24
    specialize beta_horner_derivative_constant c
  4. L25
    specialize beta_horner_derivative_constant t
  5. L26
    specialize beta_horner_derivative_constant x1
  6. L27
    specialize beta_horner_derivative_constant x2
  7. L28
    apply beta_horner_derivative_constant
  8. L29
    exact hdecomposition_witness_witness_witness_right_left
05Separate the logical casesL30–32

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L30
    cases hconstant
  2. L31
    cases hconstant_witness
  3. L32
    cases hconstant_witness_right
06Construct an explicit witnessL33–34

Supply the displayed value, then prove that it has the required property.

  1. L33
    exists x3
  2. L34
    exists x
07Separate the logical casesL35–35

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L35
    split
08Use earlier factsL36–36

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L36
    exact hconstant_witness_left
09Separate the logical casesL37–37

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L37
    split
10Use earlier factsL38–38

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L38
    exact hdecomposition_witness_witness_witness_left
11Separate the logical casesL39–39

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L39
    split
12Calculate and transport equalitiesL40–40

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L40
    trans x1 * t + x
13Use earlier factsL41–41

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L41
    exact hdecomposition_witness_witness_witness_right_right_left
14Calculate and transport equalitiesL42–44

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L42
    rewrite hconstant_witness_right_left
  2. L43
    refl
  3. L44
    trans x2 * t + x1
15Use earlier factsL45–45

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L45
    exact hdecomposition_witness_witness_witness_right_right_right
16Calculate and transport equalitiesL46–47

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L46
    rewrite hconstant_witness_right_right
  2. L47
    rewrite hconstant_witness_right_left
17Use earlier factsL48–48

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L48
    specialize mul_zero_left t
18Calculate and transport equalitiesL49–49

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L49
    rewrite mul_zero_left
19Use earlier factsL50–51

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L50
    specialize zero_add x3
  2. L51
    exact zero_add

Library-wide reading audit

Original exact command ledger · 51 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro t
  4. 0004intro n
  5. 0005intro z
  6. 0006intro hpair
  7. 0007have hdecomposition : exists a r q. ((((exists fs_h_hd_linear_step. fs_h_hd_linear_step + S (a) = S ((S (S 0)) * c)) /\ exists fs_q_hd_linear_step. b = fs_q_hd_linear_step * S ((S (S 0)) * c) + (a))) /\ ((exists ff_u_hd_linear_prefix ff_v_hd_linear_prefix ff_d_hd_linear_prefix ff_e_hd_linear_prefix. ((((((exists fs_h_ph_hd_linear_prefix_body_value_start. fs_h_ph_hd_linear_prefix_body_value_start + S (0) = S ((S (0)) * ff_v_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_value_start. ff_u_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_value_start * S ((S (0)) * ff_v_hd_linear_prefix) + (0))) /\ ((((exists fs_h_ph_hd_linear_prefix_body_value_terminal. fs_h_ph_hd_linear_prefix_body_value_terminal + S (r) = S ((S (S 0)) * ff_v_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_value_terminal. ff_u_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_value_terminal * S ((S (S 0)) * ff_v_hd_linear_prefix) + (r))) /\ forall ff_i_ph_hd_linear_prefix_body_value_steps. (exists ph_bound_hd_linear_prefix_body_value_steps. ph_bound_hd_linear_prefix_body_value_steps + S ff_i_ph_hd_linear_prefix_body_value_steps = S 0) -> exists ff_coefficient_ph_hd_linear_prefix_body_value_steps ff_previous_ph_hd_linear_prefix_body_value_steps ff_current_ph_hd_linear_prefix_body_value_steps. ((((exists fs_h_ph_hd_linear_prefix_body_value_steps_coefficient. fs_h_ph_hd_linear_prefix_body_value_steps_coefficient + S (ff_coefficient_ph_hd_linear_prefix_body_value_steps) = S ((S (ff_i_ph_hd_linear_prefix_body_value_steps)) * c)) /\ exists fs_q_ph_hd_linear_prefix_body_value_steps_coefficient. b = fs_q_ph_hd_linear_prefix_body_value_steps_coefficient * S ((S (ff_i_ph_hd_linear_prefix_body_value_steps)) * c) + (ff_coefficient_ph_hd_linear_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_linear_prefix_body_value_steps_before. fs_h_ph_hd_linear_prefix_body_value_steps_before + S (ff_previous_ph_hd_linear_prefix_body_value_steps) = S ((S (ff_i_ph_hd_linear_prefix_body_value_steps)) * ff_v_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_value_steps_before. ff_u_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_value_steps_before * S ((S (ff_i_ph_hd_linear_prefix_body_value_steps)) * ff_v_hd_linear_prefix) + (ff_previous_ph_hd_linear_prefix_body_value_steps))) /\ ((((exists fs_h_ph_hd_linear_prefix_body_value_steps_after. fs_h_ph_hd_linear_prefix_body_value_steps_after + S (ff_current_ph_hd_linear_prefix_body_value_steps) = S ((S (S ff_i_ph_hd_linear_prefix_body_value_steps)) * ff_v_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_value_steps_after. ff_u_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_value_steps_after * S ((S (S ff_i_ph_hd_linear_prefix_body_value_steps)) * ff_v_hd_linear_prefix) + (ff_current_ph_hd_linear_prefix_body_value_steps))) /\ ff_current_ph_hd_linear_prefix_body_value_steps = ff_previous_ph_hd_linear_prefix_body_value_steps * t + ff_coefficient_ph_hd_linear_prefix_body_value_steps)))))) /\ (((((exists fs_h_ph_hd_linear_prefix_body_derivative_start. fs_h_ph_hd_linear_prefix_body_derivative_start + S (0) = S ((S (0)) * ff_e_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_derivative_start. ff_d_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_derivative_start * S ((S (0)) * ff_e_hd_linear_prefix) + (0))) /\ ((((exists fs_h_ph_hd_linear_prefix_body_derivative_terminal. fs_h_ph_hd_linear_prefix_body_derivative_terminal + S (q) = S ((S (S 0)) * ff_e_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_derivative_terminal. ff_d_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_derivative_terminal * S ((S (S 0)) * ff_e_hd_linear_prefix) + (q))) /\ forall ff_i_ph_hd_linear_prefix_body_derivative_steps. (exists ph_bound_hd_linear_prefix_body_derivative_steps. ph_bound_hd_linear_prefix_body_derivative_steps + S ff_i_ph_hd_linear_prefix_body_derivative_steps = S 0) -> exists ff_coefficient_ph_hd_linear_prefix_body_derivative_steps ff_previous_ph_hd_linear_prefix_body_derivative_steps ff_current_ph_hd_linear_prefix_body_derivative_steps. ((((exists fs_h_ph_hd_linear_prefix_body_derivative_steps_coefficient. fs_h_ph_hd_linear_prefix_body_derivative_steps_coefficient + S (ff_coefficient_ph_hd_linear_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_linear_prefix_body_derivative_steps)) * ff_v_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_derivative_steps_coefficient. ff_u_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_derivative_steps_coefficient * S ((S (ff_i_ph_hd_linear_prefix_body_derivative_steps)) * ff_v_hd_linear_prefix) + (ff_coefficient_ph_hd_linear_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_linear_prefix_body_derivative_steps_before. fs_h_ph_hd_linear_prefix_body_derivative_steps_before + S (ff_previous_ph_hd_linear_prefix_body_derivative_steps) = S ((S (ff_i_ph_hd_linear_prefix_body_derivative_steps)) * ff_e_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_derivative_steps_before. ff_d_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_derivative_steps_before * S ((S (ff_i_ph_hd_linear_prefix_body_derivative_steps)) * ff_e_hd_linear_prefix) + (ff_previous_ph_hd_linear_prefix_body_derivative_steps))) /\ ((((exists fs_h_ph_hd_linear_prefix_body_derivative_steps_after. fs_h_ph_hd_linear_prefix_body_derivative_steps_after + S (ff_current_ph_hd_linear_prefix_body_derivative_steps) = S ((S (S ff_i_ph_hd_linear_prefix_body_derivative_steps)) * ff_e_hd_linear_prefix)) /\ exists fs_q_ph_hd_linear_prefix_body_derivative_steps_after. ff_d_hd_linear_prefix = fs_q_ph_hd_linear_prefix_body_derivative_steps_after * S ((S (S ff_i_ph_hd_linear_prefix_body_derivative_steps)) * ff_e_hd_linear_prefix) + (ff_current_ph_hd_linear_prefix_body_derivative_steps))) /\ ff_current_ph_hd_linear_prefix_body_derivative_steps = ff_previous_ph_hd_linear_prefix_body_derivative_steps * t + ff_coefficient_ph_hd_linear_prefix_body_derivative_steps)))))))) /\ ((n = r * t + a) /\ z = q * t + r)))
  8. 0008specialize beta_horner_derivative_successor_decompose b
  9. 0009specialize beta_horner_derivative_successor_decompose c
  10. 0010specialize beta_horner_derivative_successor_decompose t
  11. 0011specialize beta_horner_derivative_successor_decompose (S 0)
  12. 0012specialize beta_horner_derivative_successor_decompose n
  13. 0013specialize beta_horner_derivative_successor_decompose z
  14. 0014apply beta_horner_derivative_successor_decompose
  15. 0015exact hpair
  16. 0016cases hdecomposition
  17. 0017cases hdecomposition_witness
  18. 0018cases hdecomposition_witness_witness
  19. 0019cases hdecomposition_witness_witness_witness
  20. 0020cases hdecomposition_witness_witness_witness_right
  21. 0021cases hdecomposition_witness_witness_witness_right_right
  22. 0022have hconstant : exists a. ((((exists fs_h_hd_linear_prefix_coefficient. fs_h_hd_linear_prefix_coefficient + S (a) = S ((S (0)) * c)) /\ exists fs_q_hd_linear_prefix_coefficient. b = fs_q_hd_linear_prefix_coefficient * S ((S (0)) * c) + (a))) /\ ((x1 = a) /\ x2 = 0))
  23. 0023specialize beta_horner_derivative_constant b
  24. 0024specialize beta_horner_derivative_constant c
  25. 0025specialize beta_horner_derivative_constant t
  26. 0026specialize beta_horner_derivative_constant x1
  27. 0027specialize beta_horner_derivative_constant x2
  28. 0028apply beta_horner_derivative_constant
  29. 0029exact hdecomposition_witness_witness_witness_right_left
  30. 0030cases hconstant
  31. 0031cases hconstant_witness
  32. 0032cases hconstant_witness_right
  33. 0033exists x3
  34. 0034exists x
  35. 0035split
  36. 0036exact hconstant_witness_left
  37. 0037split
  38. 0038exact hdecomposition_witness_witness_witness_left
  39. 0039split
  40. 0040trans x1 * t + x
  41. 0041exact hdecomposition_witness_witness_witness_right_right_left
  42. 0042rewrite hconstant_witness_right_left
  43. 0043refl
  44. 0044trans x2 * t + x1
  45. 0045exact hdecomposition_witness_witness_witness_right_right_right
  46. 0046rewrite hconstant_witness_right_right
  47. 0047rewrite hconstant_witness_right_left
  48. 0048specialize mul_zero_left t
  49. 0049rewrite mul_zero_left
  50. 0050specialize zero_add x3
  51. 0051exact zero_add

Separate complete second-wave branches: Full G095 proof · Alpha v27.