MovingLines.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Polynomial motion of smooth line configurations

def OAI.Nagata.Workers.W14.lineMarkYDerivative line 19
Source documentation
The certified Y derivative of the actual reduced line-union equation.
```
def lineMarkYDerivative (k n : ℕ) (i : Fin (k * k + n)) : ℂ :=
…
```
theorem OAI.Nagata.Workers.W14.lineMarkYDerivative_ne_zero line 23
def OAI.Nagata.Workers.W14.lineMarkVelocity line 28
Source documentation
Explicit vertical velocity realizing the requested normal displacement.
```
def lineMarkVelocity (k n : ℕ) (displacement : Fin (k * k + n) → ℂ)
    (i : Fin (k * k + n)) : ℂ × ℂ :=
…
```
theorem OAI.Nagata.Workers.W14.lineMarkVelocity_normal line 32
theorem OAI.Nagata.Workers.W14.lineMarkVelocity_zero line 37
def OAI.Nagata.Workers.W14.lineMarkCoordinateMotion line 42
Source documentation
Actual coordinate polynomials of the explicit vertical affine motions.
```
def lineMarkCoordinateMotion (k n : ℕ) (displacement : Fin (k * k + n) → ℂ) :
    Fin (k * k + n) × Fin 2 → Polynomial ℂ :=
…
```
theorem OAI.Nagata.Workers.W14.lineMarkCoordinateMotion_eval line 47
theorem OAI.Nagata.Workers.W14.lineMarkCoordinateMotion_base line 57
theorem OAI.Nagata.Workers.W14.lineMarkCoordinateMotion_base_injective line 68

theorem OAI.Nagata.Workers.W14.universalSupport_line_motion_family line 77

Source documentation

Actual universal equations give a single genuine homogeneous polynomial family at the explicit line marks, with every chart order valid for every s.

theorem universalSupport_line_motion_family {k n d : ℕ}
    {m : Fin (k * k + n) → ℕ}
    (hU : Nagata.W13.UniversalSupport (k * k + n) d m)
    (displacement : Fin (k * k + n) → ℂ) :
    ∃ S : Polynomial (MvPolynomial (Fin 3) ℂ),
      S.coeff 0 ≠ 0 ∧ (∀ α, (S.coeff α).IsHomogeneous d) ∧
      ∀ s i, Nagata.AffineMultiplicity.orderAtLeast
        (pairCoordinates (orderedAffinePoint k n i + s • lineMarkVelocity k n displacement i))
        (m i) (Nagata.W27.directChartHom 2 (S.eval (MvPolynomial.C s))) := by
…

Mentions: OAI.Nagata.W13.UniversalSupport, OAI.Nagata.Workers.W14.lineMarkVelocity, OAI.Nagata.W27.directChartHom

def OAI.Nagata.Workers.W14.triangleDisplacement line 95
Source documentation
Triangle displacement pattern: zero at all nine original marks and one at each extra point.
```
def triangleDisplacement (n : ℕ) (i : Fin (3 * 3 + n)) : ℂ :=
…
```
theorem OAI.Nagata.Workers.W14.triangleDisplacement_first_nine line 98
theorem OAI.Nagata.Workers.W14.triangleDisplacement_extra line 101