JT0028

jordan_tuple_representatives_exists

Extract an actual finite coordinate-representative box from the existing beta recoding theorem.

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. ∃ c. ∃ T. JordanTupleRepresentatives(k,n,c,T)

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

Definition DAG

UniformBetaPrefixBox(c,T,l,B) · 1BetaPrefixEqual(b,c,d,e,l) · 1JordanTupleRepresentatives(k,n,c,T) · 1Lt(a,b) · 1

Actual proof prerequisites

matrix_rank_uniform_beta_prefix_box_exists · checked external prerequisitejordan_tuple_prefix_equal
Original expanded first-order statement 
forall k n. exists c T. forall jt_code_representativesexists jt_scale_representativesexists. (forall jt_index_representativesexistsbound. (exists jt_gap_representativesexistsboundindex. jt_gap_representativesexistsboundindex+S (jt_index_representativesexistsbound)=(k)) -> exists jt_value_representativesexistsbound. ((((exists fs_h_jt_representativesexistsboundat. fs_h_jt_representativesexistsboundat + S (jt_value_representativesexistsbound) = S ((S (jt_index_representativesexistsbound)) * jt_scale_representativesexists)) /\ exists fs_q_jt_representativesexistsboundat. jt_code_representativesexists = fs_q_jt_representativesexistsboundat * S ((S (jt_index_representativesexistsbound)) * jt_scale_representativesexists) + (jt_value_representativesexistsbound))) /\ (exists jt_gap_representativesexistsboundvalue. jt_gap_representativesexistsboundvalue+S (jt_value_representativesexistsbound)=(n)))) -> exists jt_representative_representativesexists. ((exists jt_gap_representativesexistsindex. jt_gap_representativesexistsindex+S (jt_representative_representativesexists)=(T)) /\ (forall jt_index_representativesexistsequal jt_left_representativesexistsequal jt_right_representativesexistsequal. (exists jt_gap_representativesexistsequalindex. jt_gap_representativesexistsequalindex+S (jt_index_representativesexistsequal)=(k)) -> (((exists fs_h_jt_representativesexistsequalleft. fs_h_jt_representativesexistsequalleft + S (jt_left_representativesexistsequal) = S ((S (jt_index_representativesexistsequal)) * jt_scale_representativesexists)) /\ exists fs_q_jt_representativesexistsequalleft. jt_code_representativesexists = fs_q_jt_representativesexistsequalleft * S ((S (jt_index_representativesexistsequal)) * jt_scale_representativesexists) + (jt_left_representativesexistsequal))) -> (((exists fs_h_jt_representativesexistsequalright. fs_h_jt_representativesexistsequalright + S (jt_right_representativesexistsequal) = S ((S (jt_index_representativesexistsequal)) * c)) /\ exists fs_q_jt_representativesexistsequalright. jt_representative_representativesexists = fs_q_jt_representativesexistsequalright * S ((S (jt_index_representativesexistsequal)) * c) + (jt_right_representativesexistsequal))) -> jt_left_representativesexistsequal=jt_right_representativesexistsequal))

Complete tactic proof in conservative notation

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

31 script commands · 10 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.

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 (1)
jordan tuple prefix equal
01Fix variables and assumptionsL1–2

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

  1. L1
    intro k
  2. L2
    intro n
02Establish hboxL3–6

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix rank uniform beta prefix box exists.

  1. L3
    have hbox : ∃ c. ∃ T. UniformBetaPrefixBox(c,T,k,n)Definitions: UniformBetaPrefixBox(c,T,k,n)Original native command in the exact edition
  2. L4
    specialize matrix_rank_uniform_beta_prefix_box_exists (k)
  3. L5
    specialize matrix_rank_uniform_beta_prefix_box_exists (n)
  4. L6
    apply matrix_rank_uniform_beta_prefix_box_exists
03Separate the logical casesL7–9

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

  1. L7
    cases hbox
  2. L8
    cases hbox_witness
  3. L9
    cases hbox_witness_witness
04Construct an explicit witnessL10–11

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

  1. L10
    exists x
  2. L11
    exists x1
05Fix variables and assumptionsL12–14

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

  1. L12
    intro b
  2. L13
    intro e
  3. L14
    intro hb
06Establish hzL15–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hbox witness witness right.

  1. L15
    have hz : ∃ z. Lt(z,x1) ∧ BetaPrefixEqual(b,e,z,x,k)Definitions: Lt(z,x1)BetaPrefixEqual(b,e,z,x,k)Original native command in the exact edition
  2. L16
    specialize hbox_witness_witness_right (b)
  3. L17
    specialize hbox_witness_witness_right (e)
  4. L18
    apply hbox_witness_witness_right
  5. L19
    exact hb
07Separate the logical casesL20–21

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

  1. L20
    cases hz
  2. L21
    cases hz_witness
08Construct an explicit witnessL22–22

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

  1. L22
    exists x2
09Separate the logical casesL23–23

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

  1. L23
    split
10Use earlier factsL24–31

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

  1. L24
    exact hz_witness_left
  2. L25
    specialize jordan_tuple_prefix_equal (b)
  3. L26
    specialize jordan_tuple_prefix_equal (e)
  4. L27
    specialize jordan_tuple_prefix_equal (x2)
  5. L28
    specialize jordan_tuple_prefix_equal (x)
  6. L29
    specialize jordan_tuple_prefix_equal (k)
  7. L30
    apply jordan_tuple_prefix_equal
  8. L31
    exact hz_witness_right

Library-wide reading audit

Original defined command ledger · 31 lines
  1. 0001intro k
  2. 0002intro n
  3. 0003have hbox : ∃ c. ∃ T. UniformBetaPrefixBox(c,T,k,n)
  4. 0004specialize matrix_rank_uniform_beta_prefix_box_exists (k)
  5. 0005specialize matrix_rank_uniform_beta_prefix_box_exists (n)
  6. 0006apply matrix_rank_uniform_beta_prefix_box_exists
  7. 0007cases hbox
  8. 0008cases hbox_witness
  9. 0009cases hbox_witness_witness
  10. 0010exists x
  11. 0011exists x1
  12. 0012intro b
  13. 0013intro e
  14. 0014intro hb
  15. 0015have hz : ∃ z. Lt(z,x1) ∧ BetaPrefixEqual(b,e,z,x,k)
  16. 0016specialize hbox_witness_witness_right (b)
  17. 0017specialize hbox_witness_witness_right (e)
  18. 0018apply hbox_witness_witness_right
  19. 0019exact hb
  20. 0020cases hz
  21. 0021cases hz_witness
  22. 0022exists x2
  23. 0023split
  24. 0024exact hz_witness_left
  25. 0025specialize jordan_tuple_prefix_equal (b)
  26. 0026specialize jordan_tuple_prefix_equal (e)
  27. 0027specialize jordan_tuple_prefix_equal (x2)
  28. 0028specialize jordan_tuple_prefix_equal (x)
  29. 0029specialize jordan_tuple_prefix_equal (k)
  30. 0030apply jordan_tuple_prefix_equal
  31. 0031exact hz_witness_right