Main.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.SquareRootDegree.signed_violations line 13
Source documentation
Every stage and the final sign readout use finitely many actual Boolean inputs.
```
theorem signed_violations : SignedViolations := by
…
```
Mentions: OAI.SquareRootDegree.SignedViolations
theorem OAI.SquareRootDegree.main line 20
Source documentation
Unbounded violations for ordinary real Fourier degree and uniform cube averages.
Distinct definitions of this name: ComparatorChallenges/SquareRootDegree.lean:57 (same statement text; different proof or body). Qualify references as OAI.SquareRootDegree.main@path.
```
theorem main : SignedViolations ∧ ¬ BddAbove AbsoluteRatios := by
…
```
Mentions: OAI.SquareRootDegree.SignedViolations, OAI.SquareRootDegree.AbsoluteRatios