JT0057

jordan_tuple_bounded_one_entry_zero

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

Every decoded coordinate in a tuple bounded by one equals zero.

Exact expanded first-order arithmetic statement

forall b c k i a. (forall jt_index_unit_tuple. (exists jt_gap_unit_tupleindex. jt_gap_unit_tupleindex+S (jt_index_unit_tuple)=(k)) -> exists jt_value_unit_tuple. ((((exists fs_h_jt_unit_tupleat. fs_h_jt_unit_tupleat + S (jt_value_unit_tuple) = S ((S (jt_index_unit_tuple)) * c)) /\ exists fs_q_jt_unit_tupleat. b = fs_q_jt_unit_tupleat * S ((S (jt_index_unit_tuple)) * c) + (jt_value_unit_tuple))) /\ (exists jt_gap_unit_tuplevalue. jt_gap_unit_tuplevalue+S (jt_value_unit_tuple)=(1)))) -> (exists jt_gap_unit_index. jt_gap_unit_index+S (i)=(k)) -> (((exists fs_h_jt_unit_entry. fs_h_jt_unit_entry + S (a) = S ((S (i)) * c)) /\ exists fs_q_jt_unit_entry. b = fs_q_jt_unit_entry * S ((S (i)) * c) + (a))) -> (a=0)

Constructive proof overview

Generated structural guide

Every decoded coordinate in a tuple bounded by one equals zero.

The unchanged tactic script uses 3 declared prerequisites and contains 26 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_at_unique Alpha theorem; checked-use authorized le_zero Alpha theorem; checked-use authorized le_of_succ_le_succ Alpha theorem; checked-use authorized

Direct dependents

JT0059 jordan_tuples_bounded_one_equal

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

26 script commands · 6 reading checkpoints · 1 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.

01Fix variables and assumptionsL1–8

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro k
  4. L4
    intro i
  5. L5
    intro a
  6. L6
    intro hBound
  7. L7
    intro hi
  8. L8
    intro ha
02Establish hValueL9–12

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

  1. L9
    have hValue : exists z. ((((exists fs_h_jt_unit_value. fs_h_jt_unit_value + S (z) = S ((S (i)) * c)) /\ exists fs_q_jt_unit_value. b = fs_q_jt_unit_value * S ((S (i)) * c) + (z))) /\ (exists jt_gap_unit_bound. jt_gap_unit_bound+S (z)=(1)))
  2. L10
    specialize hBound (i)
  3. L11
    apply hBound
  4. L12
    exact hi
03Separate the logical casesL13–14

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

  1. L13
    cases hValue
  2. L14
    cases hValue_witness
04Calculate and transport equalitiesL15–15

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

  1. L15
    trans x
05Use earlier factsL16–25

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

  1. L16
    specialize beta_at_unique (b)
  2. L17
    specialize beta_at_unique (c)
  3. L18
    specialize beta_at_unique (i)
  4. L19
    specialize beta_at_unique (a)
  5. L20
    specialize beta_at_unique (x)
  6. L21
    apply beta_at_unique
  7. L22
    exact ha
  8. L23
    exact hValue_witness_left
  9. L24
    apply le_zero
  10. L25
    apply le_of_succ_le_succ
06Use earlier factsL26–26

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

  1. L26
    exact hValue_witness_right

Library-wide reading audit

Original exact command ledger · 26 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro k
  4. 0004intro i
  5. 0005intro a
  6. 0006intro hBound
  7. 0007intro hi
  8. 0008intro ha
  9. 0009have hValue : exists z. ((((exists fs_h_jt_unit_value. fs_h_jt_unit_value + S (z) = S ((S (i)) * c)) /\ exists fs_q_jt_unit_value. b = fs_q_jt_unit_value * S ((S (i)) * c) + (z))) /\ (exists jt_gap_unit_bound. jt_gap_unit_bound+S (z)=(1)))
  10. 0010specialize hBound (i)
  11. 0011apply hBound
  12. 0012exact hi
  13. 0013cases hValue
  14. 0014cases hValue_witness
  15. 0015trans x
  16. 0016specialize beta_at_unique (b)
  17. 0017specialize beta_at_unique (c)
  18. 0018specialize beta_at_unique (i)
  19. 0019specialize beta_at_unique (a)
  20. 0020specialize beta_at_unique (x)
  21. 0021apply beta_at_unique
  22. 0022exact ha
  23. 0023exact hValue_witness_left
  24. 0024apply le_zero
  25. 0025apply le_of_succ_le_succ
  26. 0026exact hValue_witness_right