1. ElevenTwelfths
  2. ActualFixedShellModels
import OAI.NumberTheory.DirichletL.RowCompletion.BranchDecoding

Actual fixed-shell models from branch decoding

This fixed-shell construction is adapted from OpenAI's row-completion sources at commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. It imports only the immediate lower-level module BranchDecoding and exposes the fixed-shell identity and model interface needed by the direct 11 / 12 argument. The nonvanishing conclusion is proved later, in ElevenTwelfths.Unconditional.

namespace ElevenTwelfthsnoncomputable sectionopen scoped BigOperators Classical SchwartzMap ContDiffopen OAIopen OAI.ActualEisensteinCubicopen OAI.CanonicalRowCompletionopen OAI.CanonicalRowCompletion.ActualFiberopen OAI.CanonicalCoefficientClassopen OAI.CanonicalQuadraticSieveopen OAI.CompletedGaussopen OAI.CubicEisensteinopen OAI.InitialMeanSquareopen UniqueFactorizationMonoidnamespace ActualFixedShellModelslocal notation "Eis" => OAI.ActualEisensteinCubic.Ononcomputable local instance collectionUnitsFintype : Fintype Eisˣ := ⊢ Fintype Eisˣ this:Finite Eisˣ := ···⊢ Fintype Eisˣ All goals completed! 🐙variable (q : ℕ) (hq : q ≠ 0) (m : Eis) (hm : m ≠ 0) (rows : Finset (Ideal Eis)) (R F : Ideal Eis) (hR : R ≠ 0) (hF : Squarefree F) (hrows : ∀ I ∈ rows, I ≠ 0) (v : Eisˣ)variable [Fintype (Eis ⧸ Ideal.span {reflectionConductor q})]theorem reflectedFiber_four_mul_value_local (K : ℝ) (Ψ : Eis →* ℂ) (hΨ : ∀ n, ‖Ψ n‖ ≤ 1) (hbound : ∀ I ∈ rows, (Ideal.absNorm I : ℝ) ≤ K) (J : RowIndex q m rows R F) (W : ℝ → ℂ) (lo hi : ℝ) (hlo : 0 < lo) (hsupp : Function.support W ⊆ Set.Icc lo hi) (hW : ContDiff ℝ ∞ W) (X : ℝ) (hX : 0 < X) (hK : 0 < completedResidualScale K R (maskIdeal q m F)) (hk : completedResidualScale K R (maskIdeal q m F) / 2 ≤ (Ideal.absNorm (rowResidualPart J.val (maskIdeal q m F)) : ℝ)) : let k := fiberResidualIndex rows R (maskIdeal q m F) K (mask_bad q m F) (fun I hI ↦ ⟨hrows I hI, hbound I hI⟩) J 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X := q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))⊢ let k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))this:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Fintype (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun x => Fintype.ofFinite (fixedFourierGeometry (reflectionConductor q) ⋯ x).PhaseResidue⊢ let k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))this:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Fintype (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun x => Fintype.ofFinite (fixedFourierGeometry (reflectionConductor q) ⋯ x).PhaseResidued:ReflectedFiberData (fixedReflectionRayCount (reflectionConductor q) ⋯) (fixedCuspLevelBound (reflectionConductor q)) K R F (maskIdeal q m F) := reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ⊢ let k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))this:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Fintype (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun x => Fintype.ofFinite (fixedFourierGeometry (reflectionConductor q) ⋯ x).PhaseResidued:ReflectedFiberData (fixedReflectionRayCount (reflectionConductor q) ⋯) (fixedCuspLevelBound (reflectionConductor q)) K R F (maskIdeal q m F) := reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J⊢ let k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))this:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Fintype (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun x => Fintype.ofFinite (fixedFourierGeometry (reflectionConductor q) ⋯ x).PhaseResidued:ReflectedFiberData (fixedReflectionRayCount (reflectionConductor q) ⋯) (fixedCuspLevelBound (reflectionConductor q)) K R F (maskIdeal q m F) := reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jf:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h rho u B l => (d.branch ((fixedReflectionRayEquiv (reflectionConductor q) ⋯) ⟨h, (rho, u)⟩, encodeReflectionSix ⟨B, l⟩)).value W X 1 completedRamifiedStep k⊢ let k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))this:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Fintype (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun x => Fintype.ofFinite (fixedFourierGeometry (reflectionConductor q) ⋯ x).PhaseResidued:ReflectedFiberData (fixedReflectionRayCount (reflectionConductor q) ⋯) (fixedCuspLevelBound (reflectionConductor q)) K R F (maskIdeal q m F) := reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jf:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h rho u B l => (d.branch ((fixedReflectionRayEquiv (reflectionConductor q) ⋯) ⟨h, (rho, u)⟩, encodeReflectionSix ⟨B, l⟩)).value W X 1 completedRamifiedStep kg:Eis ⧸ Ideal.span {reflectionConductor q} → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h u B l => sourceCompressedTerm q hq m hm rows R F hR hF hrows v h B J u l W X⊢ let k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))this:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Fintype (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun x => Fintype.ofFinite (fixedFourierGeometry (reflectionConductor q) ⋯ x).PhaseResidued:ReflectedFiberData (fixedReflectionRayCount (reflectionConductor q) ⋯) (fixedCuspLevelBound (reflectionConductor q)) K R F (maskIdeal q m F) := reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jf:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h rho u B l => (d.branch ((fixedReflectionRayEquiv (reflectionConductor q) ⋯) ⟨h, (rho, u)⟩, encodeReflectionSix ⟨B, l⟩)).value W X 1 completedRamifiedStep kg:Eis ⧸ Ideal.span {reflectionConductor q} → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h u B l => sourceCompressedTerm q hq m hm rows R F hR hF hrows v h B J u l W Xchosen:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun h B => (data q m hm rows R F hF hrows v J).sourceRowResidue (fixedBaseConductor q) (reflectionConductor q) ⋯ h (fixedFourierGeometry (reflectionConductor q) ⋯ h) (sourcePrimeSet q hq m hm rows R F hR hF hrows v B J)⊢ let k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))this:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Fintype (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun x => Fintype.ofFinite (fixedFourierGeometry (reflectionConductor q) ⋯ x).PhaseResidued:ReflectedFiberData (fixedReflectionRayCount (reflectionConductor q) ⋯) (fixedCuspLevelBound (reflectionConductor q)) K R F (maskIdeal q m F) := reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jf:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h rho u B l => (d.branch ((fixedReflectionRayEquiv (reflectionConductor q) ⋯) ⟨h, (rho, u)⟩, encodeReflectionSix ⟨B, l⟩)).value W X 1 completedRamifiedStep kg:Eis ⧸ Ideal.span {reflectionConductor q} → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h u B l => sourceCompressedTerm q hq m hm rows R F hR hF hrows v h B J u l W Xchosen:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun h B => (data q m hm rows R F hF hrows v J).sourceRowResidue (fixedBaseConductor q) (reflectionConductor q) ⋯ h (fixedFourierGeometry (reflectionConductor q) ⋯ h) (sourcePrimeSet q hq m hm rows R F hR hF hrows v B J)alpha:Eis ⧸ Ideal.span {reflectionConductor q} → ℂ := fun h => sourceFixedCoefficient q hq m hm rows R F hF hrows v Ψ h J⊢ let k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))this:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Fintype (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun x => Fintype.ofFinite (fixedFourierGeometry (reflectionConductor q) ⋯ x).PhaseResidued:ReflectedFiberData (fixedReflectionRayCount (reflectionConductor q) ⋯) (fixedCuspLevelBound (reflectionConductor q)) K R F (maskIdeal q m F) := reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jf:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h rho u B l => (d.branch ((fixedReflectionRayEquiv (reflectionConductor q) ⋯) ⟨h, (rho, u)⟩, encodeReflectionSix ⟨B, l⟩)).value W X 1 completedRamifiedStep kg:Eis ⧸ Ideal.span {reflectionConductor q} → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h u B l => sourceCompressedTerm q hq m hm rows R F hR hF hrows v h B J u l W Xchosen:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun h B => (data q m hm rows R F hF hrows v J).sourceRowResidue (fixedBaseConductor q) (reflectionConductor q) ⋯ h (fixedFourierGeometry (reflectionConductor q) ⋯ h) (sourcePrimeSet q hq m hm rows R F hR hF hrows v B J)alpha:Eis ⧸ Ideal.span {reflectionConductor q} → ℂ := fun h => sourceFixedCoefficient q hq m hm rows R F hF hrows v Ψ h Jshape:Eis ⧸ Ideal.span {reflectionConductor q} → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → ℂ := fun h B => sourceShapeFactor q hq m hm rows R F hR hF hrows v h B J⊢ let k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))this:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Fintype (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun x => Fintype.ofFinite (fixedFourierGeometry (reflectionConductor q) ⋯ x).PhaseResidued:ReflectedFiberData (fixedReflectionRayCount (reflectionConductor q) ⋯) (fixedCuspLevelBound (reflectionConductor q)) K R F (maskIdeal q m F) := reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jf:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h rho u B l => (d.branch ((fixedReflectionRayEquiv (reflectionConductor q) ⋯) ⟨h, (rho, u)⟩, encodeReflectionSix ⟨B, l⟩)).value W X 1 completedRamifiedStep kg:Eis ⧸ Ideal.span {reflectionConductor q} → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h u B l => sourceCompressedTerm q hq m hm rows R F hR hF hrows v h B J u l W Xchosen:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun h B => (data q m hm rows R F hF hrows v J).sourceRowResidue (fixedBaseConductor q) (reflectionConductor q) ⋯ h (fixedFourierGeometry (reflectionConductor q) ⋯ h) (sourcePrimeSet q hq m hm rows R F hR hF hrows v B J)alpha:Eis ⧸ Ideal.span {reflectionConductor q} → ℂ := fun h => sourceFixedCoefficient q hq m hm rows R F hF hrows v Ψ h Jshape:Eis ⧸ Ideal.span {reflectionConductor q} → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → ℂ := fun h B => sourceShapeFactor q hq m hm rows R F hR hF hrows v h B Jw:Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → ℂ := FreeReflection.reflectionInactiveStratumWeight R F (maskIdeal q m F) (freeConductor q)⊢ let k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))this:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Fintype (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun x => Fintype.ofFinite (fixedFourierGeometry (reflectionConductor q) ⋯ x).PhaseResidued:ReflectedFiberData (fixedReflectionRayCount (reflectionConductor q) ⋯) (fixedCuspLevelBound (reflectionConductor q)) K R F (maskIdeal q m F) := reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jf:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h rho u B l => (d.branch ((fixedReflectionRayEquiv (reflectionConductor q) ⋯) ⟨h, (rho, u)⟩, encodeReflectionSix ⟨B, l⟩)).value W X 1 completedRamifiedStep kg:Eis ⧸ Ideal.span {reflectionConductor q} → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h u B l => sourceCompressedTerm q hq m hm rows R F hR hF hrows v h B J u l W Xchosen:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun h B => (data q m hm rows R F hF hrows v J).sourceRowResidue (fixedBaseConductor q) (reflectionConductor q) ⋯ h (fixedFourierGeometry (reflectionConductor q) ⋯ h) (sourcePrimeSet q hq m hm rows R F hR hF hrows v B J)alpha:Eis ⧸ Ideal.span {reflectionConductor q} → ℂ := fun h => sourceFixedCoefficient q hq m hm rows R F hF hrows v Ψ h Jshape:Eis ⧸ Ideal.span {reflectionConductor q} → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → ℂ := fun h B => sourceShapeFactor q hq m hm rows R F hR hF hrows v h B Jw:Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → ℂ := FreeReflection.reflectionInactiveStratumWeight R F (maskIdeal q m F) (freeConductor q)hbranch:∀ (h : Eis ⧸ Ideal.span {reflectionConductor q}) (rho : (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue) (u : Eisˣ) (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) (l : ↥B → Fin 3), 4 * f h rho u B l = if rho = chosen h B then alpha h * shape h B * g h u B l else 0⊢ let k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))this:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Fintype (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun x => Fintype.ofFinite (fixedFourierGeometry (reflectionConductor q) ⋯ x).PhaseResidued:ReflectedFiberData (fixedReflectionRayCount (reflectionConductor q) ⋯) (fixedCuspLevelBound (reflectionConductor q)) K R F (maskIdeal q m F) := reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jf:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h rho u B l => (d.branch ((fixedReflectionRayEquiv (reflectionConductor q) ⋯) ⟨h, (rho, u)⟩, encodeReflectionSix ⟨B, l⟩)).value W X 1 completedRamifiedStep kg:Eis ⧸ Ideal.span {reflectionConductor q} → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h u B l => sourceCompressedTerm q hq m hm rows R F hR hF hrows v h B J u l W Xchosen:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun h B => (data q m hm rows R F hF hrows v J).sourceRowResidue (fixedBaseConductor q) (reflectionConductor q) ⋯ h (fixedFourierGeometry (reflectionConductor q) ⋯ h) (sourcePrimeSet q hq m hm rows R F hR hF hrows v B J)alpha:Eis ⧸ Ideal.span {reflectionConductor q} → ℂ := fun h => sourceFixedCoefficient q hq m hm rows R F hF hrows v Ψ h Jshape:Eis ⧸ Ideal.span {reflectionConductor q} → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → ℂ := fun h B => sourceShapeFactor q hq m hm rows R F hR hF hrows v h B Jw:Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → ℂ := FreeReflection.reflectionInactiveStratumWeight R F (maskIdeal q m F) (freeConductor q)hbranch:∀ (h : Eis ⧸ Ideal.span {reflectionConductor q}) (rho : (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue) (u : Eisˣ) (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) (l : ↥B → Fin 3), 4 * f h rho u B l = if rho = chosen h B then alpha h * shape h B * g h u B l else 0hvalue:d.value W X 1 completedRamifiedStep k = ∑ h, ∑ rho, ∑ u, ∑ B, w B * ∑ l, f h rho u B l⊢ let k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))this:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Fintype (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun x => Fintype.ofFinite (fixedFourierGeometry (reflectionConductor q) ⋯ x).PhaseResidued:ReflectedFiberData (fixedReflectionRayCount (reflectionConductor q) ⋯) (fixedCuspLevelBound (reflectionConductor q)) K R F (maskIdeal q m F) := reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jf:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h rho u B l => (d.branch ((fixedReflectionRayEquiv (reflectionConductor q) ⋯) ⟨h, (rho, u)⟩, encodeReflectionSix ⟨B, l⟩)).value W X 1 completedRamifiedStep kg:Eis ⧸ Ideal.span {reflectionConductor q} → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h u B l => sourceCompressedTerm q hq m hm rows R F hR hF hrows v h B J u l W Xchosen:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun h B => (data q m hm rows R F hF hrows v J).sourceRowResidue (fixedBaseConductor q) (reflectionConductor q) ⋯ h (fixedFourierGeometry (reflectionConductor q) ⋯ h) (sourcePrimeSet q hq m hm rows R F hR hF hrows v B J)alpha:Eis ⧸ Ideal.span {reflectionConductor q} → ℂ := fun h => sourceFixedCoefficient q hq m hm rows R F hF hrows v Ψ h Jshape:Eis ⧸ Ideal.span {reflectionConductor q} → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → ℂ := fun h B => sourceShapeFactor q hq m hm rows R F hR hF hrows v h B Jw:Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → ℂ := FreeReflection.reflectionInactiveStratumWeight R F (maskIdeal q m F) (freeConductor q)hbranch:∀ (h : Eis ⧸ Ideal.span {reflectionConductor q}) (rho : (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue) (u : Eisˣ) (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) (l : ↥B → Fin 3), 4 * f h rho u B l = if rho = chosen h B then alpha h * shape h B * g h u B l else 0hvalue:d.value W X 1 completedRamifiedStep k = ∑ h, ∑ rho, ∑ u, ∑ B, w B * ∑ l, f h rho u B l⊢ 4 * d.value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})K:ℝΨ:Eis →* ℂhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1hbound:∀ I ∈ rows, ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < XhK:0 < completedResidualScale K R (maskIdeal q m F)hk:completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))this:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Fintype (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun x => Fintype.ofFinite (fixedFourierGeometry (reflectionConductor q) ⋯ x).PhaseResidued:ReflectedFiberData (fixedReflectionRayCount (reflectionConductor q) ⋯) (fixedCuspLevelBound (reflectionConductor q)) K R F (maskIdeal q m F) := reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jf:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h rho u B l => (d.branch ((fixedReflectionRayEquiv (reflectionConductor q) ⋯) ⟨h, (rho, u)⟩, encodeReflectionSix ⟨B, l⟩)).value W X 1 completedRamifiedStep kg:Eis ⧸ Ideal.span {reflectionConductor q} → Eisˣ → (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) → (↥B → Fin 3) → ℂ := fun h u B l => sourceCompressedTerm q hq m hm rows R F hR hF hrows v h B J u l W Xchosen:(h : Eis ⧸ Ideal.span {reflectionConductor q}) → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue := fun h B => (data q m hm rows R F hF hrows v J).sourceRowResidue (fixedBaseConductor q) (reflectionConductor q) ⋯ h (fixedFourierGeometry (reflectionConductor q) ⋯ h) (sourcePrimeSet q hq m hm rows R F hR hF hrows v B J)alpha:Eis ⧸ Ideal.span {reflectionConductor q} → ℂ := fun h => sourceFixedCoefficient q hq m hm rows R F hF hrows v Ψ h Jshape:Eis ⧸ Ideal.span {reflectionConductor q} → Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → ℂ := fun h B => sourceShapeFactor q hq m hm rows R F hR hF hrows v h B Jw:Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q)) → ℂ := FreeReflection.reflectionInactiveStratumWeight R F (maskIdeal q m F) (freeConductor q)hbranch:∀ (h : Eis ⧸ Ideal.span {reflectionConductor q}) (rho : (fixedFourierGeometry (reflectionConductor q) ⋯ h).PhaseResidue) (u : Eisˣ) (B : Finset ↥(FreeReflection.pool R (maskIdeal q m F) (freeConductor q))) (l : ↥B → Fin 3), 4 * f h rho u B l = if rho = chosen h B then alpha h * shape h B * g h u B l else 0hvalue:d.value W X 1 completedRamifiedStep k = ∑ h, ∑ rho, ∑ u, ∑ B, w B * ∑ l, f h rho u B l⊢ 4 * ∑ h, ∑ rho, ∑ u, ∑ B, w B * ∑ l, f h rho u B l = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X All goals completed! 🐙theorem completedT_eq_reflectedFiber_idealValue_local (Ψ : Eis →* ℂ) (hΨperiod : OAI.CanonicalCoefficientClass.FactorsModulo (OAI.CanonicalCoefficientClass.fixedBaseConductor q) Ψ) (hΨ : ∀ n, ‖Ψ n‖ ≤ 1) (K : ℝ) (hshell : ∀ I ∈ rows, K / 2 ≤ (Ideal.absNorm I : ℝ) ∧ (Ideal.absNorm I : ℝ) ≤ K) (J : RowIndex q m rows R F) (W : ℝ → ℂ) (lo hi : ℝ) (hlo : 0 < lo) (hsupp : Function.support W ⊆ Set.Icc lo hi) (hW : ContDiff ℝ ∞ W) (X : ℝ) (hX : 0 < X) : completedT (rowTwist Ψ (maskElement q m) (OAI.ConcretePrimeRowBridge.idealGenerator F) (v.val * OAI.ConcretePrimeRowBridge.idealGenerator J.val)) W X = (4 * thetaDerivativeScalar⁻¹ * fixedRadialCoefficientScalar) * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).idealValue W X 1 completedRamifiedStep (rowResidualPart J.val (maskIdeal q m F)) := q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})Ψ:Eis →* ℂhΨperiod:FactorsModulo (fixedBaseConductor q) ΨhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1K:ℝhshell:∀ I ∈ rows, K / 2 ≤ ↑(Ideal.absNorm I) ∧ ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < X⊢ completedT (rowTwist Ψ (maskElement q m) (ConcretePrimeRowBridge.idealGenerator F) (↑v * ConcretePrimeRowBridge.idealGenerator ↑J)) W X = 4 * thetaDerivativeScalar⁻¹ * fixedRadialCoefficientScalar * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).idealValue W X 1 completedRamifiedStep (rowResidualPart (↑J) (maskIdeal q m F)) q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})Ψ:Eis →* ℂhΨperiod:FactorsModulo (fixedBaseConductor q) ΨhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1K:ℝhshell:∀ I ∈ rows, K / 2 ≤ ↑(Ideal.absNorm I) ∧ ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < Xk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J⊢ completedT (rowTwist Ψ (maskElement q m) (ConcretePrimeRowBridge.idealGenerator F) (↑v * ConcretePrimeRowBridge.idealGenerator ↑J)) W X = 4 * thetaDerivativeScalar⁻¹ * fixedRadialCoefficientScalar * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).idealValue W X 1 completedRamifiedStep (rowResidualPart (↑J) (maskIdeal q m F)) q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})Ψ:Eis →* ℂhΨperiod:FactorsModulo (fixedBaseConductor q) ΨhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1K:ℝhshell:∀ I ∈ rows, K / 2 ≤ ↑(Ideal.absNorm I) ∧ ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < Xk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jhs:0 < completedResidualScale K R (maskIdeal q m F) ∧ completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))⊢ completedT (rowTwist Ψ (maskElement q m) (ConcretePrimeRowBridge.idealGenerator F) (↑v * ConcretePrimeRowBridge.idealGenerator ↑J)) W X = 4 * thetaDerivativeScalar⁻¹ * fixedRadialCoefficientScalar * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).idealValue W X 1 completedRamifiedStep (rowResidualPart (↑J) (maskIdeal q m F)) q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})Ψ:Eis →* ℂhΨperiod:FactorsModulo (fixedBaseConductor q) ΨhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1K:ℝhshell:∀ I ∈ rows, K / 2 ≤ ↑(Ideal.absNorm I) ∧ ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < Xk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jhs:0 < completedResidualScale K R (maskIdeal q m F) ∧ completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))he:have k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X⊢ completedT (rowTwist Ψ (maskElement q m) (ConcretePrimeRowBridge.idealGenerator F) (↑v * ConcretePrimeRowBridge.idealGenerator ↑J)) W X = 4 * thetaDerivativeScalar⁻¹ * fixedRadialCoefficientScalar * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).idealValue W X 1 completedRamifiedStep (rowResidualPart (↑J) (maskIdeal q m F)) q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})Ψ:Eis →* ℂhΨperiod:FactorsModulo (fixedBaseConductor q) ΨhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1K:ℝhshell:∀ I ∈ rows, K / 2 ≤ ↑(Ideal.absNorm I) ∧ ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < Xk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jhs:0 < completedResidualScale K R (maskIdeal q m F) ∧ completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))he:have k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W X⊢ thetaDerivativeScalar⁻¹ * fixedRadialCoefficientScalar * (4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep (fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J)) = 4 * thetaDerivativeScalar⁻¹ * fixedRadialCoefficientScalar * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).idealValue W X 1 completedRamifiedStep (rowResidualPart (↑J) (maskIdeal q m F)) q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})Ψ:Eis →* ℂhΨperiod:FactorsModulo (fixedBaseConductor q) ΨhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1K:ℝhshell:∀ I ∈ rows, K / 2 ≤ ↑(Ideal.absNorm I) ∧ ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < Xk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jhs:0 < completedResidualScale K R (maskIdeal q m F) ∧ completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))he:have k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W Xhid:rowResidualPart (↑J) (maskIdeal q m F) = ↑k⊢ thetaDerivativeScalar⁻¹ * fixedRadialCoefficientScalar * (4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep (fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J)) = 4 * thetaDerivativeScalar⁻¹ * fixedRadialCoefficientScalar * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).idealValue W X 1 completedRamifiedStep (rowResidualPart (↑J) (maskIdeal q m F)) q:ℕhq:q ≠ 0m:Eishm:m ≠ 0rows:Finset (Ideal Eis)R:Ideal EisF:Ideal EishR:R ≠ 0hF:Squarefree Fhrows:∀ I ∈ rows, I ≠ 0v:Eisˣinst✝:Fintype (Eis ⧸ Ideal.span {reflectionConductor q})Ψ:Eis →* ℂhΨperiod:FactorsModulo (fixedBaseConductor q) ΨhΨ:∀ (n : Eis), ‖Ψ n‖ ≤ 1K:ℝhshell:∀ I ∈ rows, K / 2 ≤ ↑(Ideal.absNorm I) ∧ ↑(Ideal.absNorm I) ≤ KJ:↥(RowIndex q m rows R F)W:ℝ → ℂlo:ℝhi:ℝhlo:0 < lohsupp:Function.support W ⊆ Set.Icc lo hihW:ContDiff ℝ ∞ WX:ℝhX:0 < Xk:↥(idealRange (completedResidualScale K R (maskIdeal q m F))) := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ Jhs:0 < completedResidualScale K R (maskIdeal q m F) ∧ completedResidualScale K R (maskIdeal q m F) / 2 ≤ ↑(Ideal.absNorm (rowResidualPart (↑J) (maskIdeal q m F)))he:have k := fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J; 4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k = compressedSourceTotal q hq m hm rows R F hR hF hrows v Ψ J W Xhid:rowResidualPart (↑J) (maskIdeal q m F) = ↑k⊢ thetaDerivativeScalar⁻¹ * fixedRadialCoefficientScalar * (4 * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep (fiberResidualIndex rows R (maskIdeal q m F) K ⋯ ⋯ J)) = 4 * thetaDerivativeScalar⁻¹ * fixedRadialCoefficientScalar * (reflectedFiber q hq m hm rows R F hR hF hrows v K Ψ hΨ).value W X 1 completedRamifiedStep k All goals completed! 🐙def actualReflectionScale : ℂ := 4 * thetaDerivativeScalar⁻¹ * fixedRadialCoefficientScalartheorem actual_fixedShellModels (q : ℕ) (hq : q ≠ 0) (chi : DirichletCharacter ℂ q) : HasFixedShellModels (reflectionExcludedPrimes q) (initialBase chi) (fixedReflectionRayCount (reflectionConductor q) (reflectionConductor_ne_zero q hq)) actualReflectionScale 1 completedRamifiedStep (fixedCuspLevelBound (reflectionConductor q)) := q:ℕhq:q ≠ 0chi:DirichletCharacter ℂ q⊢ HasFixedShellModels (reflectionExcludedPrimes q) (initialBase chi) (fixedReflectionRayCount (reflectionConductor q) ⋯) actualReflectionScale 1 completedRamifiedStep (fixedCuspLevelBound (reflectionConductor q)) q:ℕhq:q ≠ 0chi:DirichletCharacter ℂ qthis:Finite (Eis ⧸ Ideal.span {reflectionConductor q}) := ···⊢ HasFixedShellModels (reflectionExcludedPrimes q) (initialBase chi) (fixedReflectionRayCount (reflectionConductor q) ⋯) actualReflectionScale 1 completedRamifiedStep (fixedCuspLevelBound (reflectionConductor q)) q:ℕhq:q ≠ 0chi:DirichletCharacter ℂ qthis✝:Finite (Eis ⧸ Ideal.span {reflectionConductor q}) := ···this:Fintype (Eis ⧸ Ideal.span {reflectionConductor q}) := Fintype.ofFinite (Eis ⧸ Ideal.span {reflectionConductor q})⊢ HasFixedShellModels (reflectionExcludedPrimes q) (initialBase chi) (fixedReflectionRayCount (reflectionConductor q) ⋯) actualReflectionScale 1 completedRamifiedStep (fixedCuspLevelBound (reflectionConductor q)) q:ℕhq:q ≠ 0chi:DirichletCharacter ℂ qthis✝:Finite (Eis ⧸ Ideal.span {reflectionConductor q}) := ···this:Fintype (Eis ⧸ Ideal.span {reflectionConductor q}) := Fintype.ofFinite (Eis ⧸ Ideal.span {reflectionConductor q})⊢ ∀ (Ψ : Eis →* ℂ), FactorsModulo (fixedBaseConductor q) Ψ → ∀ (hΨnorm : ∀ (n : Eis), ‖Ψ n‖ ≤ 1) (m : Eis) (hm : m ≠ 0) (F : Ideal Eis) (hF : Squarefree F) (u : Eisˣ) (W : ℝ → ℂ) (a b : ℝ), 0 < a → Function.support W ⊆ Set.Icc a b → ContDiff ℝ ∞ W → ∀ (K X : ℝ), 0 < K → 0 < X → ∀ (rows : Finset (Ideal Eis)) (hrows : ∀ I ∈ rows, I ≠ 0 ∧ K / 2 ≤ ↑(Ideal.absNorm I) ∧ ↑(Ideal.absNorm I) ≤ K) (R : Ideal Eis) (hR : R ∈ rows) (J : ↥(RowIndex q m rows R F)), completedT (rowTwist Ψ (maskElement q m) (ConcretePrimeRowBridge.idealGenerator F) (↑u * ConcretePrimeRowBridge.idealGenerator ↑J)) W X = actualReflectionScale * (reflectedFiber q hq m hm rows R F ⋯ hF ⋯ u K Ψ hΨnorm).idealValue W X 1 completedRamifiedStep (rowResidualPart (↑J) (maskIdeal q m F)) q:ℕhq:q ≠ 0chi:DirichletCharacter ℂ qthis✝:Finite (Eis ⧸ Ideal.span {reflectionConductor q}) := ···this:Fintype (Eis ⧸ Ideal.span {reflectionConductor q}) := Fintype.ofFinite (Eis ⧸ Ideal.span {reflectionConductor q})Ψ:Eis →* ℂhperiod:FactorsModulo (fixedBaseConductor q) Ψhnorm:∀ (n : Eis), ‖Ψ n‖ ≤ 1m:Eishm:m ≠ 0F:Ideal EishF:Squarefree Fu:EisˣW:ℝ → ℂa:ℝb:ℝha:0 < ahs:Function.support W ⊆ Set.Icc a bhW:ContDiff ℝ ∞ WK:ℝX:ℝhK:0 < KhX:0 < Xrows:Finset (Ideal Eis)hrows:∀ I ∈ rows, I ≠ 0 ∧ K / 2 ≤ ↑(Ideal.absNorm I) ∧ ↑(Ideal.absNorm I) ≤ KR:Ideal EishR:R ∈ rowsJ:↥(RowIndex q m rows R F)⊢ completedT (rowTwist Ψ (maskElement q m) (ConcretePrimeRowBridge.idealGenerator F) (↑u * ConcretePrimeRowBridge.idealGenerator ↑J)) W X = actualReflectionScale * (reflectedFiber q hq m hm rows R F ⋯ hF ⋯ u K Ψ hnorm).idealValue W X 1 completedRamifiedStep (rowResidualPart (↑J) (maskIdeal q m F)) All goals completed! 🐙theorem exists_actual_fixedShellModels (q : ℕ) [NeZero q] (chi : DirichletCharacter ℂ q) : ∃ (rays : ℕ) (scale : ℂ), HasFixedShellModels (reflectionExcludedPrimes q) (initialBase chi) rays scale 1 completedRamifiedStep (fixedCuspLevelBound (reflectionConductor q)) := q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ q⊢ ∃ rays scale, HasFixedShellModels (reflectionExcludedPrimes q) (initialBase chi) rays scale 1 completedRamifiedStep (fixedCuspLevelBound (reflectionConductor q)) All goals completed! 🐙end ActualFixedShellModels

The concrete Voronoi construction supplies the theta models used by the mean square. Kept separate from amplification and nonvanishing so the family estimate can use it directly.

theorem actual_hasCanonicalThetaModels (q : ℕ) [NeZero q] (chi : DirichletCharacter ℂ q) : HasCanonicalThetaModels (reflectionExcludedPrimes q) (conjugateMonoid (normCharacter chi)) 1 completedRamifiedStep (fixedCuspLevelBound (reflectionConductor q)) := q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ q⊢ HasCanonicalThetaModels (reflectionExcludedPrimes q) (conjugateMonoid (normCharacter chi)) 1 completedRamifiedStep (fixedCuspLevelBound (reflectionConductor q)) q:ℕinst✝:NeZero qchi:DirichletCharacter ℂ qrays:ℕscale:ℂhfixed:HasFixedShellModels (reflectionExcludedPrimes q) (initialBase chi) rays scale 1 completedRamifiedStep (fixedCuspLevelBound (reflectionConductor q))⊢ HasCanonicalThetaModels (reflectionExcludedPrimes q) (conjugateMonoid (normCharacter chi)) 1 completedRamifiedStep (fixedCuspLevelBound (reflectionConductor q)) All goals completed! 🐙endend ElevenTwelfths