Comparison.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Reciprocal low-degree rigidity and positive elementary sheaf-transfer inequalities.

theorem OAI.KLInvariance.Comparison.low_degree_zero_of_eval_reciprocal line 24
Source documentation
A polynomial supported strictly below the middle cannot equal its reciprocal on an open real interval. This discharges the final rigidity step after the source's two comparison inequalities have been combined.
```
theorem low_degree_zero_of_eval_reciprocal (p : ℝ[X]) (d : ℕ)
    (hp : 2 * p.natDegree < d)
    (h : ∀ q : ℝ, 0 < q → q < 1 → p.eval q = q ^ d * p.eval q⁻¹) : p = 0 := by
…
```

theorem OAI.KLInvariance.Comparison.eq_of_eval_difference_reciprocal line 50

Source documentation

The exact polynomial conclusion from reciprocal difference equality, without assuming positivity of KL coefficients.

theorem eq_of_eval_difference_reciprocal (p p' : ℤ[X]) (d : ℕ)
    (hp : 2 * p.natDegree < d) (hp' : 2 * p'.natDegree < d)
    (h : ∀ q : ℝ, 0 < q → q < 1 →
      p.eval₂ (Int.castRingHom ℝ) q - p'.eval₂ (Int.castRingHom ℝ) q =
      q ^ d * (p.eval₂ (Int.castRingHom ℝ) q⁻¹ -
        p'.eval₂ (Int.castRingHom ℝ) q⁻¹)) : p = p' := by
…

def OAI.KLInvariance.Comparison.transfer line 74
Source documentation
The genuine elementary transfer id + T E_xy from the source's edge schedule, expressed on vectors rather than with a choice of enumeration.
```
noncomputable def transfer (T : ℝ) (x y : V) (v : V → ℝ) : V → ℝ :=
…
```
theorem OAI.KLInvariance.Comparison.transfer_monotone line 77
theorem OAI.KLInvariance.Comparison.transfer_injective line 85
def OAI.KLInvariance.Comparison.idealState line 98
theorem OAI.KLInvariance.Comparison.state_le_ideal line 105
Source documentation
Propagation of the actual Hilbert-series bound through all earlier edges. No freeness or positivity of the vectors is needed for this part.
```
theorem state_le_ideal (T : ℝ) (hT : 0 ≤ T) (edges : ℕ → V × V)
    (D : ℕ → V → ℝ) (n : ℕ)
    (hstep : ∀ k < n, D (k + 1) ≤ transfer T (edges k).1 (edges k).2 (D k)) :
    D n ≤ idealState T edges (D 0) n := by
…
```
Mentions: OAI.KLInvariance.Comparison.transfer, OAI.KLInvariance.Comparison.idealState
theorem OAI.KLInvariance.Comparison.every_step_eq_of_endpoint_eq line 119
Source documentation
Endpoint equality forces every edge-image deficit to vanish, including those invisible in codimension one. This uses actual inequalities and the injectivity of elementary edge transfers; it does not assume image equality. It is the no-deficit conclusion of source (6.8).
```
theorem every_step_eq_of_endpoint_eq (T : ℝ) (hT : 0 ≤ T)
    (edges : ℕ → V × V) (D : ℕ → V → ℝ) (n : ℕ)
    (hedges : ∀ k < n, (edges k).1 ≠ (edges k).2)
    (hstep : ∀ k < n, D (k + 1) ≤ transfer T (edges k).1 (edges k).2 (D k))
    (hend : D n = idealState T edges (D 0) n) :
    ∀ k < n, D (k + 1) = transfer T (edges k).1 (edges k).2 (D k) := by
…
```
Mentions: OAI.KLInvariance.Comparison.transfer, OAI.KLInvariance.Comparison.idealState