/-
Copyright (c) 2026 LANA Project. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: LANA Project
-/
import Iut.Concrete.LocalConstruct.LogShell
import Iut.Concrete.LocalConstruct.ArchLogShell
import Iut.Concrete.LocalConstruct.Hull
import Iut.Concrete.LocalConstruct.Prop14
import Iut.Concrete.LocalConstruct.ShellBound

/-!
# The concrete local theory (taxis #4, #278)

This file exposes the constructions of `Iut/Concrete/LocalConstruct/*`, uniformly in the
rational place, as the definitions `Iut.LocalTheory.Tensor`, `integral`, `logShell`,
`componentVol`, `admissible`, `indAut`, `incl` and the theorems about them (IUT III,
Propositions 3.1, 3.2, 3.9; IUT IV, Propositions 1.2, 1.4, 1.5) consumed by the concrete large
volume container. Everything is proved from the construction; no propositional input
remains, and there is no interface: the statement layer refers to these definitions
directly.

* `(R_I)^∼ ⊆ 𝓘_I` (`integral_subset_logShell`, `LogShell.lean`; the log-shell of a packet is
  the `(R_I)^∼`-module generated by the tensor product of the log-shells of the factors).
* Least hull regions `a·(R_I)^∼` containing an admissible region at a prime
  (`exists_leastHull_finite`, `Hull.lean`; componentwise in the residue fields of the packet,
  `ResidueField.lean`); the archimedean counterpart, least polydiscs `a·B_I` (`a` a unit, i.e.
  every component of `a` in the direct sum decomposition of the packet into copies of `ℝ`, `ℂ`
  nonzero), `exists_leastHull_infinite`, is in `Admissible.lean` (IUT III, Remark 3.9.5(i)).
* The indeterminacy automorphisms (`IndAut.lean`): at a prime, all `ℚ_p`-linear automorphisms
  of the packet preserving `⊗_j 𝓘_{c j}` (IUT IV, Proposition 1.2); at `∞`, the maps induced
  by independent actions of `{±1}` on the direct factors `ℝ`, `ℝ·i` of the factors and by the
  automorphisms of the factors (IUT III, Theorem 3.11 (Ind1), (Ind2), Proposition 1.2(vii);
  `ArchIndAut.lean`).
* IUT IV, Proposition 1.4(iii) (`prop14iii_lattice`, `Prop14Lattice.lean`), from Propositions
  1.1 (`PacketDifferent.lean`, `LocalDifferent.lean`) and 1.2 (`LatticeSandwich.lean`).
-/

namespace Iut

open PadicLogVolume

namespace LocalConstruct

open NumberField
open scoped Pointwise

universe u

variable (K : Type u) [Field K] [NumberField K]

/-- **The log-shell of a packet**, uniformly in the rational place (`LocalTheory.logShell`):
the `(R_I)^∼`-module generated by `⊗_j 𝓘_{c j}` at a prime; at the archimedean place the closed
unit ball of the tensor-product Hermitian metric for which the log-shell of each factor (the
closed disc of radius `π`) is the closed unit ball (`archLogShell`; IUT III,
Proposition 3.2(ii)). -/
noncomputable def logShellAt {ι : Type} [Fintype ι] :
    ∀ (vQ : RationalPlace) (c : ι → Place K), Set (Tensor K vQ c)
  | .finite p, c => logShell p c
  | .infinite, c => archLogShell c

variable {K}

lemma logShellAt_finite {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K) :
    logShellAt K (.finite p) c = logShell p c := rfl

lemma logShellAt_infinite {ι : Type} [Fintype ι] (c : ι → Place K) :
    logShellAt K .infinite c = archLogShell c := rfl

variable (K)


end LocalConstruct

/-! ## The local theory of the tensor packets

The constructions of `Iut/Concrete/LocalConstruct/*`, uniformly in the rational place, as
definitions and theorems in the namespace `Iut.LocalTheory` (the base field `K` explicit).
These are the objects and facts consumed by the concrete large volume container
(`Iut/Concrete/Container.lean`) and by the local estimates of IUT IV, Theorem 1.10. -/

namespace LocalTheory

open LocalConstruct NumberField
open scoped Pointwise

variable (K : Type u) [Field K] [NumberField K]

/-- **The tensor packet** `⊗_{j} K_{c j}` over `ℚ_p` (resp. `ℝ`), a topological commutative
ring (a finite product of local fields; IUT III, Proposition 3.1). -/
abbrev Tensor {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K) : Type u :=
  LocalConstruct.Tensor K vQ c

/-- The inclusion `x ↦ 1 ⊗ ⋯ ⊗ x ⊗ ⋯ ⊗ 1` of the `j`-th tensor factor at a nonarchimedean
place. -/
noncomputable abbrev incl {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K) (j : ι)
    (w : FinitePlace K) (h : c j = Place.finite w) : completionAt K w →+* Tensor K (.finite p) c :=
  LocalConstruct.incl p c j w h

/-- **The integral structure**: `(R_I)^∼`, the maximal order of the packet, at a prime (IUT IV,
Proposition 1.2); the product of unit balls `B_I` at the archimedean place (Proposition
1.5(iii)). -/
noncomputable abbrev integral {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K) :
    Set (Tensor K vQ c) :=
  LocalConstruct.integralAt vQ c

/-- **The log-shell of a packet**: at a prime, the `(R_I)^∼`-module generated by the tensor
product of the log-shells `⊗_j 𝓘_{c j}` (which contains `(R_I)^∼`); at `∞`, the closed unit
ball of the tensor-product Hermitian metric (IUT III, Proposition 3.2(ii)), i.e. the closed
ball of radius `π^{|I|}` for the tensor product of the standard metrics of the factors; it
lies in `(√2·π)^{|I|}·B_I` (`prop15`). -/
noncomputable abbrev logShell {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K) :
    Set (Tensor K vQ c) :=
  LocalConstruct.logShellAt K vQ c

/-- **The tensor product of the log-shells** `⊗_j 𝓘_{c j}` at a prime (IUT III,
Proposition 3.2): the `ℤ_p`-span of the elementary tensors of log-shell elements. This is
the base region of the theta-pilot region at a prime (the indeterminacy (Ind3): the Kummer
images of the theta values lie in the log-shells). -/
noncomputable abbrev shell {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K) :
    Set (Tensor K (.finite p) c) :=
  LocalConstruct.tensorLogShell p c

/-- **The normalized Haar log-volume** on regions of a packet (IUT IV, Proposition 1.4(i);
IUT III, Proposition 3.9). -/
noncomputable abbrev componentVol {ι : Type} [Fintype ι] (vQ : RationalPlace)
    (c : ι → Place K) : Set (Tensor K vQ c) → ℝ :=
  LocalConstruct.componentVol vQ c

/-- **The admissible class** of the holomorphic hull (IUT III, Remark 3.9.5(i)): nonempty
relatively compact regions of positive finite Haar measure. -/
noncomputable abbrev admissible {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K) :
    Set (Set (Tensor K vQ c)) :=
  LocalConstruct.admissible vQ c

/-- **The indeterminacy automorphisms** `φ` of IUT IV, Propositions 1.2 and 1.5, through which
the indeterminacies (Ind1), (Ind2) act on the packet: at a prime, every `ℚ_p`-linear
automorphism preserving the lattice `⊗_j 𝓘_{c j}` (equivalently `log_p(R_I^×)`); at `∞`, the
maps `⊗_j ψ_j` with `ψ_j ∈ {id, conj, −1, −conj}` on a factor `ℂ` and `ψ_j = ±1` on a factor `ℝ`
(IUT III, Theorem 3.11 (Ind1), (Ind2), Proposition 1.2(vii)). -/
noncomputable abbrev indAut {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K) :
    Set (Tensor K vQ c → Tensor K vQ c) :=
  LocalConstruct.indAut vQ c

/-- Residue characteristics of finite places are prime. -/
theorem residueChar_prime (w : FinitePlace K) : (residueChar w).Prime :=
  Iut.residueChar_prime w

/-- Finitely many finite places over each prime. -/
theorem fiber_finite (p : ℕ) : Finite {w : FinitePlace K // residueChar w = p} :=
  LocalConstruct.fiber_finite p

/-- Only finitely many finite places are ramified over `ℚ`. -/
theorem ramified_finite : {w : FinitePlace K | ramIdx K w ≠ 1}.Finite :=
  LocalConstruct.ramified_finite

/-- Local degrees are positive. -/
theorem localDeg_pos (w : FinitePlace K) : 0 < localDeg K w :=
  LocalConstruct.localDeg_pos w

/-- The different exponent vanishes at unramified places. -/
theorem ordDifferent_eq_zero (w : FinitePlace K) (h : ramIdx K w = 1) : ordDifferent K w = 0 :=
  LocalConstruct.ordDifferent_eq_zero w h

/-- `∑_{w ∣ p} [K_w : ℚ_p] = [K : ℚ]`. -/
theorem sum_localDeg (p : ℕ) (hp : p.Prime) [Fintype {w : FinitePlace K // residueChar w = p}] :
    ∑ w : {w : FinitePlace K // residueChar w = p}, localDeg K w.1 = Module.finrank ℚ K :=
  LocalConstruct.sum_localDeg p hp

/-- `∑_{w ∣ ∞} [K_w : ℝ] = [K : ℚ]`. -/
theorem sum_mult : ∑ w : InfinitePlace K, w.mult = Module.finrank ℚ K :=
  LocalConstruct.sum_mult

/-- `ord_p` is multiplicative. -/
theorem ordp_mul (w : FinitePlace K) (x y : completionAt K w) (hx : x ≠ 0) (hy : y ≠ 0) :
    ordp K w (x * y) = ordp K w x + ordp K w y :=
  LocalConstruct.ordp_mul w x y hx hy

/-- Units of a factor are units of the packet. -/
theorem isUnit_incl {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K) (j : ι)
    (w : FinitePlace K) (h : c j = Place.finite w) (x : completionAt K w) (hx : x ≠ 0) :
    IsUnit (incl K p c j w h x) :=
  LocalConstruct.isUnit_incl p c j w h x hx

/-- `1 ∈ (R_I)^∼`. -/
theorem one_mem_integral {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K) :
    (1 : Tensor K vQ c) ∈ integral K vQ c :=
  LocalConstruct.one_mem_integralAt vQ c

/-- Scaling by an element of nonnegative `ord_p` shrinks the integral structure. -/
theorem smul_integral_subset {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K) (j : ι)
    (w : FinitePlace K) (h : c j = Place.finite w) (x : completionAt K w) (hx : x ≠ 0)
    (hord : 0 ≤ ordp K w x) :
    incl K p c j w h x • integral K (.finite p) c ⊆ integral K (.finite p) c :=
  LocalConstruct.smul_integral_subset_of_ordp p c j w h x hx hord

/-- Log-shells are relatively compact. -/
theorem logShell_relCompact {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K) :
    IsCompact (closure (logShell K vQ c)) := by
  cases vQ with
  | finite p => exact LocalConstruct.isCompact_closure_logShell p c
  | infinite => exact LocalConstruct.isCompact_closure_archLogShell c

/-- At a prime the log-shell contains the integral structure (IUT III, Proposition 1.2). -/
theorem integral_subset_logShell {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K) :
    integral K (.finite p) c ⊆ logShell K (.finite p) c :=
  LocalConstruct.integral_subset_logShell p c

/-- At an odd prime unramified in every factor the log-shell is the integral structure
(IUT I, Definition 5.4.5; IUT IV, Proposition 1.4(iv)). -/
theorem logShell_eq_integral {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K)
    (hp : Odd (p : ℕ)) (hc : ∀ j w, c j = Place.finite w → ramIdx K w = 1) :
    logShell K (.finite p) c = integral K (.finite p) c :=
  LocalConstruct.logShell_eq_integral_of_unramified p c hp hc

/-- `μ^log((R_I)^∼) = 0`. -/
theorem componentVol_integral {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K) :
    componentVol K vQ c (integral K vQ c) = 0 :=
  LocalConstruct.componentVol_integral

/-- Monotonicity of the log-volume between hull regions `a·O ⊆ b·O` (`a`, `b` units). -/
theorem componentVol_mono {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K)
    (a b : Tensor K vQ c) (ha : IsUnit a) (hb : IsUnit b)
    (hab : a • integral K vQ c ⊆ b • integral K vQ c) :
    componentVol K vQ c (a • integral K vQ c) ≤ componentVol K vQ c (b • integral K vQ c) :=
  LocalConstruct.componentVol_mono a b ha hb hab

/-- Archimedean radial scaling: `μ^log(t·B_I) = log t` for real `t > 0`. -/
theorem componentVol_arch_scale {ι : Type} [Fintype ι] (c : ι → Place K) (t : ℝ) (ht : 0 < t) :
    componentVol K .infinite c (algebraMap ℝ (Tensor K .infinite c) t • integral K .infinite c) =
      Real.log t :=
  LocalConstruct.componentVol_arch_scale t ht

/-- Admissible regions are nonempty. -/
theorem admissible_nonempty {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K)
    (U : Set (Tensor K vQ c)) (hU : U ∈ admissible K vQ c) : U.Nonempty :=
  LocalConstruct.admissible_nonempty hU

/-- Admissible regions are relatively compact. -/
theorem admissible_relCompact {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K)
    (U : Set (Tensor K vQ c)) (hU : U ∈ admissible K vQ c) : IsCompact (closure U) :=
  LocalConstruct.admissible_relCompact hU

/-- The integral structure is admissible. -/
theorem integral_admissible {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K) :
    integral K vQ c ∈ admissible K vQ c :=
  LocalConstruct.integral_admissible

/-- Scaled integral structures are admissible. -/
theorem smul_integral_admissible {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K)
    (a : Tensor K vQ c) (ha : IsUnit a) : a • integral K vQ c ∈ admissible K vQ c :=
  LocalConstruct.smul_integral_admissible a ha

/-- `μ^log(p⁻¹·U) = μ^log(U) + log p` for admissible regions `U` of a packet all of whose
places lie over `p` (IUT III, Proposition 3.9(i)). -/
theorem componentVol_prime_preimage {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K)
    (hc : ∀ j, ∃ w : FinitePlace K, c j = Place.finite w ∧ residueChar w = p)
    (U : Set (Tensor K (.finite p) c)) (hU : U ∈ admissible K (.finite p) c) :
    componentVol K (.finite p) c ((fun x => ((p : ℕ) : Tensor K (.finite p) c) * x) ⁻¹' U) =
      componentVol K (.finite p) c U + Real.log p :=
  LocalConstruct.componentVol_prime_preimage_of_admissible p hc hU

/-- **Existence of least hull regions at a prime** (IUT III, Remark 3.9.5(i)). -/
theorem exists_leastHull {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K)
    (U : Set (Tensor K (.finite p) c)) (hU : U ∈ admissible K (.finite p) c) :
    ∃ a : Tensor K (.finite p) c, IsUnit a ∧ U ⊆ a • integral K (.finite p) c ∧
      ∀ b : Tensor K (.finite p) c, IsUnit b → U ⊆ b • integral K (.finite p) c →
        a • integral K (.finite p) c ⊆ b • integral K (.finite p) c :=
  LocalConstruct.exists_leastHull_finite p c hU

/-- **Existence of least hull regions at the archimedean place** (IUT III, Remark 3.9.5(i);
IUT IV, Proposition 1.5(iii)): every admissible region is contained in a least region `a·B_I`
with `a` a unit (every component of `a` nonzero). -/
theorem exists_leastHull_infinite {ι : Type} [Fintype ι] (c : ι → Place K)
    (U : Set (Tensor K .infinite c)) (hU : U ∈ admissible K .infinite c) :
    ∃ a : Tensor K .infinite c, IsUnit a ∧ U ⊆ a • integral K .infinite c ∧
      ∀ b : Tensor K .infinite c, IsUnit b → U ⊆ b • integral K .infinite c →
        a • integral K .infinite c ⊆ b • integral K .infinite c :=
  LocalConstruct.exists_leastHull_infinite c hU

/-- The radial scalings of `B_I` are monotone. -/
theorem smul_integral_infinite_mono {ι : Type} [Fintype ι] (c : ι → Place K) (t t' : ℝ)
    (ht : 0 < t) (htt' : t ≤ t') :
    algebraMap ℝ (Tensor K .infinite c) t • integral K .infinite c ⊆
      algebraMap ℝ (Tensor K .infinite c) t' • integral K .infinite c :=
  LocalConstruct.smul_integralAt_infinite_mono c t t' ht htt'

/-- The identity is an indeterminacy automorphism. -/
theorem id_mem_indAut {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K) :
    id ∈ indAut K vQ c :=
  LocalConstruct.id_mem_indAut vQ c

/-- The union of the images of a scaled integral structure under the indeterminacy
automorphisms is admissible. -/
theorem theta_admissible {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K)
    (s : Tensor K vQ c) (hs : IsUnit s) :
    (⋃ φ ∈ indAut K vQ c, φ '' (s • integral K vQ c)) ∈ admissible K vQ c :=
  LocalConstruct.theta_admissible vQ c s hs

/-- The union of the images of the log-shell under the indeterminacy automorphisms is
admissible. -/
theorem thetaShell_admissible {ι : Type} [Fintype ι] (vQ : RationalPlace) (c : ι → Place K) :
    (⋃ φ ∈ indAut K vQ c, φ '' logShell K vQ c) ∈ admissible K vQ c := by
  cases vQ with
  | finite p => exact LocalConstruct.tensorAut_thetaShell_admissible p c
  | infinite => exact LocalConstruct.archIndAut_thetaShell_admissible c

/-- **IUT IV, Proposition 1.4(iii)** for the indeterminacy automorphisms of IUT III,
Theorem 3.11 (Ind2) and the log-shell base region (Ind3): for `x ∈ K_{c l}`, `x ≠ 0`, the
images `φ(incl_l(x)·⊗𝓘)` lie in a hull region `a·(R_I)^∼` of log-volume at most
`(−ord_p x + d_I + 1)·log p + ∑_{i ∈ I*} (3 + log e_i) + [l ∈ I*]·(3 + log e_l)`, for packets
all of whose places lie over `p`. -/
theorem prop14_iii {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K)
    (hc : ∀ j, ∃ w : FinitePlace K, c j = Place.finite w ∧ residueChar w = p)
    (d : ι → ℝ) (hd : ∀ i w', c i = Place.finite w' → d i = differentExponent K w')
    (l : ι) (w : FinitePlace K) (h : c l = Place.finite w) (x : completionAt K w)
    (hx : x ≠ 0) :
    ∃ a : Tensor K (.finite p) c, IsUnit a ∧
      (∀ φ ∈ indAut K (.finite p) c,
        φ '' (incl K p c l w h x • shell K p c) ⊆ a • integral K (.finite p) c) ∧
      componentVol K (.finite p) c (a • integral K (.finite p) c) ≤
        (-ordp K w x + ∑ i, d i + 1) * Real.log p +
          (∑ i, if (p : ℕ) - 2 < ramIdxAt K (c i) then
            3 + Real.log (ramIdxAt K (c i)) else 0) +
          (if (p : ℕ) - 2 < ramIdxAt K (c l) then 3 + Real.log (ramIdxAt K (c l)) else 0) :=
  LocalConstruct.prop14iii_shell p c hc d hd l w h x hx

/-- The indeterminacy automorphisms preserve the tensor product of the log-shells. -/
theorem indAut_shell {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K)
    (φ : Tensor K (.finite p) c → Tensor K (.finite p) c) (hφ : φ ∈ indAut K (.finite p) c) :
    φ '' shell K p c = shell K p c := by
  obtain ⟨e, rfl, he⟩ := LocalConstruct.tensorAut_subset_latticeAut p c hφ
  exact he

/-- At an odd prime unramified in every factor, the tensor product of the log-shells is the
integral structure. -/
theorem shell_eq_integral {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K)
    (hc : ∀ j, ∃ w : FinitePlace K, c j = Place.finite w ∧ residueChar w = p)
    (hp : Odd (p : ℕ)) (hunr : ∀ j w, c j = Place.finite w → ramIdx K w = 1) :
    shell K p c = integral K (.finite p) c := by
  change LocalConstruct.tensorLogShell p c = LocalConstruct.integral p c
  rw [LocalConstruct.tensorLogShell_eq_order_of_unramified p c hp hunr,
    LocalConstruct.integral_eq_order_of_unramified p c hc hunr]

/-- The union of the images of a bounded open set of positive measure under the
indeterminacy automorphisms at a prime is admissible. -/
theorem iUnion_indAut_admissible {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K)
    {S : Set (Tensor K (.finite p) c)} (hb : Bornology.IsBounded S) (ho : IsOpen S)
    (hpos : 0 < LocalConstruct.haar (.finite p) c S) :
    (⋃ φ ∈ indAut K (.finite p) c, φ '' S) ∈ admissible K (.finite p) c :=
  LocalConstruct.iUnion_tensorAut_admissible p c hb ho hpos

/-- Scaled tensor products of log-shells are bounded open sets of positive measure. -/
theorem smul_shell_bounded_open_pos {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K)
    (s : Tensor K (.finite p) c) (hs : IsUnit s) :
    Bornology.IsBounded (s • shell K p c) ∧ IsOpen (s • shell K p c) ∧
      0 < LocalConstruct.haar (.finite p) c (s • shell K p c) :=
  LocalConstruct.smul_tensorLogShell_bounded_open_pos p c s hs

/-- **IUT IV, Proposition 1.4(iv)**: at an odd prime unramified in every factor, the
indeterminacy automorphisms preserve `(R_I)^∼`. -/
theorem prop14_iv {ι : Type} [Fintype ι] (p : Nat.Primes) (c : ι → Place K)
    (hc : ∀ j, ∃ w : FinitePlace K, c j = Place.finite w ∧ residueChar w = p)
    (hp : Odd (p : ℕ)) (hunr : ∀ j w, c j = Place.finite w → ramIdx K w = 1) :
    ∀ φ ∈ indAut K (.finite p) c, φ '' integral K (.finite p) c ⊆ integral K (.finite p) c :=
  LocalConstruct.latticeAut_integral_subset p c hc hp hunr

/-- **IUT IV, Proposition 1.5**: at the archimedean place the images of the log-shell (the
unit ball of the tensor-product Hermitian metric) under the indeterminacy automorphisms lie in
`(√2·π)^{|I|}·B_I` (the comparison of the tensor-product and direct-sum metrics). -/
theorem prop15 {ι : Type} [Fintype ι] (c : ι → Place K) :
    ∀ φ ∈ indAut K .infinite c, φ '' logShell K .infinite c ⊆
      algebraMap ℝ (Tensor K .infinite c) ((Real.sqrt 2 * Real.pi) ^ Fintype.card ι) •
        integral K .infinite c :=
  LocalConstruct.archIndAut_prop15 c

/-- **IUT IV, Theorem 1.10, Step (vii)**: the holomorphic hull `a·B_I` of the archimedean theta
region (the union of the images of the log-shell under the indeterminacy automorphisms) has
log-volume at most `|I|·log(√2·π)`. -/
theorem componentVol_hull_thetaShell_le {ι : Type} [Fintype ι] (c : ι → Place K)
    (a : Tensor K .infinite c) (ha : IsUnit a)
    (hleast : ∀ b : Tensor K .infinite c, IsUnit b →
      (⋃ φ ∈ indAut K .infinite c, φ '' logShell K .infinite c) ⊆ b • integral K .infinite c →
        a • integral K .infinite c ⊆ b • integral K .infinite c) :
    componentVol K .infinite c (a • integral K .infinite c) ≤
      Fintype.card ι * Real.log (Real.sqrt 2 * Real.pi) := by
  have hb := LocalConstruct.isUnit_archScalar c
  refine (componentVol_mono K .infinite c a _ ha hb (hleast _ hb
    (Set.iUnion₂_subset fun φ hφ => prop15 K c φ hφ))).trans_eq ?_
  rw [componentVol_arch_scale K c _ (pow_pos LocalConstruct.archHullRadius_pos _),
    Real.log_pow, LocalConstruct.archHullRadius]

end LocalTheory

end Iut