import Omega.Dimension
import Omega.Placement
import Omega.Interface
import Omega.Extinction
import Omega.Finite
import Omega.Metrics

/-! Combined central theorem. The definitions in its hypotheses are part of
the mathematical specification, not claimed consequences of an unmarked shape. -/
namespace Omega
noncomputable section

theorem central_provenance_theorem
    {V : Type*} [NormedAddCommGroup V] [NormedSpace ℝ V]
    (α : V) (E : ℂ →ₗᵢ[ℝ] V) (a h : ℝ) (ha : 0 < a) (hh : 0 < h) :
    (placedG α E a=a*phi ∧ placedC α E a=a*Real.pi ∧
      placedG α E a/(placedG α E a+placedC α E a)=lam) ∧
    (∀ x : ℝ, (G a*x+C a)/(G a+C a)=T x) ∧
    (∀ d : ℕ, d < domainSize → Int.floor (lam*d)=(F d:ℤ)) ∧
    (∀ n d : ℕ, d < domainSize →
      (quantizedStep h)^[n] (h*d)=h*(F^[n] d:ℝ)) ∧
    (∀ n : ℕ, ∀ d : ℤ,
      Ledger.recover Q S (Ledger.encode Q S n d).1 (Ledger.encode Q S n d).2=d) ∧
    (∀ t : ℤ, ∀ rs : List ℤ, Ledger.Admissible Q S t rs ↔
      ∃! d : ℤ, Ledger.encode Q S rs.length d=(t,rs)) := by
  refine ⟨provenance_all_placements α E a ha,?_,certified_floor_equality,
    grid_trajectory h hh,?_,?_⟩
  · intro x
    rw [G_eq a ha,C_eq a ha]
    exact weighted_mean a x ha
  · exact Ledger.roundtrip Q S (by norm_num [Q])
  · exact Ledger.admissibility_iff Q S (by norm_num [Q]) (by norm_num [S])

end
end Omega