gaussian_product_beta_index_transport

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.

∀ b. ∀ c. ∀ i. ∀ j. ∀ a. i = j → BetaAt(b,c,i,a) → BetaAt(b,c,j,a)

forall b c i j a. i=j -> (((exists ff_h_gprod_index_transport_source. ff_h_gprod_index_transport_source + S (a) = S ((S (i)) * c)) /\ exists ff_q_gprod_index_transport_source. b = ff_q_gprod_index_transport_source * S ((S (i)) * c) + (a))) -> (((exists ff_h_gprod_index_transport_target. ff_h_gprod_index_transport_target + S (a) = S ((S (j)) * c)) /\ exists ff_q_gprod_index_transport_target. b = ff_q_gprod_index_transport_target * S ((S (j)) * c) + (a)))