/-
Copyright (c) 2026 Yawara Ishida. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yawara Ishida
-/
import OddOrder.FeitThompsonCharacterData

/-!
# Feit–Thompson Section 16 assembly and odd-order theorem

Peterfalvi §§13–16 (pp. 64–92) and BG Appendix C: construct the named
Section 16 inputs, derive the final contradiction, and perform the
minimal-counterexample reduction.
-/

namespace OddOrder
open OddOrder.BG
open OddOrder.GroupTheory
open OddOrder.Isaacs
open OddOrder.RepresentationTheory
open scoped Pointwise

universe u

section
open scoped OddOrder.Peterfalvi.S15.FiniteInduce


/-- **Peterfalvi §13 coherent Dade-grid producer** (`sorry`-free) — *lane-b*
(Peterfalvi §3–§13 coherent grids).  Given the maximal pair and the type-P
structure, constructs the character grids `ω, μ, ν`, the signs `δ, δ'`, the integral
maps, and the induction identities (13.1.d/e).

The mathematically substantive fields are the genuine §13 grid:
* `omega := omegaS` — the shared `ω`-grid, materialized from the certain-type machinery of
  `mp.S` (`certainTypeS`, indexed by `mp.K`, `mp.Kstar` and aligned to `tp.W₁, tp.W₂` via
  `tp.W1_eq_K`/`W2_eq_Kstar`).  `omegaS_eq_omegaT` proves it equals the T-side reconstruction, so
  the single `ω`-field satisfies *both* induction identities;
* `mu := muS`, `nu := nuT`, `delta := deltaS`, `deltaPrime := deltaPrimeT` — the induced
  exceptional characters and signs read off `certainTypeS`/`certainTypeT`'s `columnFamily`;
* `tau3 := tau3W` — the genuine §3.2 Dade σ-integral of the G-internal TI-cyclic structure on
  `W = S ∩ T`, supported on `Ẑ = W \ (W₁ ∪ W₂)` (built from the proven BG Theorem 14.7 TI fact and
  the general §4 Dade producer; `#print axioms` is `sorryAx`-free);
* `mu_definition := muS_definition`, `nu_definition := nuT_definition` — Peterfalvi (13.1.e),
  proven `sorry`-free.

**Vestigial fields** `Sset, Tset, A0S, A0T, tauS, tauT` carry honest placeholders (`∅`, `0`).
These are *not* consumed on the FT critical path: the §13/§16 contradiction in
`Peterfalvi.S16` (`S16_NonExistenceG`) is routed entirely through `eta = τ₃ ∘ ω` (the W-side
Dade grid), never through the S/T-side maximal-coherent isometries `τ_S, τ_T`.  The only
references to `tauS`/`tauT` are the *uncited* coherence-wiring lemmas in `S15_SAndT_Setup`,
which lie off the FT path.  `Hypothesis` itself places no `Prop`
constraint on these six fields, so the placeholders introduce no unsound dependency — they are
genuine values of the right type for fields the formalized contradiction does not read.  (User
decision 2026-06-24, issue 1004: close the producer on the verified-vestigial finding rather
than build the off-path §7 maximal-coherent Dade theory.) -/
noncomputable def section16CharacterData_of_isMinimalSimpleOdd {G : Type*} [Group G] [Finite G]
    (hG : IsMinimalSimpleOdd G) (mp : Section16MaximalPair G) (tp : Section16TypePStructure mp) :
    Section16CharacterData mp tp := by
  -- The grid building blocks carry `[NeZero |certainType{S,T}.W₁|]` (the prime base-index
  -- normalization); discharge both from `|certainTypeS.W₁| = tp.q`, `|certainTypeT.W₁| = tp.p`.
  haveI : NeZero (Nat.card ↥(mp.certainTypeS hG).W1) :=
    ⟨by rw [Section16CharacterData.cardCertainTypeS_W1 hG mp tp]; exact tp.q_prime.pos.ne'⟩
  haveI : NeZero (Nat.card ↥(mp.certainTypeT hG).W1) :=
    ⟨by rw [Section16CharacterData.cardCertainTypeT_W1 hG mp tp]; exact tp.p_prime.pos.ne'⟩
  exact
    { Sset := ∅
      Tset := ∅
      A0S := ∅
      A0T := ∅
      tauS := 0
      tauT := 0
      omega := Section16CharacterData.omegaS hG mp tp
      mu := Section16CharacterData.muS hG mp tp
      nu := Section16CharacterData.nuT hG mp tp
      delta := Section16CharacterData.deltaS hG mp tp
      deltaPrime := Section16CharacterData.deltaPrimeT hG mp tp
      delta_pm_one :=
        ⟨fun j => ((mp.certainTypeS hG).columnFamily
            (Section16CharacterData.chi2enum hG mp tp j)).sign_eq,
         fun i => ((mp.certainTypeT hG).columnFamily
            (Section16CharacterData.colT hG mp tp i)).sign_eq⟩
      mu_degree_modEq_delta := fun i j => by
        haveI : NeZero (Nat.card ↥(mp.certainTypeS hG).W1) :=
          ⟨by rw [Section16CharacterData.cardCertainTypeS_W1 hG mp tp]; exact tp.q_prime.pos.ne'⟩
        obtain ⟨a, ha⟩ := (mp.certainTypeS hG).certainType_degree_modEq
          (Section16CharacterData.chi2enum hG mp tp j) (Section16CharacterData.eqQ hG mp tp i)
        refine ⟨a, ?_⟩
        have hq : (tp.q : ℂ) = (Nat.card ↥(mp.certainTypeS hG).W1 : ℂ) := by
          rw [Section16CharacterData.cardCertainTypeS_W1 hG mp tp]
        simp only [Section16CharacterData.muS, Section16CharacterData.deltaS, hq]
        exact ha
      delta_zero_eq_one := by
        haveI : NeZero (Nat.card ↥(mp.certainTypeS hG).W1) :=
          ⟨by rw [Section16CharacterData.cardCertainTypeS_W1 hG mp tp]; exact tp.q_prime.pos.ne'⟩
        change Section16CharacterData.deltaS hG mp tp ⟨0, tp.p_prime.pos⟩ = 1
        rw [Section16CharacterData.deltaS, Section16CharacterData.chi2enum_zero]
        exact ((mp.certainTypeS hG).certainType_zero_column_anchor).1
      tau3 := Section16CharacterData.tau3W hG mp tp
      mu_definition := Section16CharacterData.muS_definition hG mp tp
      mu_irreducible := fun i j =>
        (((mp.certainTypeS hG).columnFamily (Section16CharacterData.chi2enum hG mp tp j)).mu
          (Section16CharacterData.eqQ hG mp tp i)).isIrreducible
      mu_col_injective := fun j i i' h =>
        (Section16CharacterData.eqQ hG mp tp).injective
          ((((mp.certainTypeS hG).columnFamily
            (Section16CharacterData.chi2enum hG mp tp j)).injective)
            (OddOrder.RepresentationTheory.IrreducibleCharacter.ext h))
      mu_orthonormal := Section16CharacterData.muS_orthonormal hG mp tp
      mu_diff_support := fun i {j k} hj0 hk0 hdeg =>
        Section16CharacterData.muS_diff_support hG mp tp i hj0 hk0 hdeg
      mu_apply_of_not_mem_W2 := fun i j w hwW hwS hw2 =>
        Section16CharacterData.muS_apply_of_not_mem_W2 hG mp tp i j w hwW hwS hw2
      mu_conj := Section16CharacterData.muS_conj hG mp tp
      tau3_omega_conj := Section16CharacterData.tau3W_omegaS_conj hG mp tp
      mu_colSum_eq_induce := fun j => by
        refine ⟨ClassFunction.restrict ((derivedInG mp.S).subgroupOf mp.S)
            (((mp.certainTypeS hG).columnFamily
              (Section16CharacterData.chi2enum hG mp tp j)).mu 0 : ClassFunction ↥mp.S ℂ),
          ?_, ?_, ?_⟩
        · exact (mp.certainTypeS hG).certainTypeRestrict_isIrreducible _
        · calc (∑ i : Fin tp.q, Section16CharacterData.muS hG mp tp i j)
              = ∑ i' : Fin (Nat.card ↥(mp.certainTypeS hG).W1),
                  (((mp.certainTypeS hG).columnFamily
                    (Section16CharacterData.chi2enum hG mp tp j)).mu i' :
                    ClassFunction ↥mp.S ℂ) := by
                simp only [Section16CharacterData.muS]
                exact Equiv.sum_comp (Section16CharacterData.eqQ hG mp tp)
                  (fun i' => (((mp.certainTypeS hG).columnFamily
                    (Section16CharacterData.chi2enum hG mp tp j)).mu i' :
                    ClassFunction ↥mp.S ℂ))
            _ = _ := ((mp.certainTypeS hG).induce_restrict_certainType_eq _).symm
        · intro hjne hsub
          have hχ₂ne : Section16CharacterData.chi2enum hG mp tp j ≠ 1 := by
            rw [← Section16CharacterData.chi2enum_zero hG mp tp]
            exact fun h => hjne ((Section16CharacterData.chi2enum hG mp tp).injective h)
          refine (mp.certainTypeS hG).not_subset_characterKernel_chiRestrict_of_ne_one
            hχ₂ne ?_
          have hseq : ((tp.W2.subgroupOf mp.S).subgroupOf
                ((derivedInG mp.S).subgroupOf mp.S))
              = (((mp.certainTypeS hG).W2).subgroupOf
                ((derivedInG mp.S).subgroupOf mp.S)) := by
            rw [Section16CharacterData.certainTypeS_W2_eq hG mp, tp.W2_eq_Kstar hG]
          exact hseq ▸ hsub
      mu_reducible_dichotomy := Section16CharacterData.muS_reducible_dichotomy hG mp tp
      nu_definition := Section16CharacterData.nuT_definition hG mp tp
      nu_irreducible := Section16CharacterData.nuT_irreducible hG mp tp
      nu_row_injective := Section16CharacterData.nuT_row_injective hG mp tp
      nu_orthonormal := Section16CharacterData.nuT_orthonormal hG mp tp
      nu_degree_modEq_deltaPrime :=
        Section16CharacterData.nuT_degree_modEq_deltaPrime hG mp tp
      deltaPrime_zero_eq_one := Section16CharacterData.deltaPrimeT_zero_eq_one hG mp tp
      nu_rowSum_eq_induce := Section16CharacterData.nuT_rowSum_eq_induce hG mp tp
      nu_reducible_dichotomy := Section16CharacterData.nuT_reducible_dichotomy hG mp tp
      nu_diff_support := Section16CharacterData.nuT_diff_support hG mp tp
      nu_apply_of_not_mem_W1 := Section16CharacterData.nuT_apply_of_not_mem_W1 hG mp tp
      nu_conj := Section16CharacterData.nuT_conj hG mp tp
      tau3_isometry := Section16CharacterData.tau3W_isometry hG mp tp
      tau3_trivial := Section16CharacterData.tau3W_trivial hG mp tp
      tau3_apply_of_regular := fun α w hwW hnot =>
        Section16CharacterData.tau3W_apply_of_regular hG mp tp α w hwW hnot
      tau3_mem_ZIrr := fun _ hz => Section16CharacterData.tau3W_mem_ZIrr hG mp tp hz
      omega_orthonormal := Section16CharacterData.omegaS_inner hG mp tp
      omega_apply_one := Section16CharacterData.omegaS_apply_one hG mp tp
      omega_mem_ZIrr := Section16CharacterData.omegaS_mem_ZIrr hG mp tp
      omega_mul := Section16CharacterData.omegaS_mul hG mp tp
      omega_col_zero_apply_of_mem_W2 :=
        Section16CharacterData.omegaS_col_zero_apply_of_mem_W2 hG mp tp
      omega_row_zero_apply_of_mem_W1 :=
        Section16CharacterData.omegaS_row_zero_apply_of_mem_W1 hG mp tp
      omega_pow_q_of_mem_W1 := Section16CharacterData.omegaS_pow_q_of_mem_W1 hG mp tp
      omega_pow_p_of_mem_W2 := Section16CharacterData.omegaS_pow_p_of_mem_W2 hG mp tp
      eta_complete_vanish := fun χ horth w hwW hnot =>
        Section16CharacterData.tau3W_omegaS_complete_vanish hG mp tp χ horth hwW hnot
      eta_fourcorner_vanish := fun i j hi hj x hx =>
        Section16CharacterData.tau3W_omegaS_fourcorner_vanish hG mp tp i j hi hj (by
          intro hmem
          obtain ⟨a, ha, hconj⟩ := Group.mem_conjugatesOfSet_iff.mp hmem
          obtain ⟨c, hc⟩ := isConj_iff.mp hconj
          exact hx (OddOrder.GroupTheory.mem_conjClassSet.mpr ⟨a, ha, c, hc⟩))
      eta_row_vanish_of_one_zero := fun x h0 i hi =>
        Section16CharacterData.tau3W_omegaS_row_vanish_of_one_zero hG mp tp h0 i hi
      eta_row_galois_orbit :=
        Section16CharacterData.tau3W_omegaS_row_galois_orbit hG mp tp
      eta_column_galois_orbit :=
        Section16CharacterData.tau3W_omegaS_column_galois_orbit hG mp tp
      eta_intCast_of_coprime := fun g hg i j =>
        Section16CharacterData.tau3W_omegaS_intCast_of_coprime hG mp tp i j hg
      eta_pair_of_coprime := fun g hg i j =>
        Section16CharacterData.tau3W_omegaS_pair_of_coprime hG mp tp i j hg
      eta_principal_of_coprime := fun g hg =>
        Section16CharacterData.tau3W_omegaS_principal_of_coprime hG mp tp hg }

/-- **Assembly of `Section16Inputs` from the three lane producers** (`sorry`-free).
Each field of `Section16Inputs` is sourced from exactly one of `mp` / `tp` / `cd`;
the character fields unify because `mp.S, mp.T, tp.W, tp.q, tp.p` are the chosen
witnesses. -/
noncomputable def section16Inputs_of_isMinimalSimpleOdd {G : Type*} [Group G] [Finite G]
    (hG : IsMinimalSimpleOdd G) : Section16Inputs G :=
  let mp := section16MaximalPair_of_isMinimalSimpleOdd hG
  let tp := section16TypePStructure_of_isMinimalSimpleOdd hG
    (OddOrder.Peterfalvi.S12.no_typeV_maximal_unconditional hG) mp
  let cd := section16CharacterData_of_isMinimalSimpleOdd hG mp tp
  { S := mp.S
    T := mp.T
    W1 := tp.W1
    W2 := tp.W2
    W := tp.W
    U := tp.U
    V := tp.V
    S_maximal := mp.S_maximal
    T_maximal := mp.T_maximal
    S_ne_T := mp.S_ne_T
    S_nonI := mp.S_nonI
    T_nonI := mp.T_nonI
    one_typeII := mp.one_typeII
    theorem88_caseB := mp.theorem88_caseB
    W_eq_inter := tp.W_eq_inter
    W_eq_join := tp.W_eq_join
    W1_inf_W2_eq_bot := tp.W1_inf_W2_eq_bot
    W1_commutes_W2 := tp.W1_commutes_W2
    W_cyclic := tp.W_cyclic
    S_deriv_eq_PU := tp.S_deriv_eq_PU
    T_deriv_eq_QV := tp.T_deriv_eq_QV
    V_inf_Q_eq_bot := tp.V_inf_Q_eq_bot
    W2_isComplement_T_deriv := tp.W2_isComplement_T_deriv
    W1_normalizes_U := tp.W1_normalizes_U
    W2_normalizes_V := tp.W2_normalizes_V
    q := tp.q
    p := tp.p
    q_prime := tp.q_prime
    p_prime := tp.p_prime
    q_eq_card_W1 := tp.q_eq_card_W1
    p_eq_card_W2 := tp.p_eq_card_W2
    u := tp.u
    v := tp.v
    c := tp.c
    d := tp.d
    c_eq_card_C := tp.c_eq_card_C
    d_eq_card_D := tp.d_eq_card_D
    card_U_eq_uc := tp.card_U_eq_uc
    card_V_eq_vd := tp.card_V_eq_vd
    Sset := cd.Sset
    Tset := cd.Tset
    A0S := cd.A0S
    A0T := cd.A0T
    tauS := cd.tauS
    tauT := cd.tauT
    omega := cd.omega
    mu := cd.mu
    nu := cd.nu
    delta := cd.delta
    deltaPrime := cd.deltaPrime
    delta_pm_one := cd.delta_pm_one
    mu_degree_modEq_delta := cd.mu_degree_modEq_delta
    delta_zero_eq_one := cd.delta_zero_eq_one
    tau3 := cd.tau3
    mu_definition := cd.mu_definition
    mu_irreducible := cd.mu_irreducible
    mu_col_injective := cd.mu_col_injective
    mu_orthonormal := cd.mu_orthonormal
    mu_diff_support := cd.mu_diff_support
    mu_apply_of_not_mem_W2 := cd.mu_apply_of_not_mem_W2
    mu_conj := cd.mu_conj
    tau3_omega_conj := cd.tau3_omega_conj
    mu_colSum_eq_induce := cd.mu_colSum_eq_induce
    mu_reducible_dichotomy := cd.mu_reducible_dichotomy
    nu_definition := cd.nu_definition
    nu_irreducible := cd.nu_irreducible
    nu_row_injective := cd.nu_row_injective
    nu_orthonormal := cd.nu_orthonormal
    nu_degree_modEq_deltaPrime := cd.nu_degree_modEq_deltaPrime
    deltaPrime_zero_eq_one := cd.deltaPrime_zero_eq_one
    nu_rowSum_eq_induce := cd.nu_rowSum_eq_induce
    nu_reducible_dichotomy := cd.nu_reducible_dichotomy
    nu_diff_support := cd.nu_diff_support
    nu_apply_of_not_mem_W1 := cd.nu_apply_of_not_mem_W1
    nu_conj := cd.nu_conj
    q_lt_p := tp.q_lt_p
    Sdata := tp.Sdata
    Sdata_U_eq := tp.Sdata_U_eq
    Sdata_W1_eq := tp.Sdata_W1_eq
    S_U_commutative := tp.S_U_commutative
    Sdata_W2_eq := tp.Sdata_W2_eq
    tau3_isometry := cd.tau3_isometry
    tau3_trivial := cd.tau3_trivial
    tau3_apply_of_regular := cd.tau3_apply_of_regular
    tau3_mem_ZIrr := cd.tau3_mem_ZIrr
    omega_orthonormal := cd.omega_orthonormal
    omega_apply_one := cd.omega_apply_one
    omega_mem_ZIrr := cd.omega_mem_ZIrr
    omega_mul := cd.omega_mul
    omega_col_zero_apply_of_mem_W2 := cd.omega_col_zero_apply_of_mem_W2
    omega_row_zero_apply_of_mem_W1 := cd.omega_row_zero_apply_of_mem_W1
    omega_pow_q_of_mem_W1 := cd.omega_pow_q_of_mem_W1
    omega_pow_p_of_mem_W2 := cd.omega_pow_p_of_mem_W2
    eta_complete_vanish := cd.eta_complete_vanish
    eta_fourcorner_vanish := cd.eta_fourcorner_vanish
    eta_row_vanish_of_one_zero := cd.eta_row_vanish_of_one_zero
    eta_row_galois_orbit := cd.eta_row_galois_orbit
    eta_column_galois_orbit := cd.eta_column_galois_orbit
    eta_intCast_of_coprime := cd.eta_intCast_of_coprime
    eta_pair_of_coprime := cd.eta_pair_of_coprime
    eta_principal_of_coprime := cd.eta_principal_of_coprime }

/-- **Assembly of the Section 16 configuration from named inputs** (`sorry`-free).

Given the `Section16Inputs` witnesses, this builds `Peterfalvi.S16.Hypothesis`
without any `sorry`.  Beyond carrying the input fields, it *derives* the fields of
`Peterfalvi.S15.Hypothesis` that are not independent data:

* `finiteG` from the ambient `[Finite G]`;
* the Fitting kernels `P := F(S)`, `Q := F(T)` (`maxNilpotentNormalHall`) and the
  centralizer complements `C := U ∩ C_G(P)`, `D := V ∩ C_G(Q)` definitionally, so
  `P_eq_SF`, `Q_eq_TF`, `C_eq`, `D_eq` are `rfl` — they are determined by
  `S, T, U, V`, not separate data;
* `q_odd`, `p_odd` from `Odd |G|` (subgroup orders divide `|G|`);
* `eta := τ₃ ∘ ω`, discharging **Peterfalvi (13.1.d)** `η_{ij} = ω_{ij}^{τ₃}`
  definitionally — `η` is the τ₃-image of the `ω`-grid, not separate data;
* `m` as the **(13.10)/(13.11)** rational formula in `p, q`, with `m_eq` by `rfl`.

These derivations are why `Section16Inputs` is a *strictly smaller* obligation
than `Peterfalvi.S16.Hypothesis`: discharging the menu does not require separately
producing `P, Q, C, D`, `η`, `m`, or the oddness facts. -/
noncomputable def sectionSixteenHypothesis_of_inputs {G : Type*} [Group G] [Finite G]
    (hodd : Odd (Nat.card G)) (inp : Section16Inputs G) :
    Peterfalvi.S16.Hypothesis (G := G) where
  base :=
    { S := inp.S
      T := inp.T
      W1 := inp.W1
      W2 := inp.W2
      W := inp.W
      P := maxNilpotentNormalHall inp.S
      Q := maxNilpotentNormalHall inp.T
      U := inp.U
      V := inp.V
      C := inp.U ⊓ Subgroup.centralizer (maxNilpotentNormalHall inp.S : Set G)
      D := inp.V ⊓ Subgroup.centralizer (maxNilpotentNormalHall inp.T : Set G)
      S_maximal := inp.S_maximal
      T_maximal := inp.T_maximal
      S_ne_T := inp.S_ne_T
      S_nonI := inp.S_nonI
      T_nonI := inp.T_nonI
      one_typeII := inp.one_typeII
      theorem88_caseB := inp.theorem88_caseB
      W_eq_inter := inp.W_eq_inter
      W_eq_join := inp.W_eq_join
      W1_inf_W2_eq_bot := inp.W1_inf_W2_eq_bot
      W1_commutes_W2 := inp.W1_commutes_W2
      W_cyclic := inp.W_cyclic
      P_eq_SF := rfl
      Q_eq_TF := rfl
      S_deriv_eq_PU := inp.S_deriv_eq_PU
      T_deriv_eq_QV := inp.T_deriv_eq_QV
      Q_inf_V_eq_bot := inp.V_inf_Q_eq_bot
      W2_isComplement_T_deriv := inp.W2_isComplement_T_deriv
      C_eq := rfl
      D_eq := rfl
      W1_normalizes_U := inp.W1_normalizes_U
      W2_normalizes_V := inp.W2_normalizes_V
      q := inp.q
      p := inp.p
      q_prime := inp.q_prime
      p_prime := inp.p_prime
      q_odd := by
        rw [inp.q_eq_card_W1]
        exact hodd.of_dvd_nat (Subgroup.card_subgroup_dvd_card inp.W1)
      p_odd := by
        rw [inp.p_eq_card_W2]
        exact hodd.of_dvd_nat (Subgroup.card_subgroup_dvd_card inp.W2)
      q_eq_card_W1 := inp.q_eq_card_W1
      p_eq_card_W2 := inp.p_eq_card_W2
      u := inp.u
      v := inp.v
      c := inp.c
      d := inp.d
      c_eq_card_C := inp.c_eq_card_C
      d_eq_card_D := inp.d_eq_card_D
      card_U_eq_uc := inp.card_U_eq_uc
      card_V_eq_vd := inp.card_V_eq_vd
      Sset := inp.Sset
      Tset := inp.Tset
      A0S := inp.A0S
      A0T := inp.A0T
      tauS := inp.tauS
      tauT := inp.tauT
      omega := inp.omega
      eta := fun i j => inp.tau3 (inp.omega i j)
      mu := inp.mu
      nu := inp.nu
      delta := inp.delta
      deltaPrime := inp.deltaPrime
      delta_pm_one := inp.delta_pm_one
      mu_degree_modEq_delta := inp.mu_degree_modEq_delta
      delta_zero_eq_one := inp.delta_zero_eq_one
      tau3 := inp.tau3
      eta_eq_tau_omega := fun _ _ => rfl
      mu_definition := inp.mu_definition
      mu_irreducible := inp.mu_irreducible
      mu_col_injective := inp.mu_col_injective
      mu_orthonormal := inp.mu_orthonormal
      mu_diff_support := inp.mu_diff_support
      mu_apply_of_not_mem_W2 := inp.mu_apply_of_not_mem_W2
      mu_conj := inp.mu_conj
      eta_conj := inp.tau3_omega_conj
      mu_colSum_eq_induce := inp.mu_colSum_eq_induce
      mu_reducible_dichotomy := inp.mu_reducible_dichotomy
      nu_definition := inp.nu_definition
      m := 1 - 1 / ((inp.q : ℚ) - 1) - ((inp.q : ℚ) - 1) / (inp.q : ℚ) ^ inp.p +
        1 / (((inp.q : ℚ) - 1) * (inp.q : ℚ) ^ inp.p)
      m_eq := rfl
      Sdata := inp.Sdata
      Sdata_U_eq := inp.Sdata_U_eq
      Sdata_W1_eq := inp.Sdata_W1_eq
      S_U_commutative := inp.S_U_commutative
      Sdata_W2_eq := inp.Sdata_W2_eq
      tau3_isometry := inp.tau3_isometry
      tau3_trivial := inp.tau3_trivial
      tau3_apply_of_regular := inp.tau3_apply_of_regular
      tau3_mem_ZIrr := inp.tau3_mem_ZIrr
      omega_orthonormal := inp.omega_orthonormal
      omega_apply_one := inp.omega_apply_one
      omega_mem_ZIrr := inp.omega_mem_ZIrr
      omega_mul := inp.omega_mul
      omega_col_zero_apply_of_mem_W2 := inp.omega_col_zero_apply_of_mem_W2
      omega_row_zero_apply_of_mem_W1 := inp.omega_row_zero_apply_of_mem_W1
      omega_pow_q_of_mem_W1 := inp.omega_pow_q_of_mem_W1
      omega_pow_p_of_mem_W2 := inp.omega_pow_p_of_mem_W2
      eta_complete_vanish := inp.eta_complete_vanish
      eta_fourcorner_vanish := inp.eta_fourcorner_vanish
      eta_row_vanish_of_one_zero := inp.eta_row_vanish_of_one_zero
      eta_row_galois_orbit := inp.eta_row_galois_orbit
      eta_column_galois_orbit := inp.eta_column_galois_orbit
      eta_intCast_of_coprime := inp.eta_intCast_of_coprime
      eta_pair_of_coprime := inp.eta_pair_of_coprime
      eta_principal_of_coprime := inp.eta_principal_of_coprime }
  nuGridSupply :=
    { nu_irreducible := inp.nu_irreducible
      nu_row_injective := inp.nu_row_injective
      nu_orthonormal := inp.nu_orthonormal
      nu_degree_modEq_deltaPrime := inp.nu_degree_modEq_deltaPrime
      deltaPrime_zero_eq_one := inp.deltaPrime_zero_eq_one
      nu_rowSum_eq_induce := inp.nu_rowSum_eq_induce
      nu_reducible_dichotomy := inp.nu_reducible_dichotomy
      nu_diff_support := inp.nu_diff_support
      nu_apply_of_not_mem_W1 := inp.nu_apply_of_not_mem_W1
      nu_conj := inp.nu_conj }
  q_lt_p := inp.q_lt_p

/-- **Canonical pure ν-grid supply from named Section 16 inputs** (issue 1030).

The T-side Peterfalvi (4.3)--(4.9) facts are explicit fields of `Section16Inputs`.
Consequently they assemble into the pure `NuGridSupplyData` package at the same
axiom-clean boundary as `sectionSixteenHypothesis_of_inputs`; no generic row-translation
principle and no post-(14.9) commutativity fact is used. -/
theorem sectionSixteenNuGridSupplyData_of_inputs
    {G : Type*} [Group G] [Finite G] (hodd : Odd (Nat.card G))
    (inp : Section16Inputs G) :
    Peterfalvi.S15.NuGridSupplyData (sectionSixteenHypothesis_of_inputs hodd inp).base := by
  exact (sectionSixteenHypothesis_of_inputs hodd inp).nuGridSupply

/-- **Canonical Section 16 configuration from a minimal simple odd-order group.**
The named Bender–Glauberman and Peterfalvi producers construct
`Section16Inputs G`, and the axiom-clean `sectionSixteenHypothesis_of_inputs`
assembles those inputs into the field-normalizer configuration of Peterfalvi (14.2).

Axiom audit (2026-07-15): this definition and
`section16Inputs_of_isMinimalSimpleOdd` depend only on `propext`,
`Classical.choice`, and `Quot.sound`.  In particular, the former gated input-menu
obligation is no longer the FT frontier.

The downstream `noMinimalSimpleOdd_of_section16` bridge, BG Appendix C final contradiction,
and `feitThompson` have now been audited against the same standard-three-axiom boundary. -/
noncomputable def sectionSixteenHypothesis_of_isMinimalSimpleOdd
    {G : Type*} [Group G] [Finite G] (hG : IsMinimalSimpleOdd G) :
    Peterfalvi.S16.Hypothesis (G := G) :=
  sectionSixteenHypothesis_of_inputs hG.odd (section16Inputs_of_isMinimalSimpleOdd hG)

end

/-- **No minimal simple group of odd order exists.** Combining the upstream
construction of the Section 16 configuration
(`sectionSixteenHypothesis_of_isMinimalSimpleOdd`) with the already-formalized
final contradiction (`noMinimalSimpleOdd_of_section16`). -/
theorem noMinimalSimpleOdd {G : Type*} [Group G] [Finite G]
    (hG : IsMinimalSimpleOdd G) : False :=
  noMinimalSimpleOdd_of_section16 hG
    (OddOrder.Peterfalvi.S12.no_typeV_maximal_unconditional hG)
    (fun s13 => OddOrder.Peterfalvi.S13.S_H0C_not_coherent_unconditional hG s13)
    (sectionSixteenHypothesis_of_isMinimalSimpleOdd hG)

/-! ## The minimal-counterexample reduction -/

/-- **Minimal-counterexample reduction** (pure group theory, `sorry`-free).

If no minimal simple group of odd order exists, then every finite group of odd
order is solvable.

The proof is strong induction on `Nat.card G`. If `G` were a non-solvable group of
odd order, then — using the induction hypothesis on its (smaller, odd-order) proper
subgroups and proper quotients — every proper subgroup is solvable and `G` is
simple: a proper nontrivial normal subgroup `N` would make `G` an extension of the
solvable group `N` by the solvable group `G ⧸ N`, hence solvable
(`solvable_of_ker_le_range`). Thus `G` would be a minimal simple group of odd
order, contradicting the hypothesis `hno`. -/
theorem feitThompson_of_noMinimalSimpleOdd
    (hno : ∀ (H : Type u) [Group H] [Finite H], IsMinimalSimpleOdd H → False)
    {G : Type u} [Group G] [Finite G] (hodd : Odd (Nat.card G)) :
    IsSolvable G := by
  -- Strong induction on the order, generalized over all groups in this universe.
  suffices key : ∀ (n : ℕ) (K : Type u) [Group K] [Finite K],
      Nat.card K = n → Odd (Nat.card K) → IsSolvable K from key (Nat.card G) G rfl hodd
  intro n
  induction n using Nat.strong_induction_on with
  | _ n ih =>
    intro K _ _ hcard hodd'
    subst hcard
    by_contra hns
    -- `K` is nontrivial: a subsingleton group is solvable.
    have hNT : Nontrivial K := by
      by_contra hc
      rw [not_nontrivial_iff_subsingleton] at hc
      haveI := hc
      exact hns inferInstance
    -- `K` is simple: a proper nontrivial normal subgroup splits `K` as a solvable
    -- extension of a solvable group, making `K` solvable.
    have hsimple : IsSimpleGroup K := by
      refine { toNontrivial := hNT, eq_bot_or_eq_top_of_normal := fun N hN => ?_ }
      by_contra hcon
      rw [not_or] at hcon
      obtain ⟨hNbot, hNtop⟩ := hcon
      -- `N` is solvable (proper subgroup of odd order, induction hypothesis).
      have hN_odd : Odd (Nat.card ↥N) :=
        hodd'.of_dvd_nat (Subgroup.card_subgroup_dvd_card N)
      have hNlt : Nat.card ↥N < Nat.card K := by
        have hidx : 1 < N.index := Subgroup.one_lt_index_of_ne_top hNtop
        have h := lt_mul_of_one_lt_right (Nat.card_pos (α := ↥N)) hidx
        rwa [Subgroup.card_mul_index] at h
      haveI : IsSolvable ↥N := ih (Nat.card ↥N) hNlt ↥N rfl hN_odd
      -- `K ⧸ N` is solvable (proper quotient of odd order, induction hypothesis).
      have hQ_odd : Odd (Nat.card (K ⧸ N)) :=
        hodd'.of_dvd_nat (Subgroup.card_quotient_dvd_card N)
      have hQlt : Nat.card (K ⧸ N) < Nat.card K := by
        have hN1 : 1 < Nat.card ↥N :=
          Finite.one_lt_card_iff_nontrivial.mpr ((Subgroup.nontrivial_iff_ne_bot N).mpr hNbot)
        have h := lt_mul_of_one_lt_right (Nat.card_pos (α := K ⧸ N)) hN1
        rwa [← Subgroup.card_eq_card_quotient_mul_card_subgroup] at h
      haveI : IsSolvable (K ⧸ N) := ih (Nat.card (K ⧸ N)) hQlt (K ⧸ N) rfl hQ_odd
      -- Extension of a solvable group by a solvable group is solvable.
      have hfg : (QuotientGroup.mk' N).ker ≤ (N.subtype).range :=
        le_of_eq ((QuotientGroup.ker_mk' N).trans (Subgroup.subtype_range N).symm)
      exact hns (solvable_of_ker_le_range N.subtype (QuotientGroup.mk' N) hfg)
    -- Every proper subgroup is solvable (smaller, odd order, induction hypothesis).
    have hproper : ∀ M : Subgroup K, M < ⊤ → IsSolvable ↥M := by
      intro M hM
      have hM_odd : Odd (Nat.card ↥M) :=
        hodd'.of_dvd_nat (Subgroup.card_subgroup_dvd_card M)
      have hMlt : Nat.card ↥M < Nat.card K := by
        have hidx : 1 < M.index := Subgroup.one_lt_index_of_ne_top (ne_of_lt hM)
        have h := lt_mul_of_one_lt_right (Nat.card_pos (α := ↥M)) hidx
        rwa [Subgroup.card_mul_index] at h
      exact ih (Nat.card ↥M) hMlt ↥M rfl hM_odd
    -- `K` is then a minimal simple group of odd order — impossible.
    exact hno K ⟨hodd', hsimple, hns, hproper⟩

/-! ## The Feit–Thompson theorem -/

/-- **Feit-Thompson theorem**: every finite group of odd order is solvable.

This combines the `sorry`-free minimal-counterexample reduction
(`feitThompson_of_noMinimalSimpleOdd`) with the non-existence of a minimal simple
group of odd order (`noMinimalSimpleOdd`).  The complete theorem is axiom-clean:
`#print axioms` reports only `propext`, `Classical.choice`, and `Quot.sound`. -/
theorem feitThompson {G : Type*} [Group G] [Finite G]
    (hodd : Odd (Nat.card G)) :
    IsSolvable G :=
  feitThompson_of_noMinimalSimpleOdd (fun _ _ _ hG => noMinimalSimpleOdd hG) hodd

end OddOrder
