Target.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.HasC1CurveChart line 12
Source documentation
A regular C¹ parametrization of the curve near a point, with a continuous inverse.
Also declared: ComparatorChallenges/GammaPassage.lean:85 (same declaration text).
```
def HasC1CurveChart (S : Set Plane) (v : Plane) : Prop :=
…
```
def OAI.GammaFPP.GammaDifferentiabilityTarget line 23
Source documentation
The Gamma theorem: an actual deterministic passage-time limit norm exists for every positive shape and rate and every iid environment with that law. Its Frechet differentiability and literal unit-ball boundary charts are conclusions. No shape theorem, norm, or no-corner hypothesis is supplied.
Also declared: ComparatorChallenges/GammaPassage.lean:96 (same declaration text).
```
def GammaDifferentiabilityTarget : Prop :=
…
```