You are agent A2 in a bounded team attacking one mathematical question. Work independently; you will not see the other agents.

SETTING (Proposition VI of the satake-two-levels pages: Sakellaridis's theorem, restated for a local field of characteristic p).

Fields. p is an odd prime, q a power of p. F is a non-archimedean local field with ring of integers O, uniformizer ϖ, residue field F_q, |ϖ| = q^{-1}. Two cases that must never be confused:
  char F = 0 : F/Q_p finite ("p-adic"). Sakellaridis assumes F/Q_p unramified "to avoid complicated formulas", saying "the modifications needed to remove this assumption are trivial" (§1.1, p. 2).
  char F = p : F = F_q((t)), O = F_q[[t]], ϖ = t.
"p odd" is the residue characteristic in both cases; the characteristic of F is 0 or p.

Groups. G is a split reductive group scheme over O with connected fibres and simply connected derived group; B ⊇ A a Borel subgroup and a split maximal torus over O; U the unipotent radical of B; W the Weyl group; K = G(O); J the Iwahori subgroup (preimage of B(F_q)). H_K = C_c(K\G(F)/K), vol K = 1; the Satake isomorphism S : H_K ≅ C[A^*]^W, A^* the complex dual torus (unramified characters of A(F)).

Variety. Sakellaridis uses right actions and writes X = H\G; our pages use left actions, X = G/H (read x·g as g^{-1}x). X is a G-scheme over O with an open B_F-orbit X̊_F; X̊ := X \ closure(X \ X̊_F); x0 ∈ X̊(O), H its stabilizer.
Invariants (Sakellaridis §2.1–2.2, §6.1, §7.1, §8): P(X) = {p : X̊p = X̊}; L(X) a Levi of P(X) with [L(X),L(X)] ⊆ H; A_X = L(X)/(L(X)∩H); 𝒳(X) the B-eigencharacters of F(X)^(B); Λ_X = Hom(𝒳(X), Z); Λ_X^+ the monoid of G-invariant valuations, V its cone; A_X^+ ⊆ A_X(F) the points with label in Λ_X^+ (via Λ_X ≅ A_X(F)/A_X(O), λ ↦ e^λ(ϖ)); W_X the little Weyl group (Knop's action of W on the B_F̄-orbits of maximal rank is transitive, the stabilizer of X̊ is W(X) = W_X ⋉ W_{P(X)}); δ(X) = |d(X)|, d(X) the modular character of L(X)∩B; δ(X)^{1/2}A_X^* ⊆ A^* the translate of the image of A_X^* → A^*; Δ_X the normalized spherical roots; colours, virtual weighted colours, Θ, Θ^+.
Functions. C_K = C_c^∞(X(F))^K, a module over H_K by (f∗φ)(x) = Σ_{gK∈G(F)/K} f(g)φ(g^{-1}x); φ0 = 1_{X(O)}; (SG): H_K∗φ0 = C_K. The restriction map r : C[A^*]^W → S := C[δ(X)^{1/2}A_X^*]^{W_X} (Sakellaridis (8.2), p. 65).

HYPOTHESES, relabelled (page numbers of arXiv:0905.4244v3 = printed pages).
  (A1₀) char F = 0 (§1.1, p. 2).
  (A1ₚ) char F = p, i.e. F = F_q((t)). Not in the paper.
  (A1)  G split reductive over O, connected fibres, simply connected derived group (§1.7, p. 6).
  (A2)  Integral model (§1.7, p. 7): X is a quasi-affine G-scheme over O; X̊ is smooth and surjective over O and its special fibre is homogeneous under B_{F_q}; X has a G-eigenmeasure and X̊ a B-invariant measure.
  (A3a) Rank-one models over O (Sakellaridis's Axiom 2.2.1, p. 9): for every B_F-orbit Y_F ⊆ X_F of maximal rank and every simple root α, the O-scheme YP_α/R(P_α) is isomorphic to one of PGL2\PGL2, SU\PGL2 (S ⊆ N(U)), T\PGL2 (T a non-trivial torus over O) or N(T)\PGL2; and the complement of YP_α is the closure of the complement of (YP_α)_F. Here the O-scheme Y is "the complement of the closure of the complement of Y_F in its closure" (p. 9).
  (A3b) Cartan decomposition (Axiom 2.4.1, p. 10): A_X^+ contains a complete set of representatives of the K-orbits on X(F); elements of A_X^+ with distinct images in Λ_X^+ lie in distinct K-orbits.
  (A3c) Iwahori orbits (Axiom 2.4.2, p. 11): xJ ⊆ xB(O) for x ∈ A_X^+.
  (A4)  Spherical roots and colours, over F̄: (i) no pair (Y, α) of maximal rank is of type N, and δ(X)^{-1/2}χ̃ is unramified (opening of §6, p. 41); (ii) L_γ is a classical group for every γ ∈ Δ_X (§7, p. 58); (iii) Statement 6.3.1 (pp. 44–45), which follows from (i) and (ii) by Theorem 6.3.2 (p. 45); (iv) Statement 7.1.5 (p. 60).
  (A5)  X is homogeneous and affine, and X̊(F) is a single B(F)-orbit (§8, p. 63).

PUBLISHED, characteristic 0. Theorem 8.0.2 (p. 64): under (A1₀), (A1)–(A5) there is a canonical isomorphism C_K ≅ S, compatible with the H_K-structure and the Satake isomorphism (f acts on S as multiplication by r(S f)), with 1_{X(O)} ↦ 1. Corollary 8.0.4 (p. 65): if r is onto, C_K is a principal H_K-module generated by φ0. Hence, in characteristic 0, (SG) ⟺ r onto.

THE CASE E6/F4. G_Z the split simply connected Chevalley group of type E6, pinning (T, B, {x_{α_i}}), Bourbaki labels (chain 1–3–4–5–6, node 2 on node 4). θ0 = Int(σ_L)∘C, with C the Chevalley involution and σ_L the Tits lift of w_L, the longest element of W(D4) on nodes 2,3,4,5; θ0|_T = −w_L; type E IV; θ0 is an involution defined over Z (S4-11). The model M_θ: X_O := (G_Z/G_Z^{θ0}) ⊗ O with p odd; H_O = G_O^{θ0}, smooth with fibres of type F4; x0 = eH. Λ_X = Λ_S = Ze1 ⊕ Ze6 with e_i = (1−θ0)α_i^∨; W_X = S3; restricted roots A2, all multiplicities 8; P(X) the standard parabolic of nodes {2,3,4,5}, L = Z_G(S), S = (T^{−θ0})°; 45 Borel orbits of maximal rank (|W(E6)|/(|W_X|·|W(D4)|) = 51840/(6·192)).
Known for p-adic F (char 0), p odd (salvage returns S4, S4b): (A1), (A2), (A3b), (A3c), (A4), (A5) hold for M_θ, and the types in (A3a) over F̄ are only G and U; (A3a) as O-schemes is open. Proposition VII (proved, every q): r is not onto; so wherever Theorem 8.0.2 holds for M_θ, (SG) fails.

TEAM QUESTION.
 (Q1) Formulate and prove Sakellaridis's Theorem 8.0.2 over a local field of characteristic p: F = F_q((t)), p odd, for a symmetric X = G/G^θ (θ an involution of G over O) satisfying (A1)–(A5), every statement over F̄ read over an algebraic closure of F_q((t)). State exactly which further hypotheses, if any, the characteristic-p proof needs. At minimum: X = M_θ (E6/F4).
 (Q2) Prove (A3a) for M_θ over every complete discrete valuation ring O with odd residue characteristic, mixed (p-adic) and equal (F_q[[t]]) characteristic, or exhibit the pairs (Y, α) where it fails.
 (Q3) Verify (A1), (A2), (A3b), (A3c), (A4), (A5) for M_θ over F_q((t)), p odd, replacing every characteristic-0 citation.
A complete answer gives the characteristic-p theorem with its exact hypotheses and a proof in which every step is proved or cited with its number and checked to hold in characteristic p; (A3a) for M_θ over every O as above; and the hypotheses verified for M_θ over F_q((t)). Then, for E6/F4 over F_q((t)) and over p-adic F (p odd), (SG) ⟺ r onto, so (SG) fails.

DOES NOT COUNT. "The proof carries over verbatim" without checking each characteristic-0 input: Knop [Kn91, Kn94, Kn95, Kn96], Brion [Br01], Brion–Luna–Vust [BLV86], Luna [Lu01], Sakellaridis [Sa06, Sa08, Sa12], Braverman–Kazhdan [BK98], Casselman and Casselman–Shalika [Ca80, CS80], Wasserman [Was96], Akhiezer [Ak83], Tate's thesis in §5.3. A p-adic result presented as a characteristic-p result. (A3a) checked over F̄ only (the types), or only on one fibre, or "at almost every place", instead of as an isomorphism of O-schemes. A close-fields transfer that assumes Theorem 8.0.2 for ramified p-adic fields without checking Sakellaridis's normalizations (§3.8, §5.3). Numerical checks for small q only. A statement about E6/F4 over F_q((t)) obtained by citing Theorem 8.0.2 in characteristic 0.

CHECKLIST (the ways a wrong answer typically fails; audits check every one).
 1. Hypothesis transfer: a characteristic-0 theorem used in characteristic p.
 2. Residue characteristic confused with the characteristic of F.
 3. Generic fibre, special fibre and O-scheme confused; in particular Sakellaridis's scheme structure on Y.
 4. A type over F̄ taken for an isomorphism of O-schemes.
 5. Non-reduced stabilizers and inseparable orbit maps in characteristic p.
 6. Finiteness of B(F)-orbits and of Galois cohomology in characteristic p (H^1(F, μ_p) and Artin–Schreier classes are infinite).
 7. Normalizations: measures, the conductor of ψ, "unramified over Q_p".
 8. Left versus right actions; Λ_X^+ versus Λ_S^+; anti-dominant versus dominant labels.
 9. A statement "at almost every place" used at a given place.
 10. Circularity: the conclusion of Theorem 8.0.2 in characteristic p used to verify its hypotheses.
 11. Bad primes: p = 3 is bad for E6 and F4.

TERMINOLOGY TRAPS. The type of (Y, α) (G, U, T, N) is a statement over F̄; (A3a) is a statement about O-schemes. X(O) and Kx0 are different sets in general (equal for M_θ by Hensel and Lang). K-orbits, B(F)-orbits and B_F̄-orbits are different things. Λ_X^+ is the valuation monoid (for symmetric X the image of the anti-dominant chamber); our pages label K-orbits by dominant μ ∈ Λ_S^+ through t^μ x0. W_X for E6/F4 is S3. "Unramified over Q_p" is a simplification of the paper, not part of the characteristic-p question. "Symmetric" means H = G^θ (or an open subgroup of it) for an involution θ.

FILES (read HTML with  sed -e 's/<[^>]*>/ /g' FILE | tr -s ' \n'  and PDFs with  pdftotext -layout FILE - ).
 Sakellaridis, Spherical functions on spherical varieties, arXiv:0905.4244v3: /Users/miltonlin/Projects/Trees/subpages/tools/solve-maths/satake-two-levels/props/sources/sakellaridis-v3.pdf ; as text: /private/tmp/claude-501/-Users-miltonlin-Projects-Trees/75c2c3d9-ef06-4644-b59b-d12583740b0c/scratchpad/solve-vi/sak.txt (§2.2.1 near line 503, §3.3 near 720, Theorem 4.2.2 near 1410, §5.4 near 1823, §6.19 near 3388, Theorem 7.2.1 near 3631, §8 near 3830).
 Proposition VI page (hypotheses with their status, the E6/F4 verification): /Users/miltonlin/Projects/Trees/subpages/tools/solve-maths/satake-two-levels/props/sakellaridis.html
 Salvage returns S4, S4b (the p-adic verification for E6/F4; nodes S4-1 … S4-14): /Users/miltonlin/Projects/Trees/subpages/tools/solve-maths/satake-two-levels/audit/S4.json and S4b.json
 E6/F4 root data and the symmetric pair: /Users/miltonlin/Projects/Trees/subpages/tools/proof_graphs/spherical-generation/families/e6-f4.html ; Proposition VII: /Users/miltonlin/Projects/Trees/subpages/tools/solve-maths/satake-two-levels/props/e6-f4-module.html
 Other local sources: /Users/miltonlin/Projects/Trees/subpages/tools/solve-maths/satake-two-levels/props/sources/{conrad-reductive-group-schemes,milne-iag-v2,chen-yi-v4,zhu-satake-v2,bf-satake-v2,stacks-algebra,stacks-more-algebra}.pdf

RULES.
- Return concrete lemmas, constructions, computations or counterexamples, each with a proof or an explicit gap. No status reports, no optimism. Label every claim: proved (here, or cited with exact result number) · heuristic · gap. An analogue in one characteristic does not certify an inference in the other.
- Check the exact meaning of every term you use (see the traps above).
- Do not search the web for a solution of this question; ordinary mathematical background (statements and standing hypotheses of standard theorems and papers) may be looked up. Prefer the local sources. When you cite a paper you could not open, say so.
- You may run short Python checks with `python3 -I` (standard library only; no sympy or numpy) for finite computations: single process, a few seconds each, no parallelism. Keep scripts in /private/tmp/claude-501/-Users-miltonlin-Projects-Trees/75c2c3d9-ef06-4644-b59b-d12583740b0c/scratchpad/solve-vi/A2/ (create it). Do not modify anything under /Users/miltonlin/Projects/Trees.
- Timestamps: at the start of every node run `date -u +%Y-%m-%dT%H:%M:%SZ` and record it in the node. Work in nodes: an idea, a lemma with proof, a computation, a check, an objection, a dead end (status blocked, with the exact missing lemma), or a verdict. Produce 5–14 nodes.
- Write every node as a stage of a mathematics paper: a plain-words name, a one-sentence summary, the precise statement, and the argument as numbered steps, readable by a mathematician outside the subfield. Cite other nodes as [[A2-3]], never by bare code in prose; state computations as mathematics (what was computed, the result, why it suffices), not as code or program output.
- Concept keys for nodes: setup · transfer · integral · hypotheses · close · synthesis.
- FINAL ANSWER: only one JSON object inside a ```json fence, with the schema below; also write the identical JSON to /private/tmp/claude-501/-Users-miltonlin-Projects-Trees/75c2c3d9-ef06-4644-b59b-d12583740b0c/scratchpad/solve-vi/A2/return.json. Escape JSON strings properly (double every backslash, escape quotes and newlines). Nothing outside the fence.

RETURN SCHEMA
{"agent":"A2",
 "family":"approach family, at most twelve words",
 "nodes":[
  {"id":"A2-1","t":"2026-10-18T02:10:12Z",
   "kind":"idea|lemma|computation|check|objection|blocked|verdict",
   "status":"proved|refuted|blocked|open|heuristic|superseded",
   "label":"Setup|Definition|Strategy|Lemma|Proposition|Theorem|Corollary|Computation|Example|Counterexample|Remark|Objection|Audit|Conjecture|Dead end|Summary",
   "name":"tree label: at most 44 characters, plain text (Unicode, no TeX), says what the step establishes",
   "title":"page title, at most 90 characters, inline TeX allowed",
   "summary":"one or two sentences: what this step establishes and why it matters",
   "statement":"the precise claim (Markdown + TeX); empty for Strategy and Remark",
   "parents":["A2-0"],
   "body":"the argument: Markdown; math as \\( \\) inline and $$ $$ display; proofs as numbered steps; other nodes as [[A2-1]]; results cited with exact numbers and the file they come from",
   "concept":"one of: setup, transfer, integral, hypotheses, close, synthesis",
   "key":false,
   "sources":["sakellaridis-v3.pdf, Axiom 2.2.1, p. 9"]}],
 "result":{"status":"proved|partial|refuted|blocked",
           "statement":"precise statement of what was established",
           "gap":"exact remaining obligation, or none"},
 "blocked_routes":["route and the theorem-strength lemma it would need"],
 "scripts":["paths of scripts run"]}

YOUR TARGET. (Q2).
YOUR APPROACH FAMILY. Tits lifts and θ-twisted Borel orbits over Z[1/2]: prove (A3a) for M_θ once over Z[1/2] and base-change to every O with 2 ∈ O^×. Starting points:
1. Show that the Borel orbits of maximal rank of X over an algebraically closed field of characteristic ≠ 2 are the orbits B·ẇx0, with ẇ ∈ N_G(T)(Z) a Tits lift of w and w in a set of representatives of W/W_H(T), W_H(T) = N_H(T)/T^{θ0} ≅ W(F4); and that there are 45 of them in every characteristic ≠ 2.
2. Compute the stabilizer B_{ẇx0} = B ∩ ẇHẇ^{-1} = (B ∩ θ_w(B))^{θ_w}, θ_w := Int(ẇ)∘θ0∘Int(ẇ)^{-1}, in terms of roots (θ_w acts on roots by wθ0w^{-1}), and prove that it is a smooth group scheme over Z[1/2] whose fibre dimension does not depend on the fibre.
3. For each orbit Y and simple root α, determine the type of (Y, α) in every characteristic ≠ 2, the O-scheme YP_α/R(P_α), and an explicit isomorphism with the standard model over O.
4. Prove that the orbit map B/B_y → X_O is an immersion over O whose image is Sakellaridis's O-scheme Y (the complement of the closure of the complement of Y_F in its closure), including the complement clause of (A3a). Sakellaridis's remark on p. 9 (an inductive application of the axiom along type-U edges) may help.
5. Compute all 45 × 6 pairs with a script (the root system of E6 from its Cartan matrix, θ0 = −w_L on roots; the signs of θ0 on root groups only if a step needs them), and state the outcome as mathematics.