JT0028

jordan_tuple_representatives_exists

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 31 exact native proof lines.

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

Proof neighborhood

Direct dependencies

matrix_rank_uniform_beta_prefix_box_exists Alpha theorem; checked-use authorized JT001E jordan_tuple_prefix_equal

Direct dependents

JT0029 jordan_totient_exists

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

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.

Named ingredients (1)
jordan tuple prefix equal

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–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
  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: BetaPrefixEqualLt
  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 exact command ledger · 31 lines
  1. 0001intro k
  2. 0002intro n
  3. 0003have hbox : exists c T. ((~(T=0)) /\ (forall b e. (forall jt_index_boxinput. (exists jt_gap_boxinputindex. jt_gap_boxinputindex+S (jt_index_boxinput)=(k)) -> exists jt_value_boxinput. ((((exists fs_h_jt_boxinputat. fs_h_jt_boxinputat + S (jt_value_boxinput) = S ((S (jt_index_boxinput)) * e)) /\ exists fs_q_jt_boxinputat. b = fs_q_jt_boxinputat * S ((S (jt_index_boxinput)) * e) + (jt_value_boxinput))) /\ (exists jt_gap_boxinputvalue. jt_gap_boxinputvalue+S (jt_value_boxinput)=(n)))) -> exists z. ((exists jt_gap_boxindex. jt_gap_boxindex+S (z)=(T)) /\ (forall jt_index_boxprefix jt_value_boxprefix. (exists jt_gap_boxprefixindex. jt_gap_boxprefixindex+S (jt_index_boxprefix)=(k)) -> (((exists fs_h_jt_boxprefixold. fs_h_jt_boxprefixold + S (jt_value_boxprefix) = S ((S (jt_index_boxprefix)) * e)) /\ exists fs_q_jt_boxprefixold. b = fs_q_jt_boxprefixold * S ((S (jt_index_boxprefix)) * e) + (jt_value_boxprefix))) -> (((exists fs_h_jt_boxprefixnew. fs_h_jt_boxprefixnew + S (jt_value_boxprefix) = S ((S (jt_index_boxprefix)) * c)) /\ exists fs_q_jt_boxprefixnew. z = fs_q_jt_boxprefixnew * S ((S (jt_index_boxprefix)) * c) + (jt_value_boxprefix)))))))
  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 : exists z. ((exists jt_gap_recodeindex. jt_gap_recodeindex+S (z)=(x1)) /\ (forall jt_index_recodeprefix jt_value_recodeprefix. (exists jt_gap_recodeprefixindex. jt_gap_recodeprefixindex+S (jt_index_recodeprefix)=(k)) -> (((exists fs_h_jt_recodeprefixold. fs_h_jt_recodeprefixold + S (jt_value_recodeprefix) = S ((S (jt_index_recodeprefix)) * e)) /\ exists fs_q_jt_recodeprefixold. b = fs_q_jt_recodeprefixold * S ((S (jt_index_recodeprefix)) * e) + (jt_value_recodeprefix))) -> (((exists fs_h_jt_recodeprefixnew. fs_h_jt_recodeprefixnew + S (jt_value_recodeprefix) = S ((S (jt_index_recodeprefix)) * x)) /\ exists fs_q_jt_recodeprefixnew. z = fs_q_jt_recodeprefixnew * S ((S (jt_index_recodeprefix)) * x) + (jt_value_recodeprefix)))))
  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