ChordContradiction.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A genuinely aligned positive-defect configuration is impossible.

theorem OAI.Tingley.alignedConfiguration_impossible line 18
Source documentation
The global bound and the actual aligned chords contradict one another. The two small-regime inequalities are proved from the original and literal inverse configurations; neither is an additional caller premise.
```
theorem alignedConfiguration_impossible (hM : 0 < M) (ht : 0 < t ∧ t < 1)
    (hb : HasDefectBound f M) (C : AlignedConfiguration f y t M) : False := by
…
```
Mentions: OAI.Tingley.HasDefectBound, OAI.Tingley.AlignedConfiguration