BalancedStretch.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

A rational volume-independent coordinate change for the Euclidean cube observer. The velocity is pushed forward; the force is subsequently defined by its Navier--Stokes residual, so anisotropic diffusion causes no restriction.

def OAI.ForcedComputation.BalancedStretch.coefficient line 14
def OAI.ForcedComputation.BalancedStretch.linear line 16
def OAI.ForcedComputation.BalancedStretch.inverseLinear line 20
theorem OAI.ForcedComputation.BalancedStretch.linear_apply line 24
theorem OAI.ForcedComputation.BalancedStretch.inverseLinear_apply line 27
theorem OAI.ForcedComputation.BalancedStretch.coefficient_ne line 30
def OAI.ForcedComputation.BalancedStretch.stretch line 34
theorem OAI.ForcedComputation.BalancedStretch.stretch_apply line 51
theorem OAI.ForcedComputation.BalancedStretch.stretch_symm_apply line 54
theorem OAI.ForcedComputation.BalancedStretch.stretch_symm_basis line 57
def OAI.ForcedComputation.BalancedStretch.push line 65
def OAI.ForcedComputation.BalancedStretch.velocity line 67
theorem OAI.ForcedComputation.BalancedStretch.push_smooth line 69
theorem OAI.ForcedComputation.BalancedStretch.velocity_smooth line 73
theorem OAI.ForcedComputation.BalancedStretch.push_derivative line 78
theorem OAI.ForcedComputation.BalancedStretch.push_divergence line 86
theorem OAI.ForcedComputation.BalancedStretch.velocity_divergence line 95
theorem OAI.ForcedComputation.BalancedStretch.push_zero_iff line 100
theorem OAI.ForcedComputation.BalancedStretch.push_support line 105
theorem OAI.ForcedComputation.BalancedStretch.push_compact line 114
theorem OAI.ForcedComputation.BalancedStretch.trajectory line 119
def OAI.ForcedComputation.BalancedStretch.observer line 129
Source documentation
The cube used by the balanced Euclidean main result.
```
def observer : Set Space := {x | ∀ j : Fin 3, -1 < x j ∧ x j < 2}
```
theorem OAI.ForcedComputation.BalancedStretch.nonhalting_outside line 131
theorem OAI.ForcedComputation.BalancedStretch.halting_inside line 139
theorem OAI.ForcedComputation.BalancedStretch.loading_outside line 152
Source documentation
A straight loading path stays outside the cube whenever its endpoint satisfies x₀+x₁≥4. This lets the body use a fixed machine-only normalization.
```
theorem loading_outside {p : Space} (hp : 4 ≤ p 0 + p 1)
    {θ : ℝ} (hθ : θ ∈ Icc (0 : ℝ) 1) :
    (1 - θ) • ![4, 0, 0] + θ • p ∉ observer := by
…
```
Mentions: OAI.ForcedComputation.BalancedStretch.observer