Main.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GrahamSpherical.exists_common_derivation_colorings line 13
Source documentation
A single actual real derivation defines avoiding colorings in all dimensions.
```
theorem exists_common_derivation_colorings :
    ∃ D : Derivation ℤ ℝ ℝ,
      D parameter = (1 + parameter ^ 2) / 2 ∧
      ∀ n : ℕ, AvoidsCopy witness (energyColor (derivationEnergy (n := n) D)) := by
…
```
Mentions: OAI.GrahamSpherical.parameter, OAI.GrahamSpherical.AvoidsCopy, OAI.GrahamSpherical.witness, OAI.GrahamSpherical.energyColor, OAI.GrahamSpherical.derivationEnergy
theorem OAI.GrahamSpherical.full_main line 23
Source documentation
The literal twelve-point spherical witness defeats fifty colors in every positive dimension, hence is not Euclidean Ramsey. No auxiliary premise remains.
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: OAI.GrahamSpherical.Specification.FullAuthoredResult
Proof uses: Derivation, Int, Real, And, Eq, OAI.GrahamSpherical.parameter, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, HPow.hPow, Nat, OAI.GrahamSpherical.AvoidsCopy, OAI.GrahamSpherical.witness, OAI.GrahamSpherical.energyColor, OAI.GrahamSpherical.derivationEnergy, Exists, OAI.GrahamSpherical.exists_common_derivation_colorings, OAI.GrahamSpherical.assemble_full_result, OAI.GrahamSpherical.witness_ncard, OAI.GrahamSpherical.witness_subset_sphere and 4 more
30 instances, coercions and auxiliary constants left out.
Distinct definitions of this name: ComparatorChallenges/GrahamSpherical.lean:58 (same statement text; different proof or body). Qualify references as OAI.GrahamSpherical.full_main@path.
Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem full_main : Specification.FullAuthoredResult := by
…
```
Mentions: OAI.GrahamSpherical.Specification.FullAuthoredResult