TranscendentalUnit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A transcendental principal p-adic unit

The holonomy construction chooses a transcendental element of 1 + 2ℤ₂. The existence proof below works for every prime: algebraic elements form a countable set, and the Baire theorem makes its complement dense in the complete, perfect p-adic field.

theorem OAI.CoarseAssembly.dense_padic_transcendental line 25
Source documentation
Transcendental elements over the integers are dense in the p-adic field.
```
theorem dense_padic_transcendental : Dense {x : ℚ_[p] | Transcendental ℤ x} := by
…
```
theorem OAI.CoarseAssembly.exists_transcendental_principal_unit line 38
Source documentation
The exact principal-unit choice needed for diagonal holonomy exists. The specialization p = 2 lies in 1 + 2ℤ₂.
```
theorem exists_transcendental_principal_unit :
    ∃ t : ℤ_[p]ˣ, Transcendental ℤ (t : ℤ_[p]) ∧
      ∃ a : ℤ_[p], (t : ℤ_[p]) = 1 + (p : ℤ_[p]) * a := by
…
```