JT003D

jordan_enumeration_actual_value

Every actual decoded enumeration entry is bounded and primitive.

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. ∀ n. ∀ A. ∀ B. ∀ C. ∀ D. ∀ j. ∀ i. ∀ b. ∀ c. JordanTupleEnumeration(k,n,A,B,C,D,j) → Lt(i,j) → BetaAt(A,B,i,b) ∧ BetaAt(C,D,i,c) → BetaPrefixInto(b,c,k,n) ∧ JordanPrimitiveTuple(n,b,c,k)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 2JordanPrimitiveTuple(n,b,c,k) · 2JordanTupleEnumeration(k,n,B,C,D,E,j) · 1Lt(a,b) · 1BetaAt(b,c,i,x) · 4

Actual proof prerequisites

beta_at_unique · checked external prerequisite
Original expanded first-order statement 
forall k n A B C D j i b c. (((forall jt_i_actualenum. (exists jt_gap_actualenumsoundindex. jt_gap_actualenumsoundindex+S (jt_i_actualenum)=(j)) -> exists jt_b_actualenum jt_c_actualenum. ((((((exists fs_h_jt_actualenumsoundcode. fs_h_jt_actualenumsoundcode + S (jt_b_actualenum) = S ((S (jt_i_actualenum)) * B)) /\ exists fs_q_jt_actualenumsoundcode. A = fs_q_jt_actualenumsoundcode * S ((S (jt_i_actualenum)) * B) + (jt_b_actualenum))) /\ (((exists fs_h_jt_actualenumsoundscale. fs_h_jt_actualenumsoundscale + S (jt_c_actualenum) = S ((S (jt_i_actualenum)) * D)) /\ exists fs_q_jt_actualenumsoundscale. C = fs_q_jt_actualenumsoundscale * S ((S (jt_i_actualenum)) * D) + (jt_c_actualenum))))) /\ (((forall jt_index_actualenumbound. (exists jt_gap_actualenumboundindex. jt_gap_actualenumboundindex+S (jt_index_actualenumbound)=(k)) -> exists jt_value_actualenumbound. ((((exists fs_h_jt_actualenumboundat. fs_h_jt_actualenumboundat + S (jt_value_actualenumbound) = S ((S (jt_index_actualenumbound)) * jt_c_actualenum)) /\ exists fs_q_jt_actualenumboundat. jt_b_actualenum = fs_q_jt_actualenumboundat * S ((S (jt_index_actualenumbound)) * jt_c_actualenum) + (jt_value_actualenumbound))) /\ (exists jt_gap_actualenumboundvalue. jt_gap_actualenumboundvalue+S (jt_value_actualenumbound)=(n)))) /\ (forall jt_divisor_actualenumprimitive. (exists jt_factor_actualenumprimitivemodulus. (n)=(jt_divisor_actualenumprimitive)*jt_factor_actualenumprimitivemodulus) -> (forall jt_index_actualenumprimitivecoordinates jt_value_actualenumprimitivecoordinates. (exists jt_gap_actualenumprimitivecoordinatesindex. jt_gap_actualenumprimitivecoordinatesindex+S (jt_index_actualenumprimitivecoordinates)=(k)) -> (((exists fs_h_jt_actualenumprimitivecoordinatesat. fs_h_jt_actualenumprimitivecoordinatesat + S (jt_value_actualenumprimitivecoordinates) = S ((S (jt_index_actualenumprimitivecoordinates)) * jt_c_actualenum)) /\ exists fs_q_jt_actualenumprimitivecoordinatesat. jt_b_actualenum = fs_q_jt_actualenumprimitivecoordinatesat * S ((S (jt_index_actualenumprimitivecoordinates)) * jt_c_actualenum) + (jt_value_actualenumprimitivecoordinates))) -> (exists jt_factor_actualenumprimitivecoordinatesdivides. (jt_value_actualenumprimitivecoordinates)=(jt_divisor_actualenumprimitive)*jt_factor_actualenumprimitivecoordinatesdivides)) -> jt_divisor_actualenumprimitive=1))))) /\ (((forall jt_b_actualenum jt_c_actualenum. (forall jt_index_actualenuminputbound. (exists jt_gap_actualenuminputboundindex. jt_gap_actualenuminputboundindex+S (jt_index_actualenuminputbound)=(k)) -> exists jt_value_actualenuminputbound. ((((exists fs_h_jt_actualenuminputboundat. fs_h_jt_actualenuminputboundat + S (jt_value_actualenuminputbound) = S ((S (jt_index_actualenuminputbound)) * jt_c_actualenum)) /\ exists fs_q_jt_actualenuminputboundat. jt_b_actualenum = fs_q_jt_actualenuminputboundat * S ((S (jt_index_actualenuminputbound)) * jt_c_actualenum) + (jt_value_actualenuminputbound))) /\ (exists jt_gap_actualenuminputboundvalue. jt_gap_actualenuminputboundvalue+S (jt_value_actualenuminputbound)=(n)))) -> (forall jt_divisor_actualenuminputprimitive. (exists jt_factor_actualenuminputprimitivemodulus. (n)=(jt_divisor_actualenuminputprimitive)*jt_factor_actualenuminputprimitivemodulus) -> (forall jt_index_actualenuminputprimitivecoordinates jt_value_actualenuminputprimitivecoordinates. (exists jt_gap_actualenuminputprimitivecoordinatesindex. jt_gap_actualenuminputprimitivecoordinatesindex+S (jt_index_actualenuminputprimitivecoordinates)=(k)) -> (((exists fs_h_jt_actualenuminputprimitivecoordinatesat. fs_h_jt_actualenuminputprimitivecoordinatesat + S (jt_value_actualenuminputprimitivecoordinates) = S ((S (jt_index_actualenuminputprimitivecoordinates)) * jt_c_actualenum)) /\ exists fs_q_jt_actualenuminputprimitivecoordinatesat. jt_b_actualenum = fs_q_jt_actualenuminputprimitivecoordinatesat * S ((S (jt_index_actualenuminputprimitivecoordinates)) * jt_c_actualenum) + (jt_value_actualenuminputprimitivecoordinates))) -> (exists jt_factor_actualenuminputprimitivecoordinatesdivides. (jt_value_actualenuminputprimitivecoordinates)=(jt_divisor_actualenuminputprimitive)*jt_factor_actualenuminputprimitivecoordinatesdivides)) -> jt_divisor_actualenuminputprimitive=1) -> exists jt_i_actualenum jt_d_actualenum jt_e_actualenum. ((exists jt_gap_actualenumcompleteindex. jt_gap_actualenumcompleteindex+S (jt_i_actualenum)=(j)) /\ (((((((exists fs_h_jt_actualenumcompletecode. fs_h_jt_actualenumcompletecode + S (jt_d_actualenum) = S ((S (jt_i_actualenum)) * B)) /\ exists fs_q_jt_actualenumcompletecode. A = fs_q_jt_actualenumcompletecode * S ((S (jt_i_actualenum)) * B) + (jt_d_actualenum))) /\ (((exists fs_h_jt_actualenumcompletescale. fs_h_jt_actualenumcompletescale + S (jt_e_actualenum) = S ((S (jt_i_actualenum)) * D)) /\ exists fs_q_jt_actualenumcompletescale. C = fs_q_jt_actualenumcompletescale * S ((S (jt_i_actualenum)) * D) + (jt_e_actualenum))))) /\ (forall jt_index_actualenumrepresented jt_left_actualenumrepresented jt_right_actualenumrepresented. (exists jt_gap_actualenumrepresentedindex. jt_gap_actualenumrepresentedindex+S (jt_index_actualenumrepresented)=(k)) -> (((exists fs_h_jt_actualenumrepresentedleft. fs_h_jt_actualenumrepresentedleft + S (jt_left_actualenumrepresented) = S ((S (jt_index_actualenumrepresented)) * jt_c_actualenum)) /\ exists fs_q_jt_actualenumrepresentedleft. jt_b_actualenum = fs_q_jt_actualenumrepresentedleft * S ((S (jt_index_actualenumrepresented)) * jt_c_actualenum) + (jt_left_actualenumrepresented))) -> (((exists fs_h_jt_actualenumrepresentedright. fs_h_jt_actualenumrepresentedright + S (jt_right_actualenumrepresented) = S ((S (jt_index_actualenumrepresented)) * jt_e_actualenum)) /\ exists fs_q_jt_actualenumrepresentedright. jt_d_actualenum = fs_q_jt_actualenumrepresentedright * S ((S (jt_index_actualenumrepresented)) * jt_e_actualenum) + (jt_right_actualenumrepresented))) -> jt_left_actualenumrepresented=jt_right_actualenumrepresented))))) /\ (forall jt_i_actualenum jt_h_actualenum jt_b_actualenum jt_c_actualenum jt_d_actualenum jt_e_actualenum. (exists jt_gap_actualenumfirstindex. jt_gap_actualenumfirstindex+S (jt_i_actualenum)=(j)) -> (exists jt_gap_actualenumsecondindex. jt_gap_actualenumsecondindex+S (jt_h_actualenum)=(j)) -> (((((exists fs_h_jt_actualenumfirstcode. fs_h_jt_actualenumfirstcode + S (jt_b_actualenum) = S ((S (jt_i_actualenum)) * B)) /\ exists fs_q_jt_actualenumfirstcode. A = fs_q_jt_actualenumfirstcode * S ((S (jt_i_actualenum)) * B) + (jt_b_actualenum))) /\ (((exists fs_h_jt_actualenumfirstscale. fs_h_jt_actualenumfirstscale + S (jt_c_actualenum) = S ((S (jt_i_actualenum)) * D)) /\ exists fs_q_jt_actualenumfirstscale. C = fs_q_jt_actualenumfirstscale * S ((S (jt_i_actualenum)) * D) + (jt_c_actualenum))))) -> (((((exists fs_h_jt_actualenumsecondcode. fs_h_jt_actualenumsecondcode + S (jt_d_actualenum) = S ((S (jt_h_actualenum)) * B)) /\ exists fs_q_jt_actualenumsecondcode. A = fs_q_jt_actualenumsecondcode * S ((S (jt_h_actualenum)) * B) + (jt_d_actualenum))) /\ (((exists fs_h_jt_actualenumsecondscale. fs_h_jt_actualenumsecondscale + S (jt_e_actualenum) = S ((S (jt_h_actualenum)) * D)) /\ exists fs_q_jt_actualenumsecondscale. C = fs_q_jt_actualenumsecondscale * S ((S (jt_h_actualenum)) * D) + (jt_e_actualenum))))) -> (forall jt_index_actualenumsame jt_left_actualenumsame jt_right_actualenumsame. (exists jt_gap_actualenumsameindex. jt_gap_actualenumsameindex+S (jt_index_actualenumsame)=(k)) -> (((exists fs_h_jt_actualenumsameleft. fs_h_jt_actualenumsameleft + S (jt_left_actualenumsame) = S ((S (jt_index_actualenumsame)) * jt_c_actualenum)) /\ exists fs_q_jt_actualenumsameleft. jt_b_actualenum = fs_q_jt_actualenumsameleft * S ((S (jt_index_actualenumsame)) * jt_c_actualenum) + (jt_left_actualenumsame))) -> (((exists fs_h_jt_actualenumsameright. fs_h_jt_actualenumsameright + S (jt_right_actualenumsame) = S ((S (jt_index_actualenumsame)) * jt_e_actualenum)) /\ exists fs_q_jt_actualenumsameright. jt_d_actualenum = fs_q_jt_actualenumsameright * S ((S (jt_index_actualenumsame)) * jt_e_actualenum) + (jt_right_actualenumsame))) -> jt_left_actualenumsame=jt_right_actualenumsame) -> jt_i_actualenum=jt_h_actualenum))))) -> (exists jt_gap_actualindex. jt_gap_actualindex+S (i)=(j)) -> (((((exists fs_h_jt_actualentrycode. fs_h_jt_actualentrycode + S (b) = S ((S (i)) * B)) /\ exists fs_q_jt_actualentrycode. A = fs_q_jt_actualentrycode * S ((S (i)) * B) + (b))) /\ (((exists fs_h_jt_actualentryscale. fs_h_jt_actualentryscale + S (c) = S ((S (i)) * D)) /\ exists fs_q_jt_actualentryscale. C = fs_q_jt_actualentryscale * S ((S (i)) * D) + (c))))) -> ((forall jt_index_actualbound. (exists jt_gap_actualboundindex. jt_gap_actualboundindex+S (jt_index_actualbound)=(k)) -> exists jt_value_actualbound. ((((exists fs_h_jt_actualboundat. fs_h_jt_actualboundat + S (jt_value_actualbound) = S ((S (jt_index_actualbound)) * c)) /\ exists fs_q_jt_actualboundat. b = fs_q_jt_actualboundat * S ((S (jt_index_actualbound)) * c) + (jt_value_actualbound))) /\ (exists jt_gap_actualboundvalue. jt_gap_actualboundvalue+S (jt_value_actualbound)=(n)))) /\ (forall jt_divisor_actualprimitive. (exists jt_factor_actualprimitivemodulus. (n)=(jt_divisor_actualprimitive)*jt_factor_actualprimitivemodulus) -> (forall jt_index_actualprimitivecoordinates jt_value_actualprimitivecoordinates. (exists jt_gap_actualprimitivecoordinatesindex. jt_gap_actualprimitivecoordinatesindex+S (jt_index_actualprimitivecoordinates)=(k)) -> (((exists fs_h_jt_actualprimitivecoordinatesat. fs_h_jt_actualprimitivecoordinatesat + S (jt_value_actualprimitivecoordinates) = S ((S (jt_index_actualprimitivecoordinates)) * c)) /\ exists fs_q_jt_actualprimitivecoordinatesat. b = fs_q_jt_actualprimitivecoordinatesat * S ((S (jt_index_actualprimitivecoordinates)) * c) + (jt_value_actualprimitivecoordinates))) -> (exists jt_factor_actualprimitivecoordinatesdivides. (jt_value_actualprimitivecoordinates)=(jt_divisor_actualprimitive)*jt_factor_actualprimitivecoordinatesdivides)) -> jt_divisor_actualprimitive=1))

Complete tactic proof in conservative notation

All 52 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

52 script commands · 12 reading checkpoints · 3 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro k
  2. L2
    intro n
  3. L3
    intro A
  4. L4
    intro B
  5. L5
    intro C
  6. L6
    intro D
  7. L7
    intro j
  8. L8
    intro i
  9. L9
    intro b
  10. L10
    intro c
02Fix variables and assumptionsL11–13

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

  1. L11
    intro he
  2. L12
    intro hi
  3. L13
    intro hentry
03Separate the logical casesL14–16

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

  1. L14
    cases he
  2. L15
    cases he_right
  3. L16
    cases hentry
04Establish hvL17–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply he left.

  1. L17
    have hv : ∃ d. ∃ e. BetaAt(A,B,i,d) ∧ BetaAt(C,D,i,e) ∧ (BetaPrefixInto(d,e,k,n) ∧ JordanPrimitiveTuple(n,d,e,k))Definitions: BetaAt(A,B,i,d)BetaAt(C,D,i,e)BetaPrefixInto(d,e,k,n)JordanPrimitiveTuple(n,d,e,k)Original native command in the exact edition
  2. L18
    specialize he_left (i)
  3. L19
    apply he_left
  4. L20
    exact hi
05Separate the logical casesL21–25

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

  1. L21
    cases hv
  2. L22
    cases hv_witness
  3. L23
    cases hv_witness_witness
  4. L24
    cases hv_witness_witness_right
  5. L25
    cases hv_witness_witness_left
06Establish hbL26–34

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

  1. L26
    have hb : x=b
  2. L27
    specialize beta_at_unique (A)
  3. L28
    specialize beta_at_unique (B)
  4. L29
    specialize beta_at_unique (i)
  5. L30
    specialize beta_at_unique (x)
  6. L31
    specialize beta_at_unique (b)
  7. L32
    apply beta_at_unique
  8. L33
    exact hv_witness_witness_left_left
  9. L34
    exact hentry_left
07Establish hcL35–43

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

  1. L35
    have hc : x1=c
  2. L36
    specialize beta_at_unique (C)
  3. L37
    specialize beta_at_unique (D)
  4. L38
    specialize beta_at_unique (i)
  5. L39
    specialize beta_at_unique (x1)
  6. L40
    specialize beta_at_unique (c)
  7. L41
    apply beta_at_unique
  8. L42
    exact hv_witness_witness_left_right
  9. L43
    exact hentry_right
08Separate the logical casesL44–44

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

  1. L44
    split
09Calculate and transport equalitiesL45–47

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

  1. L45
    rewrite hb at hv_witness_witness_right_left
  2. L46
    rewrite hc at hv_witness_witness_right_left
  3. L47
    rewrite hc at hv_witness_witness_right_left
10Use earlier factsL48–48

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

  1. L48
    exact hv_witness_witness_right_left
11Calculate and transport equalitiesL49–51

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

  1. L49
    rewrite hb at hv_witness_witness_right_right
  2. L50
    rewrite hc at hv_witness_witness_right_right
  3. L51
    rewrite hc at hv_witness_witness_right_right
12Use earlier factsL52–52

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

  1. L52
    exact hv_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 52 lines
  1. 0001intro k
  2. 0002intro n
  3. 0003intro A
  4. 0004intro B
  5. 0005intro C
  6. 0006intro D
  7. 0007intro j
  8. 0008intro i
  9. 0009intro b
  10. 0010intro c
  11. 0011intro he
  12. 0012intro hi
  13. 0013intro hentry
  14. 0014cases he
  15. 0015cases he_right
  16. 0016cases hentry
  17. 0017have hv : ∃ d. ∃ e. BetaAt(A,B,i,d) ∧ BetaAt(C,D,i,e) ∧ (BetaPrefixInto(d,e,k,n) ∧ JordanPrimitiveTuple(n,d,e,k))
  18. 0018specialize he_left (i)
  19. 0019apply he_left
  20. 0020exact hi
  21. 0021cases hv
  22. 0022cases hv_witness
  23. 0023cases hv_witness_witness
  24. 0024cases hv_witness_witness_right
  25. 0025cases hv_witness_witness_left
  26. 0026have hb : x=b
  27. 0027specialize beta_at_unique (A)
  28. 0028specialize beta_at_unique (B)
  29. 0029specialize beta_at_unique (i)
  30. 0030specialize beta_at_unique (x)
  31. 0031specialize beta_at_unique (b)
  32. 0032apply beta_at_unique
  33. 0033exact hv_witness_witness_left_left
  34. 0034exact hentry_left
  35. 0035have hc : x1=c
  36. 0036specialize beta_at_unique (C)
  37. 0037specialize beta_at_unique (D)
  38. 0038specialize beta_at_unique (i)
  39. 0039specialize beta_at_unique (x1)
  40. 0040specialize beta_at_unique (c)
  41. 0041apply beta_at_unique
  42. 0042exact hv_witness_witness_left_right
  43. 0043exact hentry_right
  44. 0044split
  45. 0045rewrite hb at hv_witness_witness_right_left
  46. 0046rewrite hc at hv_witness_witness_right_left
  47. 0047rewrite hc at hv_witness_witness_right_left
  48. 0048exact hv_witness_witness_right_left
  49. 0049rewrite hb at hv_witness_witness_right_right
  50. 0050rewrite hc at hv_witness_witness_right_right
  51. 0051rewrite hc at hv_witness_witness_right_right
  52. 0052exact hv_witness_witness_right_right