theorem Hex.AlgebraicPoly.Common.presentationAt?_isSome (coefficients : Array AlgebraicNumber) (gamma : AlgebraicNumber) (contained : ∀ a ∈ coefficients, a.toComplex ∈ ℚ⟮gamma.toComplex⟯) : (presentationAt? gamma coefficients).isSome = true

A proposed field presentation succeeds when coordinate recovery succeeds for every coefficient.

theorem Hex.AlgebraicPoly.Common.presentation?_isSome (coefficients : Array AlgebraicNumber) (hnonzero : ∃ a ∈ coefficients.toList, a.isZero = false) : (presentation? coefficients).isSome = true

A nonzero algebraic coefficient array always admits a checked primitive fixed-field presentation.

theorem Hex.AlgebraicPoly.Common.presentationAt?_sound (generator : AlgebraicNumber) (coefficients : Array AlgebraicNumber) {presentation : Presentation} (h : presentationAt? generator coefficients = some presentation) : presentation.coefficients.size = coefficients.size ∧ ∀ (i : ℕ) (hi : i < coefficients.size) (hiPresentation : i < presentation.coefficients.size), presentation.coefficients[i].toComplex presentation.generator.rep ⋯ = coefficients[i].toComplex

A successful presentation preserves the coefficient array length and the selected complex value of every coefficient.

theorem Hex.AlgebraicPoly.Common.presentation?_sound (coefficients : Array AlgebraicNumber) {presentation : Presentation} (h : presentation? coefficients = some presentation) : presentation.coefficients.size = coefficients.size ∧ ∀ (i : ℕ) (hi : i < coefficients.size) (hiPresentation : i < presentation.coefficients.size), presentation.coefficients[i].toComplex presentation.generator.rep ⋯ = coefficients[i].toComplex

Both the proposed-field check and the primitive-search fallback preserve all selected coefficient values.