GF001B

gaussian_unit_iff_norm_one

The inverse-witness definition of Gaussian unit is equivalent to the independently defined squared norm being one.

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

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.

Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.

Exact theorem in conservative defined notation

∀ z. ∀ N. GNorm(z,N) → (GUnit(z) → N = 1) ∧ (N = 1 → GUnit(z))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

GNorm(z,n) · 1GUnit(z) · 2

Actual proof prerequisites

gaussian_unit_has_norm_onegaussian_norm_one_is_unitgaussian_norm_functional · checked external prerequisitegaussian_norm_value_transport
Original expanded first-order statement 
forall z N. (exists ge_norm_rp_unit_iff_norm ge_norm_rn_unit_iff_norm ge_norm_ip_unit_iff_norm ge_norm_in_unit_iff_norm. ((exists ge_representation_real_code_unit_iff_normrepresentation ge_representation_imaginary_code_unit_iff_normrepresentation. (((z) = ((ge_representation_real_code_unit_iff_normrepresentation) + (ge_representation_imaginary_code_unit_iff_normrepresentation)) * S ((ge_representation_real_code_unit_iff_normrepresentation) + (ge_representation_imaginary_code_unit_iff_normrepresentation)) + ((ge_representation_imaginary_code_unit_iff_normrepresentation) + (ge_representation_imaginary_code_unit_iff_normrepresentation))) /\ ((exists ge_balance_positive_unit_iff_normrepresentationreal ge_balance_negative_unit_iff_normrepresentationreal. (((((ge_representation_real_code_unit_iff_normrepresentation) = 2 * (ge_balance_positive_unit_iff_normrepresentationreal) /\ (ge_balance_negative_unit_iff_normrepresentationreal) = 0) \/ exists ge_signed_half_unit_iff_normrepresentationrealdecode. (((ge_representation_real_code_unit_iff_normrepresentation) = 2 * ge_signed_half_unit_iff_normrepresentationrealdecode + 1 /\ (ge_balance_positive_unit_iff_normrepresentationreal) = 0) /\ (ge_balance_negative_unit_iff_normrepresentationreal) = S ge_signed_half_unit_iff_normrepresentationrealdecode))) /\ ((ge_norm_rp_unit_iff_norm) + ge_balance_negative_unit_iff_normrepresentationreal = (ge_norm_rn_unit_iff_norm) + ge_balance_positive_unit_iff_normrepresentationreal))) /\ (exists ge_balance_positive_unit_iff_normrepresentationimaginary ge_balance_negative_unit_iff_normrepresentationimaginary. (((((ge_representation_imaginary_code_unit_iff_normrepresentation) = 2 * (ge_balance_positive_unit_iff_normrepresentationimaginary) /\ (ge_balance_negative_unit_iff_normrepresentationimaginary) = 0) \/ exists ge_signed_half_unit_iff_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_unit_iff_normrepresentation) = 2 * ge_signed_half_unit_iff_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_normrepresentationimaginary) = 0) /\ (ge_balance_negative_unit_iff_normrepresentationimaginary) = S ge_signed_half_unit_iff_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_unit_iff_norm) + ge_balance_negative_unit_iff_normrepresentationimaginary = (ge_norm_in_unit_iff_norm) + ge_balance_positive_unit_iff_normrepresentationimaginary)))))) /\ (exists ge_real_square_unit_iff_normsquare ge_imaginary_square_unit_iff_normsquare. ((((((ge_norm_rp_unit_iff_norm) * (ge_norm_rp_unit_iff_norm))) + (((ge_norm_rn_unit_iff_norm) * (ge_norm_rn_unit_iff_norm)))) = ((ge_real_square_unit_iff_normsquare) + (((((ge_norm_rp_unit_iff_norm) * (ge_norm_rn_unit_iff_norm))) + (((ge_norm_rn_unit_iff_norm) * (ge_norm_rp_unit_iff_norm))))))) /\ ((((((ge_norm_ip_unit_iff_norm) * (ge_norm_ip_unit_iff_norm))) + (((ge_norm_in_unit_iff_norm) * (ge_norm_in_unit_iff_norm)))) = ((ge_imaginary_square_unit_iff_normsquare) + (((((ge_norm_ip_unit_iff_norm) * (ge_norm_in_unit_iff_norm))) + (((ge_norm_in_unit_iff_norm) * (ge_norm_ip_unit_iff_norm))))))) /\ ((N) = ge_real_square_unit_iff_normsquare + ge_imaginary_square_unit_iff_normsquare)))))) -> (((exists gr_inverse_unit_iff_forward. (exists ge_first_rp_unit_iff_forwardidentity ge_first_rn_unit_iff_forwardidentity ge_first_ip_unit_iff_forwardidentity ge_first_in_unit_iff_forwardidentity ge_second_rp_unit_iff_forwardidentity ge_second_rn_unit_iff_forwardidentity ge_second_ip_unit_iff_forwardidentity ge_second_in_unit_iff_forwardidentity. ((exists ge_representation_real_code_unit_iff_forwardidentityfirst ge_representation_imaginary_code_unit_iff_forwardidentityfirst. (((z) = ((ge_representation_real_code_unit_iff_forwardidentityfirst) + (ge_representation_imaginary_code_unit_iff_forwardidentityfirst)) * S ((ge_representation_real_code_unit_iff_forwardidentityfirst) + (ge_representation_imaginary_code_unit_iff_forwardidentityfirst)) + ((ge_representation_imaginary_code_unit_iff_forwardidentityfirst) + (ge_representation_imaginary_code_unit_iff_forwardidentityfirst))) /\ ((exists ge_balance_positive_unit_iff_forwardidentityfirstreal ge_balance_negative_unit_iff_forwardidentityfirstreal. (((((ge_representation_real_code_unit_iff_forwardidentityfirst) = 2 * (ge_balance_positive_unit_iff_forwardidentityfirstreal) /\ (ge_balance_negative_unit_iff_forwardidentityfirstreal) = 0) \/ exists ge_signed_half_unit_iff_forwardidentityfirstrealdecode. (((ge_representation_real_code_unit_iff_forwardidentityfirst) = 2 * ge_signed_half_unit_iff_forwardidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_iff_forwardidentityfirstreal) = 0) /\ (ge_balance_negative_unit_iff_forwardidentityfirstreal) = S ge_signed_half_unit_iff_forwardidentityfirstrealdecode))) /\ ((ge_first_rp_unit_iff_forwardidentity) + ge_balance_negative_unit_iff_forwardidentityfirstreal = (ge_first_rn_unit_iff_forwardidentity) + ge_balance_positive_unit_iff_forwardidentityfirstreal))) /\ (exists ge_balance_positive_unit_iff_forwardidentityfirstimaginary ge_balance_negative_unit_iff_forwardidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_iff_forwardidentityfirst) = 2 * (ge_balance_positive_unit_iff_forwardidentityfirstimaginary) /\ (ge_balance_negative_unit_iff_forwardidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_iff_forwardidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_iff_forwardidentityfirst) = 2 * ge_signed_half_unit_iff_forwardidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_forwardidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_iff_forwardidentityfirstimaginary) = S ge_signed_half_unit_iff_forwardidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_iff_forwardidentity) + ge_balance_negative_unit_iff_forwardidentityfirstimaginary = (ge_first_in_unit_iff_forwardidentity) + ge_balance_positive_unit_iff_forwardidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_iff_forwardidentitysecond ge_representation_imaginary_code_unit_iff_forwardidentitysecond. (((gr_inverse_unit_iff_forward) = ((ge_representation_real_code_unit_iff_forwardidentitysecond) + (ge_representation_imaginary_code_unit_iff_forwardidentitysecond)) * S ((ge_representation_real_code_unit_iff_forwardidentitysecond) + (ge_representation_imaginary_code_unit_iff_forwardidentitysecond)) + ((ge_representation_imaginary_code_unit_iff_forwardidentitysecond) + (ge_representation_imaginary_code_unit_iff_forwardidentitysecond))) /\ ((exists ge_balance_positive_unit_iff_forwardidentitysecondreal ge_balance_negative_unit_iff_forwardidentitysecondreal. (((((ge_representation_real_code_unit_iff_forwardidentitysecond) = 2 * (ge_balance_positive_unit_iff_forwardidentitysecondreal) /\ (ge_balance_negative_unit_iff_forwardidentitysecondreal) = 0) \/ exists ge_signed_half_unit_iff_forwardidentitysecondrealdecode. (((ge_representation_real_code_unit_iff_forwardidentitysecond) = 2 * ge_signed_half_unit_iff_forwardidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_iff_forwardidentitysecondreal) = 0) /\ (ge_balance_negative_unit_iff_forwardidentitysecondreal) = S ge_signed_half_unit_iff_forwardidentitysecondrealdecode))) /\ ((ge_second_rp_unit_iff_forwardidentity) + ge_balance_negative_unit_iff_forwardidentitysecondreal = (ge_second_rn_unit_iff_forwardidentity) + ge_balance_positive_unit_iff_forwardidentitysecondreal))) /\ (exists ge_balance_positive_unit_iff_forwardidentitysecondimaginary ge_balance_negative_unit_iff_forwardidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_iff_forwardidentitysecond) = 2 * (ge_balance_positive_unit_iff_forwardidentitysecondimaginary) /\ (ge_balance_negative_unit_iff_forwardidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_iff_forwardidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_iff_forwardidentitysecond) = 2 * ge_signed_half_unit_iff_forwardidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_forwardidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_iff_forwardidentitysecondimaginary) = S ge_signed_half_unit_iff_forwardidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_iff_forwardidentity) + ge_balance_negative_unit_iff_forwardidentitysecondimaginary = (ge_second_in_unit_iff_forwardidentity) + ge_balance_positive_unit_iff_forwardidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_iff_forwardidentityoutput ge_representation_imaginary_code_unit_iff_forwardidentityoutput. (((6) = ((ge_representation_real_code_unit_iff_forwardidentityoutput) + (ge_representation_imaginary_code_unit_iff_forwardidentityoutput)) * S ((ge_representation_real_code_unit_iff_forwardidentityoutput) + (ge_representation_imaginary_code_unit_iff_forwardidentityoutput)) + ((ge_representation_imaginary_code_unit_iff_forwardidentityoutput) + (ge_representation_imaginary_code_unit_iff_forwardidentityoutput))) /\ ((exists ge_balance_positive_unit_iff_forwardidentityoutputreal ge_balance_negative_unit_iff_forwardidentityoutputreal. (((((ge_representation_real_code_unit_iff_forwardidentityoutput) = 2 * (ge_balance_positive_unit_iff_forwardidentityoutputreal) /\ (ge_balance_negative_unit_iff_forwardidentityoutputreal) = 0) \/ exists ge_signed_half_unit_iff_forwardidentityoutputrealdecode. (((ge_representation_real_code_unit_iff_forwardidentityoutput) = 2 * ge_signed_half_unit_iff_forwardidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_iff_forwardidentityoutputreal) = 0) /\ (ge_balance_negative_unit_iff_forwardidentityoutputreal) = S ge_signed_half_unit_iff_forwardidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_iff_forwardidentity) * (ge_second_rp_unit_iff_forwardidentity))) + (((ge_first_rn_unit_iff_forwardidentity) * (ge_second_rn_unit_iff_forwardidentity))))) + (((((ge_first_ip_unit_iff_forwardidentity) * (ge_second_in_unit_iff_forwardidentity))) + (((ge_first_in_unit_iff_forwardidentity) * (ge_second_ip_unit_iff_forwardidentity))))))) + ge_balance_negative_unit_iff_forwardidentityoutputreal = (((((((ge_first_rp_unit_iff_forwardidentity) * (ge_second_rn_unit_iff_forwardidentity))) + (((ge_first_rn_unit_iff_forwardidentity) * (ge_second_rp_unit_iff_forwardidentity))))) + (((((ge_first_ip_unit_iff_forwardidentity) * (ge_second_ip_unit_iff_forwardidentity))) + (((ge_first_in_unit_iff_forwardidentity) * (ge_second_in_unit_iff_forwardidentity))))))) + ge_balance_positive_unit_iff_forwardidentityoutputreal))) /\ (exists ge_balance_positive_unit_iff_forwardidentityoutputimaginary ge_balance_negative_unit_iff_forwardidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_iff_forwardidentityoutput) = 2 * (ge_balance_positive_unit_iff_forwardidentityoutputimaginary) /\ (ge_balance_negative_unit_iff_forwardidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_iff_forwardidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_iff_forwardidentityoutput) = 2 * ge_signed_half_unit_iff_forwardidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_forwardidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_iff_forwardidentityoutputimaginary) = S ge_signed_half_unit_iff_forwardidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_iff_forwardidentity) * (ge_second_ip_unit_iff_forwardidentity))) + (((ge_first_rn_unit_iff_forwardidentity) * (ge_second_in_unit_iff_forwardidentity))))) + (((((ge_first_ip_unit_iff_forwardidentity) * (ge_second_rp_unit_iff_forwardidentity))) + (((ge_first_in_unit_iff_forwardidentity) * (ge_second_rn_unit_iff_forwardidentity))))))) + ge_balance_negative_unit_iff_forwardidentityoutputimaginary = (((((((ge_first_rp_unit_iff_forwardidentity) * (ge_second_in_unit_iff_forwardidentity))) + (((ge_first_rn_unit_iff_forwardidentity) * (ge_second_ip_unit_iff_forwardidentity))))) + (((((ge_first_ip_unit_iff_forwardidentity) * (ge_second_rn_unit_iff_forwardidentity))) + (((ge_first_in_unit_iff_forwardidentity) * (ge_second_rp_unit_iff_forwardidentity))))))) + ge_balance_positive_unit_iff_forwardidentityoutputimaginary)))))))))) -> N=1) /\ (N=1 -> (exists gr_inverse_unit_iff_backward. (exists ge_first_rp_unit_iff_backwardidentity ge_first_rn_unit_iff_backwardidentity ge_first_ip_unit_iff_backwardidentity ge_first_in_unit_iff_backwardidentity ge_second_rp_unit_iff_backwardidentity ge_second_rn_unit_iff_backwardidentity ge_second_ip_unit_iff_backwardidentity ge_second_in_unit_iff_backwardidentity. ((exists ge_representation_real_code_unit_iff_backwardidentityfirst ge_representation_imaginary_code_unit_iff_backwardidentityfirst. (((z) = ((ge_representation_real_code_unit_iff_backwardidentityfirst) + (ge_representation_imaginary_code_unit_iff_backwardidentityfirst)) * S ((ge_representation_real_code_unit_iff_backwardidentityfirst) + (ge_representation_imaginary_code_unit_iff_backwardidentityfirst)) + ((ge_representation_imaginary_code_unit_iff_backwardidentityfirst) + (ge_representation_imaginary_code_unit_iff_backwardidentityfirst))) /\ ((exists ge_balance_positive_unit_iff_backwardidentityfirstreal ge_balance_negative_unit_iff_backwardidentityfirstreal. (((((ge_representation_real_code_unit_iff_backwardidentityfirst) = 2 * (ge_balance_positive_unit_iff_backwardidentityfirstreal) /\ (ge_balance_negative_unit_iff_backwardidentityfirstreal) = 0) \/ exists ge_signed_half_unit_iff_backwardidentityfirstrealdecode. (((ge_representation_real_code_unit_iff_backwardidentityfirst) = 2 * ge_signed_half_unit_iff_backwardidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_iff_backwardidentityfirstreal) = 0) /\ (ge_balance_negative_unit_iff_backwardidentityfirstreal) = S ge_signed_half_unit_iff_backwardidentityfirstrealdecode))) /\ ((ge_first_rp_unit_iff_backwardidentity) + ge_balance_negative_unit_iff_backwardidentityfirstreal = (ge_first_rn_unit_iff_backwardidentity) + ge_balance_positive_unit_iff_backwardidentityfirstreal))) /\ (exists ge_balance_positive_unit_iff_backwardidentityfirstimaginary ge_balance_negative_unit_iff_backwardidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_iff_backwardidentityfirst) = 2 * (ge_balance_positive_unit_iff_backwardidentityfirstimaginary) /\ (ge_balance_negative_unit_iff_backwardidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_iff_backwardidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_iff_backwardidentityfirst) = 2 * ge_signed_half_unit_iff_backwardidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_backwardidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_iff_backwardidentityfirstimaginary) = S ge_signed_half_unit_iff_backwardidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_iff_backwardidentity) + ge_balance_negative_unit_iff_backwardidentityfirstimaginary = (ge_first_in_unit_iff_backwardidentity) + ge_balance_positive_unit_iff_backwardidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_iff_backwardidentitysecond ge_representation_imaginary_code_unit_iff_backwardidentitysecond. (((gr_inverse_unit_iff_backward) = ((ge_representation_real_code_unit_iff_backwardidentitysecond) + (ge_representation_imaginary_code_unit_iff_backwardidentitysecond)) * S ((ge_representation_real_code_unit_iff_backwardidentitysecond) + (ge_representation_imaginary_code_unit_iff_backwardidentitysecond)) + ((ge_representation_imaginary_code_unit_iff_backwardidentitysecond) + (ge_representation_imaginary_code_unit_iff_backwardidentitysecond))) /\ ((exists ge_balance_positive_unit_iff_backwardidentitysecondreal ge_balance_negative_unit_iff_backwardidentitysecondreal. (((((ge_representation_real_code_unit_iff_backwardidentitysecond) = 2 * (ge_balance_positive_unit_iff_backwardidentitysecondreal) /\ (ge_balance_negative_unit_iff_backwardidentitysecondreal) = 0) \/ exists ge_signed_half_unit_iff_backwardidentitysecondrealdecode. (((ge_representation_real_code_unit_iff_backwardidentitysecond) = 2 * ge_signed_half_unit_iff_backwardidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_iff_backwardidentitysecondreal) = 0) /\ (ge_balance_negative_unit_iff_backwardidentitysecondreal) = S ge_signed_half_unit_iff_backwardidentitysecondrealdecode))) /\ ((ge_second_rp_unit_iff_backwardidentity) + ge_balance_negative_unit_iff_backwardidentitysecondreal = (ge_second_rn_unit_iff_backwardidentity) + ge_balance_positive_unit_iff_backwardidentitysecondreal))) /\ (exists ge_balance_positive_unit_iff_backwardidentitysecondimaginary ge_balance_negative_unit_iff_backwardidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_iff_backwardidentitysecond) = 2 * (ge_balance_positive_unit_iff_backwardidentitysecondimaginary) /\ (ge_balance_negative_unit_iff_backwardidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_iff_backwardidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_iff_backwardidentitysecond) = 2 * ge_signed_half_unit_iff_backwardidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_backwardidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_iff_backwardidentitysecondimaginary) = S ge_signed_half_unit_iff_backwardidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_iff_backwardidentity) + ge_balance_negative_unit_iff_backwardidentitysecondimaginary = (ge_second_in_unit_iff_backwardidentity) + ge_balance_positive_unit_iff_backwardidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_iff_backwardidentityoutput ge_representation_imaginary_code_unit_iff_backwardidentityoutput. (((6) = ((ge_representation_real_code_unit_iff_backwardidentityoutput) + (ge_representation_imaginary_code_unit_iff_backwardidentityoutput)) * S ((ge_representation_real_code_unit_iff_backwardidentityoutput) + (ge_representation_imaginary_code_unit_iff_backwardidentityoutput)) + ((ge_representation_imaginary_code_unit_iff_backwardidentityoutput) + (ge_representation_imaginary_code_unit_iff_backwardidentityoutput))) /\ ((exists ge_balance_positive_unit_iff_backwardidentityoutputreal ge_balance_negative_unit_iff_backwardidentityoutputreal. (((((ge_representation_real_code_unit_iff_backwardidentityoutput) = 2 * (ge_balance_positive_unit_iff_backwardidentityoutputreal) /\ (ge_balance_negative_unit_iff_backwardidentityoutputreal) = 0) \/ exists ge_signed_half_unit_iff_backwardidentityoutputrealdecode. (((ge_representation_real_code_unit_iff_backwardidentityoutput) = 2 * ge_signed_half_unit_iff_backwardidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_iff_backwardidentityoutputreal) = 0) /\ (ge_balance_negative_unit_iff_backwardidentityoutputreal) = S ge_signed_half_unit_iff_backwardidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_iff_backwardidentity) * (ge_second_rp_unit_iff_backwardidentity))) + (((ge_first_rn_unit_iff_backwardidentity) * (ge_second_rn_unit_iff_backwardidentity))))) + (((((ge_first_ip_unit_iff_backwardidentity) * (ge_second_in_unit_iff_backwardidentity))) + (((ge_first_in_unit_iff_backwardidentity) * (ge_second_ip_unit_iff_backwardidentity))))))) + ge_balance_negative_unit_iff_backwardidentityoutputreal = (((((((ge_first_rp_unit_iff_backwardidentity) * (ge_second_rn_unit_iff_backwardidentity))) + (((ge_first_rn_unit_iff_backwardidentity) * (ge_second_rp_unit_iff_backwardidentity))))) + (((((ge_first_ip_unit_iff_backwardidentity) * (ge_second_ip_unit_iff_backwardidentity))) + (((ge_first_in_unit_iff_backwardidentity) * (ge_second_in_unit_iff_backwardidentity))))))) + ge_balance_positive_unit_iff_backwardidentityoutputreal))) /\ (exists ge_balance_positive_unit_iff_backwardidentityoutputimaginary ge_balance_negative_unit_iff_backwardidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_iff_backwardidentityoutput) = 2 * (ge_balance_positive_unit_iff_backwardidentityoutputimaginary) /\ (ge_balance_negative_unit_iff_backwardidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_iff_backwardidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_iff_backwardidentityoutput) = 2 * ge_signed_half_unit_iff_backwardidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_iff_backwardidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_iff_backwardidentityoutputimaginary) = S ge_signed_half_unit_iff_backwardidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_iff_backwardidentity) * (ge_second_ip_unit_iff_backwardidentity))) + (((ge_first_rn_unit_iff_backwardidentity) * (ge_second_in_unit_iff_backwardidentity))))) + (((((ge_first_ip_unit_iff_backwardidentity) * (ge_second_rp_unit_iff_backwardidentity))) + (((ge_first_in_unit_iff_backwardidentity) * (ge_second_rn_unit_iff_backwardidentity))))))) + ge_balance_negative_unit_iff_backwardidentityoutputimaginary = (((((((ge_first_rp_unit_iff_backwardidentity) * (ge_second_in_unit_iff_backwardidentity))) + (((ge_first_rn_unit_iff_backwardidentity) * (ge_second_ip_unit_iff_backwardidentity))))) + (((((ge_first_ip_unit_iff_backwardidentity) * (ge_second_rn_unit_iff_backwardidentity))) + (((ge_first_in_unit_iff_backwardidentity) * (ge_second_rp_unit_iff_backwardidentity))))))) + ge_balance_positive_unit_iff_backwardidentityoutputimaginary))))))))))))

Complete tactic proof in conservative notation

All 22 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

22 script commands · 6 reading checkpoints · 0 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 (3)
gaussian unit has norm onegaussian norm one is unitgaussian norm value transport
01Fix variables and assumptionsL1–3

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

  1. L1
    intro z
  2. L2
    intro N
  3. L3
    intro hnorm
02Separate the logical casesL4–4

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

  1. L4
    split
03Fix variables and assumptionsL5–5

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

  1. L5
    intro hu
04Use earlier factsL6–13

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

  1. L6
    specialize gaussian_norm_functional (z)
  2. L7
    specialize gaussian_norm_functional (N)
  3. L8
    specialize gaussian_norm_functional (1)
  4. L9
    apply gaussian_norm_functional
  5. L10
    exact hnorm
  6. L11
    specialize gaussian_unit_has_norm_one (z)
  7. L12
    apply gaussian_unit_has_norm_one
  8. L13
    exact hu
05Fix variables and assumptionsL14–14

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

  1. L14
    intro heq
06Use earlier factsL15–22

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

  1. L15
    specialize gaussian_norm_one_is_unit (z)
  2. L16
    apply gaussian_norm_one_is_unit
  3. L17
    specialize gaussian_norm_value_transport (z)
  4. L18
    specialize gaussian_norm_value_transport (N)
  5. L19
    specialize gaussian_norm_value_transport (1)
  6. L20
    apply gaussian_norm_value_transport
  7. L21
    exact heq
  8. L22
    exact hnorm

Library-wide reading audit

Original defined command ledger · 22 lines
  1. 0001intro z
  2. 0002intro N
  3. 0003intro hnorm
  4. 0004split
  5. 0005intro hu
  6. 0006specialize gaussian_norm_functional (z)
  7. 0007specialize gaussian_norm_functional (N)
  8. 0008specialize gaussian_norm_functional (1)
  9. 0009apply gaussian_norm_functional
  10. 0010exact hnorm
  11. 0011specialize gaussian_unit_has_norm_one (z)
  12. 0012apply gaussian_unit_has_norm_one
  13. 0013exact hu
  14. 0014intro heq
  15. 0015specialize gaussian_norm_one_is_unit (z)
  16. 0016apply gaussian_norm_one_is_unit
  17. 0017specialize gaussian_norm_value_transport (z)
  18. 0018specialize gaussian_norm_value_transport (N)
  19. 0019specialize gaussian_norm_value_transport (1)
  20. 0020apply gaussian_norm_value_transport
  21. 0021exact heq
  22. 0022exact hnorm