TS002K · theorem body

beta_witnessed_two_square_prefix_implies_pointwise

dependency-curried kernel-checked candidate body; not enrolled in Alpha or Stable

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.

Statement with defined notation

∀ b. ∀ c. ∀ l. (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ y = z · z + n · n) → ∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → ∃ z. ∃ n. y = z · z + n · n

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

PD0002 Lt PD0013 BetaAt

In local proof propositions

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

Proof neighborhood

Direct theorem prerequisites

beta_at_unique · Stable closed

Direct theorem dependents

TS002N beta_witnessed_two_square_factor_product

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : ∃ p. ∃ x. ∃ y. BetaAt(b,c,i,p) ∧ p = x · x + y · yDefinitions: BetaAt(b,c,i,p)Original native command in the exact edition
  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 defined 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 : ∃ p. ∃ x. ∃ y. BetaAt(b,c,i,p) ∧ p = x · x + y · y
    Exact native replay linehave 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