PQ0021

prime_field_polynomial_trim_exists

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

Every actual canonical input has a genuinely beta-coded leading-zero trim, for all moduli and all finite lengths including zero.

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

forall p b c L. (forall fom_index_pfp_trim_exists_source. (exists fom_gap_pfp_trim_exists_source_index_bound. fom_gap_pfp_trim_exists_source_index_bound + S (fom_index_pfp_trim_exists_source) = L) -> exists fom_value_pfp_trim_exists_source. ((((exists fom_beta_height_pfp_trim_exists_source_entry. fom_beta_height_pfp_trim_exists_source_entry + S (fom_value_pfp_trim_exists_source) = S ((S (fom_index_pfp_trim_exists_source)) * c)) /\ exists fom_beta_quotient_pfp_trim_exists_source_entry. b = fom_beta_quotient_pfp_trim_exists_source_entry * S ((S (fom_index_pfp_trim_exists_source)) * c) + (fom_value_pfp_trim_exists_source))) /\ (exists fom_gap_pfp_trim_exists_source_value_bound. fom_gap_pfp_trim_exists_source_value_bound + S (fom_value_pfp_trim_exists_source) = p))) -> exists t d e M. ((((L)=(t)+(M)) /\ (((forall fom_index_pfp_trim_exists_resultinput. (exists fom_gap_pfp_trim_exists_resultinput_index_bound. fom_gap_pfp_trim_exists_resultinput_index_bound + S (fom_index_pfp_trim_exists_resultinput) = L) -> exists fom_value_pfp_trim_exists_resultinput. ((((exists fom_beta_height_pfp_trim_exists_resultinput_entry. fom_beta_height_pfp_trim_exists_resultinput_entry + S (fom_value_pfp_trim_exists_resultinput) = S ((S (fom_index_pfp_trim_exists_resultinput)) * c)) /\ exists fom_beta_quotient_pfp_trim_exists_resultinput_entry. b = fom_beta_quotient_pfp_trim_exists_resultinput_entry * S ((S (fom_index_pfp_trim_exists_resultinput)) * c) + (fom_value_pfp_trim_exists_resultinput))) /\ (exists fom_gap_pfp_trim_exists_resultinput_value_bound. fom_gap_pfp_trim_exists_resultinput_value_bound + S (fom_value_pfp_trim_exists_resultinput) = p))) /\ (((forall pfp_repeat_index_trim_exists_resultremoved. (exists pfa_gap_trim_exists_resultremovedindex. pfa_gap_trim_exists_resultremovedindex + S (pfp_repeat_index_trim_exists_resultremoved) = (t)) -> (((exists ff_h_pfp_trim_exists_resultremovedentry. ff_h_pfp_trim_exists_resultremovedentry + S (0) = S ((S (pfp_repeat_index_trim_exists_resultremoved)) * c)) /\ exists ff_q_pfp_trim_exists_resultremovedentry. b = ff_q_pfp_trim_exists_resultremovedentry * S ((S (pfp_repeat_index_trim_exists_resultremoved)) * c) + (0)))) /\ (((forall pftrim_index_trim_exists_resultsuffix pftrim_value_trim_exists_resultsuffix. (exists pfa_gap_trim_exists_resultsuffixbound. pfa_gap_trim_exists_resultsuffixbound + S (pftrim_index_trim_exists_resultsuffix) = (M)) -> (((exists ff_h_pfp_trim_exists_resultsuffixsource. ff_h_pfp_trim_exists_resultsuffixsource + S (pftrim_value_trim_exists_resultsuffix) = S ((S ((t)+pftrim_index_trim_exists_resultsuffix)) * c)) /\ exists ff_q_pfp_trim_exists_resultsuffixsource. b = ff_q_pfp_trim_exists_resultsuffixsource * S ((S ((t)+pftrim_index_trim_exists_resultsuffix)) * c) + (pftrim_value_trim_exists_resultsuffix))) -> (((exists ff_h_pfp_trim_exists_resultsuffixoutput. ff_h_pfp_trim_exists_resultsuffixoutput + S (pftrim_value_trim_exists_resultsuffix) = S ((S (pftrim_index_trim_exists_resultsuffix)) * e)) /\ exists ff_q_pfp_trim_exists_resultsuffixoutput. d = ff_q_pfp_trim_exists_resultsuffixoutput * S ((S (pftrim_index_trim_exists_resultsuffix)) * e) + (pftrim_value_trim_exists_resultsuffix)))) /\ (((M)=0 \/ (exists pftrim_leading_trim_exists_resultnormal. ((((exists ff_h_pfp_trim_exists_resultnormalentry. ff_h_pfp_trim_exists_resultnormalentry + S (pftrim_leading_trim_exists_resultnormal) = S ((S (0)) * e)) /\ exists ff_q_pfp_trim_exists_resultnormalentry. d = ff_q_pfp_trim_exists_resultnormalentry * S ((S (0)) * e) + (pftrim_leading_trim_exists_resultnormal))) /\ ((~(pftrim_leading_trim_exists_resultnormal=0)))))))))))))))

Constructive proof overview

Generated structural guide

Every actual canonical input has a genuinely beta-coded leading-zero trim, for all moduli and all finite lengths including zero.

The unchanged tactic script uses 3 declared prerequisites and contains 36 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PQ001F prime_field_polynomial_leading_zero_cut_exists PQ001B prime_field_polynomial_suffix_exists PQ0020 prime_field_polynomial_trim_from_cut

Direct dependents

PQ002D prime_field_polynomial_trim_exists_unique

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

36 script commands · 8 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 (3)
prime field polynomial leading zero cut existsprime field polynomial suffix existsprime field polynomial trim from cut

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

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro L
  5. L5
    intro hc
02Establish hcutL6–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial leading zero cut exists.

  1. L6
    have hcut : ∃ t. ∃ M. L = t + M ∧ (Repeat(b,c,0,t) ∧ (M = 0 ∨ ¬M = 0 ∧ (∃ x. BetaAt(b,c,t,x) ∧ ¬x = 0)))Definitions: BetaAtRepeat
  2. L7
    specialize prime_field_polynomial_leading_zero_cut_exists (b)
  3. L8
    specialize prime_field_polynomial_leading_zero_cut_exists (c)
  4. L9
    specialize prime_field_polynomial_leading_zero_cut_exists (L)
  5. L10
    apply prime_field_polynomial_leading_zero_cut_exists
03Separate the logical casesL11–12

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

  1. L11
    cases hcut
  2. L12
    cases hcut_witness
04Establish hsL13–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial suffix exists.

  1. L13
    have hs : ∃ d. ∃ e. PolynomialSuffix(b,c,x,d,e,x1)Definitions: PolynomialSuffix
  2. L14
    specialize prime_field_polynomial_suffix_exists (b)
  3. L15
    specialize prime_field_polynomial_suffix_exists (c)
  4. L16
    specialize prime_field_polynomial_suffix_exists (x)
  5. L17
    specialize prime_field_polynomial_suffix_exists (x1)
  6. L18
    apply prime_field_polynomial_suffix_exists
05Separate the logical casesL19–20

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

  1. L19
    cases hs
  2. L20
    cases hs_witness
06Construct an explicit witnessL21–24

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

  1. L21
    exists x
  2. L22
    exists x2
  3. L23
    exists x3
  4. L24
    exists x1
07Use earlier factsL25–34

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

  1. L25
    specialize prime_field_polynomial_trim_from_cut (p)
  2. L26
    specialize prime_field_polynomial_trim_from_cut (b)
  3. L27
    specialize prime_field_polynomial_trim_from_cut (c)
  4. L28
    specialize prime_field_polynomial_trim_from_cut (L)
  5. L29
    specialize prime_field_polynomial_trim_from_cut (x)
  6. L30
    specialize prime_field_polynomial_trim_from_cut (x2)
  7. L31
    specialize prime_field_polynomial_trim_from_cut (x3)
  8. L32
    specialize prime_field_polynomial_trim_from_cut (x1)
  9. L33
    apply prime_field_polynomial_trim_from_cut
  10. L34
    exact hc
08Use earlier factsL35–36

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

  1. L35
    exact hcut_witness_witness
  2. L36
    exact hs_witness_witness

Library-wide reading audit

Original exact command ledger · 36 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro L
  5. 0005intro hc
  6. 0006have hcut : exists t M. ((((L)=(t)+(M)) /\ (((forall pfp_repeat_index_trim_exists_cutzero. (exists pfa_gap_trim_exists_cutzeroindex. pfa_gap_trim_exists_cutzeroindex + S (pfp_repeat_index_trim_exists_cutzero) = (t)) -> (((exists ff_h_pfp_trim_exists_cutzeroentry. ff_h_pfp_trim_exists_cutzeroentry + S (0) = S ((S (pfp_repeat_index_trim_exists_cutzero)) * c)) /\ exists ff_q_pfp_trim_exists_cutzeroentry. b = ff_q_pfp_trim_exists_cutzeroentry * S ((S (pfp_repeat_index_trim_exists_cutzero)) * c) + (0)))) /\ (((M)=0 \/ (((~((M)=0)) /\ ((exists pftrim_leading_trim_exists_cuthead. ((((exists ff_h_pfp_trim_exists_cutheadentry. ff_h_pfp_trim_exists_cutheadentry + S (pftrim_leading_trim_exists_cuthead) = S ((S (t)) * c)) /\ exists ff_q_pfp_trim_exists_cutheadentry. b = ff_q_pfp_trim_exists_cutheadentry * S ((S (t)) * c) + (pftrim_leading_trim_exists_cuthead))) /\ ((~(pftrim_leading_trim_exists_cuthead=0))))))))))))))
  7. 0007specialize prime_field_polynomial_leading_zero_cut_exists (b)
  8. 0008specialize prime_field_polynomial_leading_zero_cut_exists (c)
  9. 0009specialize prime_field_polynomial_leading_zero_cut_exists (L)
  10. 0010apply prime_field_polynomial_leading_zero_cut_exists
  11. 0011cases hcut
  12. 0012cases hcut_witness
  13. 0013have hs : exists d e. (forall pftrim_index_trim_exists_suffix pftrim_value_trim_exists_suffix. (exists pfa_gap_trim_exists_suffixbound. pfa_gap_trim_exists_suffixbound + S (pftrim_index_trim_exists_suffix) = (x1)) -> (((exists ff_h_pfp_trim_exists_suffixsource. ff_h_pfp_trim_exists_suffixsource + S (pftrim_value_trim_exists_suffix) = S ((S ((x)+pftrim_index_trim_exists_suffix)) * c)) /\ exists ff_q_pfp_trim_exists_suffixsource. b = ff_q_pfp_trim_exists_suffixsource * S ((S ((x)+pftrim_index_trim_exists_suffix)) * c) + (pftrim_value_trim_exists_suffix))) -> (((exists ff_h_pfp_trim_exists_suffixoutput. ff_h_pfp_trim_exists_suffixoutput + S (pftrim_value_trim_exists_suffix) = S ((S (pftrim_index_trim_exists_suffix)) * e)) /\ exists ff_q_pfp_trim_exists_suffixoutput. d = ff_q_pfp_trim_exists_suffixoutput * S ((S (pftrim_index_trim_exists_suffix)) * e) + (pftrim_value_trim_exists_suffix))))
  14. 0014specialize prime_field_polynomial_suffix_exists (b)
  15. 0015specialize prime_field_polynomial_suffix_exists (c)
  16. 0016specialize prime_field_polynomial_suffix_exists (x)
  17. 0017specialize prime_field_polynomial_suffix_exists (x1)
  18. 0018apply prime_field_polynomial_suffix_exists
  19. 0019cases hs
  20. 0020cases hs_witness
  21. 0021exists x
  22. 0022exists x2
  23. 0023exists x3
  24. 0024exists x1
  25. 0025specialize prime_field_polynomial_trim_from_cut (p)
  26. 0026specialize prime_field_polynomial_trim_from_cut (b)
  27. 0027specialize prime_field_polynomial_trim_from_cut (c)
  28. 0028specialize prime_field_polynomial_trim_from_cut (L)
  29. 0029specialize prime_field_polynomial_trim_from_cut (x)
  30. 0030specialize prime_field_polynomial_trim_from_cut (x2)
  31. 0031specialize prime_field_polynomial_trim_from_cut (x3)
  32. 0032specialize prime_field_polynomial_trim_from_cut (x1)
  33. 0033apply prime_field_polynomial_trim_from_cut
  34. 0034exact hc
  35. 0035exact hcut_witness_witness
  36. 0036exact hs_witness_witness