JT005A

jordan_unit_modulus_singleton_enumeration

An actual one-position beta list is sound, complete and duplicate-free for primitive tuples modulo one.

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

95 new Alpha admissions come from 96 source lemmas: tuple equality reflexivity reuses an already-admitted theorem and is not counted twice. All counts use actual finite beta-coded enumerations. G008 multiplicativity is proved; the general prime-power count and distinct-prime product formula are further goals. General prime-power fields (G091) remain open. Stable is unchanged.

Exact theorem in conservative defined notation

∀ k. JordanTupleEnumeration(k,1,0,0,0,0,1)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

JordanTupleEnumeration(k,n,B,C,D,E,j) · 1

Actual proof prerequisites

finite_beta_zero_code · checked external prerequisitejordan_zero_tuple_bounded_onejordan_primitive_tuple_modulus_onejordan_tuples_bounded_one_equalle_zero · checked external prerequisitele_of_succ_le_succ · checked external prerequisite
Original expanded first-order statement 
forall k. (((forall jt_i_unit_enumeration. (exists jt_gap_unit_enumerationsoundindex. jt_gap_unit_enumerationsoundindex+S (jt_i_unit_enumeration)=(1)) -> exists jt_b_unit_enumeration jt_c_unit_enumeration. ((((((exists fs_h_jt_unit_enumerationsoundcode. fs_h_jt_unit_enumerationsoundcode + S (jt_b_unit_enumeration) = S ((S (jt_i_unit_enumeration)) * 0)) /\ exists fs_q_jt_unit_enumerationsoundcode. 0 = fs_q_jt_unit_enumerationsoundcode * S ((S (jt_i_unit_enumeration)) * 0) + (jt_b_unit_enumeration))) /\ (((exists fs_h_jt_unit_enumerationsoundscale. fs_h_jt_unit_enumerationsoundscale + S (jt_c_unit_enumeration) = S ((S (jt_i_unit_enumeration)) * 0)) /\ exists fs_q_jt_unit_enumerationsoundscale. 0 = fs_q_jt_unit_enumerationsoundscale * S ((S (jt_i_unit_enumeration)) * 0) + (jt_c_unit_enumeration))))) /\ (((forall jt_index_unit_enumerationbound. (exists jt_gap_unit_enumerationboundindex. jt_gap_unit_enumerationboundindex+S (jt_index_unit_enumerationbound)=(k)) -> exists jt_value_unit_enumerationbound. ((((exists fs_h_jt_unit_enumerationboundat. fs_h_jt_unit_enumerationboundat + S (jt_value_unit_enumerationbound) = S ((S (jt_index_unit_enumerationbound)) * jt_c_unit_enumeration)) /\ exists fs_q_jt_unit_enumerationboundat. jt_b_unit_enumeration = fs_q_jt_unit_enumerationboundat * S ((S (jt_index_unit_enumerationbound)) * jt_c_unit_enumeration) + (jt_value_unit_enumerationbound))) /\ (exists jt_gap_unit_enumerationboundvalue. jt_gap_unit_enumerationboundvalue+S (jt_value_unit_enumerationbound)=(1)))) /\ (forall jt_divisor_unit_enumerationprimitive. (exists jt_factor_unit_enumerationprimitivemodulus. (1)=(jt_divisor_unit_enumerationprimitive)*jt_factor_unit_enumerationprimitivemodulus) -> (forall jt_index_unit_enumerationprimitivecoordinates jt_value_unit_enumerationprimitivecoordinates. (exists jt_gap_unit_enumerationprimitivecoordinatesindex. jt_gap_unit_enumerationprimitivecoordinatesindex+S (jt_index_unit_enumerationprimitivecoordinates)=(k)) -> (((exists fs_h_jt_unit_enumerationprimitivecoordinatesat. fs_h_jt_unit_enumerationprimitivecoordinatesat + S (jt_value_unit_enumerationprimitivecoordinates) = S ((S (jt_index_unit_enumerationprimitivecoordinates)) * jt_c_unit_enumeration)) /\ exists fs_q_jt_unit_enumerationprimitivecoordinatesat. jt_b_unit_enumeration = fs_q_jt_unit_enumerationprimitivecoordinatesat * S ((S (jt_index_unit_enumerationprimitivecoordinates)) * jt_c_unit_enumeration) + (jt_value_unit_enumerationprimitivecoordinates))) -> (exists jt_factor_unit_enumerationprimitivecoordinatesdivides. (jt_value_unit_enumerationprimitivecoordinates)=(jt_divisor_unit_enumerationprimitive)*jt_factor_unit_enumerationprimitivecoordinatesdivides)) -> jt_divisor_unit_enumerationprimitive=1))))) /\ (((forall jt_b_unit_enumeration jt_c_unit_enumeration. (forall jt_index_unit_enumerationinputbound. (exists jt_gap_unit_enumerationinputboundindex. jt_gap_unit_enumerationinputboundindex+S (jt_index_unit_enumerationinputbound)=(k)) -> exists jt_value_unit_enumerationinputbound. ((((exists fs_h_jt_unit_enumerationinputboundat. fs_h_jt_unit_enumerationinputboundat + S (jt_value_unit_enumerationinputbound) = S ((S (jt_index_unit_enumerationinputbound)) * jt_c_unit_enumeration)) /\ exists fs_q_jt_unit_enumerationinputboundat. jt_b_unit_enumeration = fs_q_jt_unit_enumerationinputboundat * S ((S (jt_index_unit_enumerationinputbound)) * jt_c_unit_enumeration) + (jt_value_unit_enumerationinputbound))) /\ (exists jt_gap_unit_enumerationinputboundvalue. jt_gap_unit_enumerationinputboundvalue+S (jt_value_unit_enumerationinputbound)=(1)))) -> (forall jt_divisor_unit_enumerationinputprimitive. (exists jt_factor_unit_enumerationinputprimitivemodulus. (1)=(jt_divisor_unit_enumerationinputprimitive)*jt_factor_unit_enumerationinputprimitivemodulus) -> (forall jt_index_unit_enumerationinputprimitivecoordinates jt_value_unit_enumerationinputprimitivecoordinates. (exists jt_gap_unit_enumerationinputprimitivecoordinatesindex. jt_gap_unit_enumerationinputprimitivecoordinatesindex+S (jt_index_unit_enumerationinputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_unit_enumerationinputprimitivecoordinatesat. fs_h_jt_unit_enumerationinputprimitivecoordinatesat + S (jt_value_unit_enumerationinputprimitivecoordinates) = S ((S (jt_index_unit_enumerationinputprimitivecoordinates)) * jt_c_unit_enumeration)) /\ exists fs_q_jt_unit_enumerationinputprimitivecoordinatesat. jt_b_unit_enumeration = fs_q_jt_unit_enumerationinputprimitivecoordinatesat * S ((S (jt_index_unit_enumerationinputprimitivecoordinates)) * jt_c_unit_enumeration) + (jt_value_unit_enumerationinputprimitivecoordinates))) -> (exists jt_factor_unit_enumerationinputprimitivecoordinatesdivides. (jt_value_unit_enumerationinputprimitivecoordinates)=(jt_divisor_unit_enumerationinputprimitive)*jt_factor_unit_enumerationinputprimitivecoordinatesdivides)) -> jt_divisor_unit_enumerationinputprimitive=1) -> exists jt_i_unit_enumeration jt_d_unit_enumeration jt_e_unit_enumeration. ((exists jt_gap_unit_enumerationcompleteindex. jt_gap_unit_enumerationcompleteindex+S (jt_i_unit_enumeration)=(1)) /\ (((((((exists fs_h_jt_unit_enumerationcompletecode. fs_h_jt_unit_enumerationcompletecode + S (jt_d_unit_enumeration) = S ((S (jt_i_unit_enumeration)) * 0)) /\ exists fs_q_jt_unit_enumerationcompletecode. 0 = fs_q_jt_unit_enumerationcompletecode * S ((S (jt_i_unit_enumeration)) * 0) + (jt_d_unit_enumeration))) /\ (((exists fs_h_jt_unit_enumerationcompletescale. fs_h_jt_unit_enumerationcompletescale + S (jt_e_unit_enumeration) = S ((S (jt_i_unit_enumeration)) * 0)) /\ exists fs_q_jt_unit_enumerationcompletescale. 0 = fs_q_jt_unit_enumerationcompletescale * S ((S (jt_i_unit_enumeration)) * 0) + (jt_e_unit_enumeration))))) /\ (forall jt_index_unit_enumerationrepresented jt_left_unit_enumerationrepresented jt_right_unit_enumerationrepresented. (exists jt_gap_unit_enumerationrepresentedindex. jt_gap_unit_enumerationrepresentedindex+S (jt_index_unit_enumerationrepresented)=(k)) -> (((exists fs_h_jt_unit_enumerationrepresentedleft. fs_h_jt_unit_enumerationrepresentedleft + S (jt_left_unit_enumerationrepresented) = S ((S (jt_index_unit_enumerationrepresented)) * jt_c_unit_enumeration)) /\ exists fs_q_jt_unit_enumerationrepresentedleft. jt_b_unit_enumeration = fs_q_jt_unit_enumerationrepresentedleft * S ((S (jt_index_unit_enumerationrepresented)) * jt_c_unit_enumeration) + (jt_left_unit_enumerationrepresented))) -> (((exists fs_h_jt_unit_enumerationrepresentedright. fs_h_jt_unit_enumerationrepresentedright + S (jt_right_unit_enumerationrepresented) = S ((S (jt_index_unit_enumerationrepresented)) * jt_e_unit_enumeration)) /\ exists fs_q_jt_unit_enumerationrepresentedright. jt_d_unit_enumeration = fs_q_jt_unit_enumerationrepresentedright * S ((S (jt_index_unit_enumerationrepresented)) * jt_e_unit_enumeration) + (jt_right_unit_enumerationrepresented))) -> jt_left_unit_enumerationrepresented=jt_right_unit_enumerationrepresented))))) /\ (forall jt_i_unit_enumeration jt_h_unit_enumeration jt_b_unit_enumeration jt_c_unit_enumeration jt_d_unit_enumeration jt_e_unit_enumeration. (exists jt_gap_unit_enumerationfirstindex. jt_gap_unit_enumerationfirstindex+S (jt_i_unit_enumeration)=(1)) -> (exists jt_gap_unit_enumerationsecondindex. jt_gap_unit_enumerationsecondindex+S (jt_h_unit_enumeration)=(1)) -> (((((exists fs_h_jt_unit_enumerationfirstcode. fs_h_jt_unit_enumerationfirstcode + S (jt_b_unit_enumeration) = S ((S (jt_i_unit_enumeration)) * 0)) /\ exists fs_q_jt_unit_enumerationfirstcode. 0 = fs_q_jt_unit_enumerationfirstcode * S ((S (jt_i_unit_enumeration)) * 0) + (jt_b_unit_enumeration))) /\ (((exists fs_h_jt_unit_enumerationfirstscale. fs_h_jt_unit_enumerationfirstscale + S (jt_c_unit_enumeration) = S ((S (jt_i_unit_enumeration)) * 0)) /\ exists fs_q_jt_unit_enumerationfirstscale. 0 = fs_q_jt_unit_enumerationfirstscale * S ((S (jt_i_unit_enumeration)) * 0) + (jt_c_unit_enumeration))))) -> (((((exists fs_h_jt_unit_enumerationsecondcode. fs_h_jt_unit_enumerationsecondcode + S (jt_d_unit_enumeration) = S ((S (jt_h_unit_enumeration)) * 0)) /\ exists fs_q_jt_unit_enumerationsecondcode. 0 = fs_q_jt_unit_enumerationsecondcode * S ((S (jt_h_unit_enumeration)) * 0) + (jt_d_unit_enumeration))) /\ (((exists fs_h_jt_unit_enumerationsecondscale. fs_h_jt_unit_enumerationsecondscale + S (jt_e_unit_enumeration) = S ((S (jt_h_unit_enumeration)) * 0)) /\ exists fs_q_jt_unit_enumerationsecondscale. 0 = fs_q_jt_unit_enumerationsecondscale * S ((S (jt_h_unit_enumeration)) * 0) + (jt_e_unit_enumeration))))) -> (forall jt_index_unit_enumerationsame jt_left_unit_enumerationsame jt_right_unit_enumerationsame. (exists jt_gap_unit_enumerationsameindex. jt_gap_unit_enumerationsameindex+S (jt_index_unit_enumerationsame)=(k)) -> (((exists fs_h_jt_unit_enumerationsameleft. fs_h_jt_unit_enumerationsameleft + S (jt_left_unit_enumerationsame) = S ((S (jt_index_unit_enumerationsame)) * jt_c_unit_enumeration)) /\ exists fs_q_jt_unit_enumerationsameleft. jt_b_unit_enumeration = fs_q_jt_unit_enumerationsameleft * S ((S (jt_index_unit_enumerationsame)) * jt_c_unit_enumeration) + (jt_left_unit_enumerationsame))) -> (((exists fs_h_jt_unit_enumerationsameright. fs_h_jt_unit_enumerationsameright + S (jt_right_unit_enumerationsame) = S ((S (jt_index_unit_enumerationsame)) * jt_e_unit_enumeration)) /\ exists fs_q_jt_unit_enumerationsameright. jt_d_unit_enumeration = fs_q_jt_unit_enumerationsameright * S ((S (jt_index_unit_enumerationsame)) * jt_e_unit_enumeration) + (jt_right_unit_enumerationsame))) -> jt_left_unit_enumerationsame=jt_right_unit_enumerationsame) -> jt_i_unit_enumeration=jt_h_unit_enumeration)))))

Complete tactic proof in conservative notation

All 64 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

64 script commands · 23 reading checkpoints · 0 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
jordan zero tuple bounded onejordan primitive tuple modulus onejordan tuples bounded one equal
01Fix variables and assumptionsL1–1

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

  1. L1
    intro k
02Separate the logical casesL2–2

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

  1. L2
    split
03Fix variables and assumptionsL3–4

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

  1. L3
    intro i
  2. L4
    intro hi
04Construct an explicit witnessL5–6

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

  1. L5
    exists 0
  2. L6
    exists 0
05Separate the logical casesL7–8

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

  1. L7
    split
  2. L8
    split
06Use earlier factsL9–12

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

  1. L9
    specialize finite_beta_zero_code (i)
  2. L10
    apply finite_beta_zero_code
  3. L11
    specialize finite_beta_zero_code (i)
  4. L12
    apply finite_beta_zero_code
07Separate the logical casesL13–13

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

  1. L13
    split
08Use earlier factsL14–19

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

  1. L14
    specialize jordan_zero_tuple_bounded_one (k)
  2. L15
    apply jordan_zero_tuple_bounded_one
  3. L16
    specialize jordan_primitive_tuple_modulus_one (0)
  4. L17
    specialize jordan_primitive_tuple_modulus_one (0)
  5. L18
    specialize jordan_primitive_tuple_modulus_one (k)
  6. L19
    apply jordan_primitive_tuple_modulus_one
09Separate the logical casesL20–20

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

  1. L20
    split
10Fix variables and assumptionsL21–24

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

  1. L21
    intro b
  2. L22
    intro c
  3. L23
    intro hBound
  4. L24
    intro hPrimitive
11Construct an explicit witnessL25–27

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

  1. L25
    exists 0
  2. L26
    exists 0
  3. L27
    exists 0
12Separate the logical casesL28–28

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

  1. L28
    split
13Construct an explicit witnessL29–29

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

  1. L29
    exists 0
14Calculate and transport equalitiesL30–30

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

  1. L30
    simp
15Separate the logical casesL31–32

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

  1. L31
    split
  2. L32
    split
16Use earlier factsL33–42

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

  1. L33
    specialize finite_beta_zero_code (0)
  2. L34
    apply finite_beta_zero_code
  3. L35
    specialize finite_beta_zero_code (0)
  4. L36
    apply finite_beta_zero_code
  5. L37
    specialize jordan_tuples_bounded_one_equal (b)
  6. L38
    specialize jordan_tuples_bounded_one_equal (c)
  7. L39
    specialize jordan_tuples_bounded_one_equal (0)
  8. L40
    specialize jordan_tuples_bounded_one_equal (0)
  9. L41
    specialize jordan_tuples_bounded_one_equal (k)
  10. L42
    apply jordan_tuples_bounded_one_equal
17Use earlier factsL43–45

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

  1. L43
    exact hBound
  2. L44
    specialize jordan_zero_tuple_bounded_one (k)
  3. L45
    apply jordan_zero_tuple_bounded_one
18Fix variables and assumptionsL46–55

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

  1. L46
    intro i
  2. L47
    intro h
  3. L48
    intro b
  4. L49
    intro c
  5. L50
    intro d
  6. L51
    intro e
  7. L52
    intro hi
  8. L53
    intro hh
  9. L54
    intro hFirst
  10. L55
    intro hSecond
19Fix variables and assumptionsL56–56

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

  1. L56
    intro hEqual
20Calculate and transport equalitiesL57–57

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

  1. L57
    trans 0
21Use earlier factsL58–60

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

  1. L58
    apply le_zero
  2. L59
    apply le_of_succ_le_succ
  3. L60
    exact hi
22Calculate and transport equalitiesL61–61

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

  1. L61
    symm
23Use earlier factsL62–64

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

  1. L62
    apply le_zero
  2. L63
    apply le_of_succ_le_succ
  3. L64
    exact hh

Library-wide reading audit

Original defined command ledger · 64 lines
  1. 0001intro k
  2. 0002split
  3. 0003intro i
  4. 0004intro hi
  5. 0005exists 0
  6. 0006exists 0
  7. 0007split
  8. 0008split
  9. 0009specialize finite_beta_zero_code (i)
  10. 0010apply finite_beta_zero_code
  11. 0011specialize finite_beta_zero_code (i)
  12. 0012apply finite_beta_zero_code
  13. 0013split
  14. 0014specialize jordan_zero_tuple_bounded_one (k)
  15. 0015apply jordan_zero_tuple_bounded_one
  16. 0016specialize jordan_primitive_tuple_modulus_one (0)
  17. 0017specialize jordan_primitive_tuple_modulus_one (0)
  18. 0018specialize jordan_primitive_tuple_modulus_one (k)
  19. 0019apply jordan_primitive_tuple_modulus_one
  20. 0020split
  21. 0021intro b
  22. 0022intro c
  23. 0023intro hBound
  24. 0024intro hPrimitive
  25. 0025exists 0
  26. 0026exists 0
  27. 0027exists 0
  28. 0028split
  29. 0029exists 0
  30. 0030simp
  31. 0031split
  32. 0032split
  33. 0033specialize finite_beta_zero_code (0)
  34. 0034apply finite_beta_zero_code
  35. 0035specialize finite_beta_zero_code (0)
  36. 0036apply finite_beta_zero_code
  37. 0037specialize jordan_tuples_bounded_one_equal (b)
  38. 0038specialize jordan_tuples_bounded_one_equal (c)
  39. 0039specialize jordan_tuples_bounded_one_equal (0)
  40. 0040specialize jordan_tuples_bounded_one_equal (0)
  41. 0041specialize jordan_tuples_bounded_one_equal (k)
  42. 0042apply jordan_tuples_bounded_one_equal
  43. 0043exact hBound
  44. 0044specialize jordan_zero_tuple_bounded_one (k)
  45. 0045apply jordan_zero_tuple_bounded_one
  46. 0046intro i
  47. 0047intro h
  48. 0048intro b
  49. 0049intro c
  50. 0050intro d
  51. 0051intro e
  52. 0052intro hi
  53. 0053intro hh
  54. 0054intro hFirst
  55. 0055intro hSecond
  56. 0056intro hEqual
  57. 0057trans 0
  58. 0058apply le_zero
  59. 0059apply le_of_succ_le_succ
  60. 0060exact hi
  61. 0061symm
  62. 0062apply le_zero
  63. 0063apply le_of_succ_le_succ
  64. 0064exact hh