JT0059

jordan_tuples_bounded_one_equal

Any two canonical tuples modulo one represent the same coordinate tuple.

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

∀ b. ∀ c. ∀ d. ∀ e. ∀ k. BetaPrefixInto(b,c,k,1) → BetaPrefixInto(d,e,k,1) → IntegerVectorZero(b,c,d,e,k)

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

Definition DAG

IntegerVectorZero(ab,ac,db,dc,l) · 1BetaPrefixInto(b,c,l,B) · 2

Actual proof prerequisites

jordan_tuple_bounded_one_entry_zero
Original expanded first-order statement 
forall b c d e k. (forall jt_index_unit_left. (exists jt_gap_unit_leftindex. jt_gap_unit_leftindex+S (jt_index_unit_left)=(k)) -> exists jt_value_unit_left. ((((exists fs_h_jt_unit_leftat. fs_h_jt_unit_leftat + S (jt_value_unit_left) = S ((S (jt_index_unit_left)) * c)) /\ exists fs_q_jt_unit_leftat. b = fs_q_jt_unit_leftat * S ((S (jt_index_unit_left)) * c) + (jt_value_unit_left))) /\ (exists jt_gap_unit_leftvalue. jt_gap_unit_leftvalue+S (jt_value_unit_left)=(1)))) -> (forall jt_index_unit_right. (exists jt_gap_unit_rightindex. jt_gap_unit_rightindex+S (jt_index_unit_right)=(k)) -> exists jt_value_unit_right. ((((exists fs_h_jt_unit_rightat. fs_h_jt_unit_rightat + S (jt_value_unit_right) = S ((S (jt_index_unit_right)) * e)) /\ exists fs_q_jt_unit_rightat. d = fs_q_jt_unit_rightat * S ((S (jt_index_unit_right)) * e) + (jt_value_unit_right))) /\ (exists jt_gap_unit_rightvalue. jt_gap_unit_rightvalue+S (jt_value_unit_right)=(1)))) -> (forall jt_index_unit_equal jt_left_unit_equal jt_right_unit_equal. (exists jt_gap_unit_equalindex. jt_gap_unit_equalindex+S (jt_index_unit_equal)=(k)) -> (((exists fs_h_jt_unit_equalleft. fs_h_jt_unit_equalleft + S (jt_left_unit_equal) = S ((S (jt_index_unit_equal)) * c)) /\ exists fs_q_jt_unit_equalleft. b = fs_q_jt_unit_equalleft * S ((S (jt_index_unit_equal)) * c) + (jt_left_unit_equal))) -> (((exists fs_h_jt_unit_equalright. fs_h_jt_unit_equalright + S (jt_right_unit_equal) = S ((S (jt_index_unit_equal)) * e)) /\ exists fs_q_jt_unit_equalright. d = fs_q_jt_unit_equalright * S ((S (jt_index_unit_equal)) * e) + (jt_right_unit_equal))) -> jt_left_unit_equal=jt_right_unit_equal)

Complete tactic proof in conservative notation

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

23 script commands · 6 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 (1)
jordan tuple bounded one entry zero
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro k
  6. L6
    intro hLeft
  7. L7
    intro hRight
  8. L8
    intro i
  9. L9
    intro a
  10. L10
    intro z
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hi
  2. L12
    intro ha
  3. L13
    intro hz
03Calculate and transport equalitiesL14–14

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

  1. L14
    trans 0
04Use earlier factsL15–18

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

  1. L15
    apply jordan_tuple_bounded_one_entry_zero
  2. L16
    exact hLeft
  3. L17
    exact hi
  4. L18
    exact ha
05Calculate and transport equalitiesL19–19

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

  1. L19
    symm
06Use earlier factsL20–23

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

  1. L20
    apply jordan_tuple_bounded_one_entry_zero
  2. L21
    exact hRight
  3. L22
    exact hi
  4. L23
    exact hz

Library-wide reading audit

Original defined command ledger · 23 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro k
  6. 0006intro hLeft
  7. 0007intro hRight
  8. 0008intro i
  9. 0009intro a
  10. 0010intro z
  11. 0011intro hi
  12. 0012intro ha
  13. 0013intro hz
  14. 0014trans 0
  15. 0015apply jordan_tuple_bounded_one_entry_zero
  16. 0016exact hLeft
  17. 0017exact hi
  18. 0018exact ha
  19. 0019symm
  20. 0020apply jordan_tuple_bounded_one_entry_zero
  21. 0021exact hRight
  22. 0022exact hi
  23. 0023exact hz