FS000H · theorem body

four_square_absolute_difference_total

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Canonical signed totality yields a natural absolute difference for any ordered pair, without importing another candidate module.

historical independently replay-verified empty-context experiment; the experiment itself persisted no certificate and granted no release authority; current checked use follows separately sealed proof bundles; no Stable promotion.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

forall left right. exists magnitude. (left = right + magnitude \/ right = left + magnitude)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

none

In local proof propositions

none
Exact expanded first-order statement
forall left right. exists magnitude. (left = right + magnitude \/ right = left + magnitude)

Proof neighborhood

Direct theorem prerequisites

signed_balance_total · Alpha closed FS0002 signed_balance_absolute_exists

Direct theorem dependents

FS000J four_square_two_square_factor_total FS0013 four_square_conjugate_absolute_coordinates_total FS001Q four_square_descent_matching_parity_absolute_even

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

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

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)
signed balance absolute exists
01Fix variables and assumptionsL1–2

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

  1. L1
    intro left
  2. L2
    intro right
02Establish hbalanceL3–4

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

  1. L3
    have hbalance : exists code. (exists sb_pos_fs_difference sb_neg_fs_difference. (((code = 2 * sb_pos_fs_difference /\ sb_neg_fs_difference = 0) \/ exists sd_half_fs_difference. ((code = 2 * sd_half_fs_difference + 1 /\ sb_pos_fs_difference = 0) /\ sb_neg_fs_difference = S sd_half_fs_difference)) /\ (left) + sb_neg_fs_difference = (right) + sb_pos_fs_difference))
  2. L4
    apply signed_balance_total
03Separate the logical casesL5–5

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

  1. L5
    cases hbalance
04Use earlier factsL6–10

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

  1. L6
    specialize signed_balance_absolute_exists x
  2. L7
    specialize signed_balance_absolute_exists left
  3. L8
    specialize signed_balance_absolute_exists right
  4. L9
    apply signed_balance_absolute_exists
  5. L10
    exact hbalance_witness

Library-wide reading audit

Original defined command ledger · 10 lines
  1. 0001intro left
  2. 0002intro right
  3. 0003have hbalance : exists code. (exists sb_pos_fs_difference sb_neg_fs_difference. (((code = 2 * sb_pos_fs_difference /\ sb_neg_fs_difference = 0) \/ exists sd_half_fs_difference. ((code = 2 * sd_half_fs_difference + 1 /\ sb_pos_fs_difference = 0) /\ sb_neg_fs_difference = S sd_half_fs_difference)) /\ (left) + sb_neg_fs_difference = (right) + sb_pos_fs_difference))
  4. 0004apply signed_balance_total
  5. 0005cases hbalance
  6. 0006specialize signed_balance_absolute_exists x
  7. 0007specialize signed_balance_absolute_exists left
  8. 0008specialize signed_balance_absolute_exists right
  9. 0009apply signed_balance_absolute_exists
  10. 0010exact hbalance_witness