NetworkBarrier.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem326.BarrierConstruction.UniformAffineApproximation line 19
Source documentation
The uniform conclusion needed from the arbitrary-tolerance affine lemma. Slopes are fixed before h is chosen, and every minimizing branch, including ties, must approximate.
```
def UniformAffineApproximation (d : ℕ) : Prop :=
…
```
structure OAI.Problem326.BarrierConstruction.AffineBarrierData line 30
Source documentation
Finite barrier data, after the network, rates, and initial point have been fixed. The remaining analytic step is trapping and global ODE continuation.
```
structure AffineBarrierData {d : ℕ} (N : ReactionNetwork d)
    (κ : Reaction N → ℝ) (x₀ : Fin d → ℝ) where
…
```
Mentions: OAI.Problem326.ReactionNetwork, OAI.Problem326.Reaction
def OAI.Problem326.BarrierConstruction.coordinateDirection line 51
Source documentation
Coordinate directions are included alongside all complex differences.
```
def coordinateDirection {d : ℕ} (i : Fin d) : Fin d → ℝ :=
…
```
def OAI.Problem326.BarrierConstruction.complexDifference line 54
theorem OAI.Problem326.BarrierConstruction.dot_coordinateDirection line 57
theorem OAI.Problem326.BarrierConstruction.dot_complexDifference line 62
def OAI.Problem326.BarrierConstruction.comparisonDirections line 68
theorem OAI.Problem326.BarrierConstruction.coordinateDirection_mem line 73
theorem OAI.Problem326.BarrierConstruction.complexDifference_mem line 78
theorem OAI.Problem326.BarrierConstruction.exists_affineBarrierData line 91
Source documentation
The full network-aware algebraic assembly. The tolerance is selected first, then fixed slopes and their positive gap, then the single small parameter. No compactness or ODE conclusion is assumed in this theorem.
```
theorem exists_affineBarrierData {d : ℕ}
    (happroximation : UniformAffineApproximation d)
    (N : ReactionNetwork d) (κ : Reaction N → ℝ)
    (hweak : WeaklyReversible N) (hκ : ∀ e, 0 < κ e)
    (x₀ : Fin d → ℝ) (hx₀ : PositiveState x₀) :
    Nonempty (AffineBarrierData N κ x₀) := by
…
```
Mentions: OAI.Problem326.BarrierConstruction.UniformAffineApproximation, OAI.Problem326.ReactionNetwork, OAI.Problem326.Reaction, OAI.Problem326.WeaklyReversible, OAI.Problem326.PositiveState, OAI.Problem326.BarrierConstruction.AffineBarrierData