RealTarget.lean`

21 declarations, 0 contain sorry, 0 declared as axioms

The arbitrary-real-error target and its exact passage from encoded rational gap reductions. The same formula map and actual machine certificate are reused; choosing smaller error tolerances does not change the computation.

structure OAI.MaxCutGames.Integration.RealTarget.PolynomialGapReduction line 18
Source documentation
A fixed-alphabet gap reduction from 3SAT, including its actual finite-machine polynomial runtime, with the two approximation thresholds expressed over ℝ.
```
structure PolynomialGapReduction (ε δ : ℝ) where
…
```
def OAI.MaxCutGames.Integration.RealTarget.ofRational line 34
Source documentation
A genuine rational-error certificate supplies every weaker real threshold. The input and output encodings and finite transition program remain identical.
```
def ofRational {e d : RationalError} {ε δ : ℝ}
    (p : Complexity.PolynomialGapReduction e d)
    (hε : (GapSemantics.errorValue e : ℝ) ≤ ε)
    (hδ : (GapSemantics.errorValue d : ℝ) ≤ δ) : PolynomialGapReduction ε δ where
…
```
Mentions: OAI.MaxCutGames.Integration.GapSemantics.errorValue, OAI.MaxCutGames.Integration.RealTarget.PolynomialGapReduction
theorem OAI.MaxCutGames.Integration.RealTarget.for_all_real_of_dyadic line 53
Source documentation
It suffices to construct the full machine-backed reduction for dyadic errors. This theorem does not assert that those certificates have been built.
```
theorem for_all_real_of_dyadic
    (certificates : ∀ m n : Nat, Nonempty
      (Complexity.PolynomialGapReduction
        (DyadicErrors.dyadicError m) (DyadicErrors.dyadicError n)))
    (ε δ : ℝ) (hε : 0 < ε) (hδ : 0 < δ) :
    Nonempty (PolynomialGapReduction ε δ) := by
…
```
Mentions: OAI.MaxCutGames.Integration.DyadicErrors.dyadicError, OAI.MaxCutGames.Integration.RealTarget.PolynomialGapReduction
def OAI.MaxCutGames.Integration.InstanceValue.maxSatisfied line 80
Source documentation
The maximum number of satisfied occurrences among all vertex labelings.
```
def maxSatisfied {q : Nat} (g : Instance q) : Nat :=
…
```
def OAI.MaxCutGames.Integration.InstanceValue.value line 86
Source documentation
The usual instance value: the largest satisfied fraction of its stored constraint list. The denominator is positive by the Instance invariant.
```
noncomputable def value {q : Nat} (g : Instance q) : ℝ :=
…
```
theorem OAI.MaxCutGames.Integration.InstanceValue.countSatisfied_le_maxSatisfied line 89
theorem OAI.MaxCutGames.Integration.InstanceValue.maxSatisfied_le_length line 97
theorem OAI.MaxCutGames.Integration.InstanceValue.maxSatisfied_attained line 103
theorem OAI.MaxCutGames.Integration.InstanceValue.value_attained line 112
theorem OAI.MaxCutGames.Integration.InstanceValue.labeling_rate_le_value line 118
theorem OAI.MaxCutGames.Integration.InstanceValue.satisfactionRate_le_value line 126
Source documentation
This value uses the same rate already defined for the encoded gap target.
```
theorem satisfactionRate_le_value {q : Nat} (g : Instance q)
    (labeling : Fin g.vertices → Fin q) :
    (GapSemantics.satisfactionRate g labeling : ℝ) ≤ value g := by
…
```
Mentions: OAI.MaxCutGames.Integration.GapSemantics.satisfactionRate, OAI.MaxCutGames.Integration.InstanceValue.value
theorem OAI.MaxCutGames.Integration.InstanceValue.value_nonneg line 131
theorem OAI.MaxCutGames.Integration.InstanceValue.value_le_one line 134
theorem OAI.MaxCutGames.Integration.InstanceValue.value_mem_unitInterval line 140

theorem OAI.MaxCutGames.Integration.InstanceValue.exists_rate_ge_iff line 144

Source documentation

Existential real completeness is precisely a lower bound on instance value.

theorem exists_rate_ge_iff {q : Nat} (g : Instance q) (hq : 0 < q) (a : ℝ) :
    (∃ labeling : Fin g.vertices → Fin q,
      a ≤ (countSatisfied labeling g.constraints : ℝ) / g.constraints.length) ↔
      a ≤ value g := by
…

Mentions: OAI.MaxCutGames.Integration.InstanceValue.value

theorem OAI.MaxCutGames.Integration.InstanceValue.forall_rate_le_iff line 156

Source documentation

Universal real soundness is precisely an upper bound on instance value.

theorem forall_rate_le_iff {q : Nat} (g : Instance q) (hq : 0 < q) (b : ℝ) :
    (∀ labeling : Fin g.vertices → Fin q,
      (countSatisfied labeling g.constraints : ℝ) / g.constraints.length ≤ b) ↔
      value g ≤ b := by
…

Mentions: OAI.MaxCutGames.Integration.InstanceValue.value

theorem OAI.MaxCutGames.Integration.InstanceValue.completeAt_iff_value line 167
theorem OAI.MaxCutGames.Integration.InstanceValue.soundAt_iff_value line 172
theorem OAI.MaxCutGames.Integration.InstanceValue.realTarget_completeness line 178
Source documentation
The unchanged real target certificate gives literal val(U) ≥ 1 - ε.
```
theorem realTarget_completeness {ε δ : ℝ}
    (p : RealTarget.PolynomialGapReduction ε δ) (formula : Formula)
    (hformula : formula.Satisfiable) :
    1 - ε ≤ value (p.reduce formula) := by
…
```
Mentions: OAI.MaxCutGames.Integration.RealTarget.PolynomialGapReduction, OAI.MaxCutGames.Integration.InstanceValue.value
theorem OAI.MaxCutGames.Integration.InstanceValue.realTarget_soundness line 187
Source documentation
The unchanged real target certificate gives literal val(U) ≤ δ.
```
theorem realTarget_soundness {ε δ : ℝ}
    (p : RealTarget.PolynomialGapReduction ε δ) (formula : Formula)
    (hformula : ¬ formula.Satisfiable) :
    value (p.reduce formula) ≤ δ := by
…
```
Mentions: OAI.MaxCutGames.Integration.RealTarget.PolynomialGapReduction, OAI.MaxCutGames.Integration.InstanceValue.value
theorem OAI.MaxCutGames.Integration.InstanceValue.realTarget_value_guarantees line 195