PolynomialCorrectorRepresentation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual periodic system admits the polynomial solution whose order bounds were established in JetPolynomialFullCorrector.

theorem OAI.ClosedSurfaceR4.JetPolynomial.exists_polynomial_system line 16
Source documentation
The family solving the complete periodic system has the represented four-coordinate correction. All equations and the zero-support property are retained from the actual periodic solver.
```
theorem exists_polynomial_system {S : TopologicalSpace.Opens Base} {O : Set LowJet}
    (hO : IsOpen O) (v : Fin 2) (g : Geometry (E := R4) S (coordinateVector v))
…
```
Mentions: OAI.ClosedSurfaceR4.JetPolynomial.Base, OAI.ClosedSurfaceR4.JetPolynomial.LowJet, OAI.ClosedSurfaceR4.JetPolynomial.R4, OAI.ClosedSurfaceR4.JetPolynomial.coordinateVector