BT00WY

thirty_two_square_eq_twice_sixteen_times_thirty_two

Alpha body-checked · checked-use disabled

The root-32 square identity carried by the shallow factorization 16*32.

Exact expanded PA statement

32 * 32 = 2 * (16 * 32)

Structural proof guide

The root-32 square identity carried by the shallow factorization 16*32.

Direct prerequisites: scaled_factor_square_identity. The authored body proceeds by intermediate claims (1), closed numeral normalization (1).

Proof neighborhood

Direct dependencies

BT00WX scaled_factor_square_identity

Direct dependents

BT00X0 floor_sqrt_factorized_threshold_thirty_two

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001have hfactor : 32 = 2 * 16
  2. 0002norm_num
  3. 0003specialize scaled_factor_square_identity 2
  4. 0004specialize scaled_factor_square_identity 16
  5. 0005specialize scaled_factor_square_identity 32
  6. 0006apply scaled_factor_square_identity
  7. 0007exact hfactor