TS002K

beta_witnessed_two_square_prefix_implies_pointwise

Dependency-curried candidate body; not Alpha-enrolled; no checked-use authority

Existentially witnessed represented entries imply representation of every actual decoded value by beta uniqueness.

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.

Exact expanded first-order arithmetic statement

forall b c l. (forall ftsf_index_witness_source. (exists ftsf_gap_witness_source_bound. ftsf_gap_witness_source_bound + S ftsf_index_witness_source = (l)) -> exists ftsf_factor_witness_source ftsf_coordinate_first_witness_source ftsf_coordinate_second_witness_source. ((((exists ff_h_ftsf_witness_source_entry. ff_h_ftsf_witness_source_entry + S (ftsf_factor_witness_source) = S ((S (ftsf_index_witness_source)) * c)) /\ exists ff_q_ftsf_witness_source_entry. b = ff_q_ftsf_witness_source_entry * S ((S (ftsf_index_witness_source)) * c) + (ftsf_factor_witness_source))) /\ ftsf_factor_witness_source = ftsf_coordinate_first_witness_source * ftsf_coordinate_first_witness_source + ftsf_coordinate_second_witness_source * ftsf_coordinate_second_witness_source)) -> (forall ftsf_index_witness_result ftsf_factor_witness_result. (exists ftsf_gap_witness_result_bound. ftsf_gap_witness_result_bound + S ftsf_index_witness_result = (l)) -> (((exists ff_h_ftsf_witness_result_entry. ff_h_ftsf_witness_result_entry + S (ftsf_factor_witness_result) = S ((S (ftsf_index_witness_result)) * c)) /\ exists ff_q_ftsf_witness_result_entry. b = ff_q_ftsf_witness_result_entry * S ((S (ftsf_index_witness_result)) * c) + (ftsf_factor_witness_result))) -> (exists ftsf_first_witness_result_representation ftsf_second_witness_result_representation. (ftsf_factor_witness_result) = ftsf_first_witness_result_representation * ftsf_first_witness_result_representation + ftsf_second_witness_result_representation * ftsf_second_witness_result_representation))

Constructive proof overview

Generated structural guide

Existentially witnessed represented entries imply representation of every actual decoded value by beta uniqueness.

The unchanged tactic script uses 1 declared prerequisite and contains 29 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

beta_at_unique Stable theorem; checked-use authorized

Direct dependents

TS002N beta_witnessed_two_square_factor_product

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This dependency-curried candidate body does not grant checked theorem use or Stable membership.

Read the argument

Proof checkpoints

29 script commands · 8 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.

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 l
  4. L4
    intro hwitnessed
  5. L5
    intro i
  6. L6
    intro a
  7. L7
    intro hi
  8. L8
    intro ha
02Use earlier factsL9–9

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

  1. L9
    specialize hwitnessed i
03Establish hfactorL10–12

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

  1. L10
    have hfactor : exists p x y. ((((exists ff_h_ftsf_witnessed_local. ff_h_ftsf_witnessed_local + S (p) = S ((S (i)) * c)) /\ exists ff_q_ftsf_witnessed_local. b = ff_q_ftsf_witnessed_local * S ((S (i)) * c) + (p))) /\ p = x * x + y * y)
  2. L11
    apply hwitnessed
  3. L12
    exact hi
04Separate the logical casesL13–16

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

  1. L13
    cases hfactor
  2. L14
    cases hfactor_witness
  3. L15
    cases hfactor_witness_witness
  4. L16
    cases hfactor_witness_witness_witness
05Establish hequalL17–25

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

  1. L17
    have hequal : a = x
  2. L18
    specialize beta_at_unique b
  3. L19
    specialize beta_at_unique c
  4. L20
    specialize beta_at_unique i
  5. L21
    specialize beta_at_unique a
  6. L22
    specialize beta_at_unique x
  7. L23
    apply beta_at_unique
  8. L24
    exact ha
  9. L25
    exact hfactor_witness_witness_witness_left
06Construct an explicit witnessL26–27

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

  1. L26
    exists x1
  2. L27
    exists x2
07Calculate and transport equalitiesL28–28

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

  1. L28
    rewrite hequal
08Use earlier factsL29–29

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

  1. L29
    exact hfactor_witness_witness_witness_right

Library-wide reading audit

Original exact command ledger · 29 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro hwitnessed
  5. 0005intro i
  6. 0006intro a
  7. 0007intro hi
  8. 0008intro ha
  9. 0009specialize hwitnessed i
  10. 0010have hfactor : exists p x y. ((((exists ff_h_ftsf_witnessed_local. ff_h_ftsf_witnessed_local + S (p) = S ((S (i)) * c)) /\ exists ff_q_ftsf_witnessed_local. b = ff_q_ftsf_witnessed_local * S ((S (i)) * c) + (p))) /\ p = x * x + y * y)
  11. 0011apply hwitnessed
  12. 0012exact hi
  13. 0013cases hfactor
  14. 0014cases hfactor_witness
  15. 0015cases hfactor_witness_witness
  16. 0016cases hfactor_witness_witness_witness
  17. 0017have hequal : a = x
  18. 0018specialize beta_at_unique b
  19. 0019specialize beta_at_unique c
  20. 0020specialize beta_at_unique i
  21. 0021specialize beta_at_unique a
  22. 0022specialize beta_at_unique x
  23. 0023apply beta_at_unique
  24. 0024exact ha
  25. 0025exact hfactor_witness_witness_witness_left
  26. 0026exists x1
  27. 0027exists x2
  28. 0028rewrite hequal
  29. 0029exact hfactor_witness_witness_witness_right