Grace/Cumulus/Algebra/Polynomial/EmptyVariables.g17

Open in Workbench Download source

Imports

EvaluationOver · HornerRelations

Declarations

• monomials.empty_unique theorem derivation
• emptyPolynomialCoefficient defgraph
• polynomial.empty_constant theorem derivation
• emptyPolynomialCoefficient.nonzero theorem derivation
• polynomialAtOver.empty_value theorem derivation
• AlgebraicOver.empty_variables theorem derivation

Source

1-- Zero-variable polynomials are constants; algebraic relations descend to coefficients.2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Grace.Cumulus.Algebra.Polynomial.EmptyVariables8import EvaluationOver9import HornerRelations1011theorem monomials.empty_unique (m : Set)12  requires monomial : m ∈ monomials(∅)13  shows m = monomialOne(∅)14proof15  have unit := monomialOne.member at ∅16  apply monomials.ext with monomial, unit17  intros i impossible18  exfalso19  exact set.empty with impossible2021defgraph emptyPolynomialCoefficient (A zero : Set) (p ∈ polynomials(∅, A, zero)) : A := p(monomialOne(∅))22proof23  have function := polynomials.function with member24  have unit := monomialOne.member at ∅25  exact FunctionBetween.apply_closed with function, unit2627theorem polynomial.empty_constant (A zero p : Set)28  requires zeroIn : zero ∈ A29  requires polynomial : p ∈ polynomials(∅, A, zero)30  shows p = polynomialConstant(∅, A, zero, emptyPolynomialCoefficient(A, zero)(p))31proof32  have function := polynomials.function with polynomial33  have coefficientMap := emptyPolynomialCoefficient.function at A, zero34  have coefficient := FunctionBetween.apply_closed with coefficientMap, polynomial35  have value := emptyPolynomialCoefficient.value with polynomial36  have constant := polynomialConstant.member at ∅, A, zero, emptyPolynomialCoefficient(A, zero)(p) with *37  have constantFunction := polynomials.function with constant38  apply FunctionBetween.ext with function, constantFunction39  intros m hm40  have same := monomials.empty_unique with hm41  have evaluated := polynomialConstant.value at ∅, A, zero, emptyPolynomialCoefficient(A, zero)(p), m with *42  have selected := singleValue.same at A, zero, emptyPolynomialCoefficient(A, zero)(p), monomialOne(∅), m with *43  cc4445theorem emptyPolynomialCoefficient.nonzero (A zero p : Set)46  requires zeroIn : zero ∈ A47  requires polynomial : p ∈ polynomials(∅, A, zero)48  requires nonzero : p ≠ constantFunction(monomials(∅), A, zero)49  shows emptyPolynomialCoefficient(A, zero)(p) ≠ zero50proof51  have constant := polynomial.empty_constant with *52  intro vanishes53  rw [vanishes, polynomialConstant.zero] at constant54  exact nonzero with constant5556section Algebras57variable (A add zero neg mul one B plus z minus times unit f v : Set)58notation ring R := (A, add, zero, neg, mul, one)59notation ring S := (B, plus, z, minus, times, unit)60notation ring Q := R[∅]61hypothesis source : IsCommRing(R)62hypothesis target : IsCommRing(S)63hypothesis hom : IsRingHom(f, R, S)64hypothesis assignment : v : ∅ → S6566theorem polynomialAtOver.empty_value (p : Set)67  requires polynomial : p ∈ Q68  shows polynomialAtOver(∅, R, S, f, v)(p) = f(emptyPolynomialCoefficient(A, zero)(p))69proof70  have zeroIn : R[0] ∈ R by typecheck71  have function := emptyPolynomialCoefficient.function at A, zero72  have coefficient := FunctionBetween.apply_closed with function, polynomial73  have constant := polynomial.empty_constant with *74  have evaluation := polynomialAtOver.constant with coefficient75  cc7677-- Top-down transport: extract each constant coefficient, preserve the nonzero78-- leading term, then map the finite Horner list through coefficient extraction.79theorem AlgebraicOver.empty_variables (x : Set)80  requires algebraic : AlgebraicOver(polynomialAtOver(∅, R, S, f, v), Q, S, x)81  shows AlgebraicOver(f, R, S, x)82proof83  obtain ⟨member, leading, polynomial, nonzero, cs, list, equation⟩ := algebraic84  have function := emptyPolynomialCoefficient.function at A, zero85  have coefficient := FunctionBetween.apply_closed with function, polynomial86  have zeroIn : R[0] ∈ R by typecheck87  have leadingNonzero := emptyPolynomialCoefficient.nonzero with *88  have coefficients := listMap.closed with *89  have agreement : ∀ p ∈ Q, polynomialAtOver(∅, R, S, f, v)(p) = f(emptyPolynomialCoefficient(A, zero)(p))90    intros p hp91    exact polynomialAtOver.empty_value with *92  have leadingValue := agreement with leading, polynomial93  have changed := monicValue.change_coefficients at Q, A, plus, times, emptyPolynomialCoefficient(A, zero), f, polynomialAtOver(∅, R, S, f, v), polynomialAtOver(∅, R, S, f, v)(leading), x, cs with *94  unfold polynomialHorner at equation95  rw [changed, leadingValue] at equation96  unfold AlgebraicOver97  refine ⟨member, emptyPolynomialCoefficient(A, zero)(leading), coefficient, leadingNonzero, listMap{Q}(emptyPolynomialCoefficient(A, zero), cs), coefficients, ?_⟩98  simp [polynomialHorner]99100end Algebras101