VII AND VIII PAGE BRIEF (root of the sakellaridis-char-p run → page writer for Propositions VII and VIII)

Propositions VII (props/e6-f4-module.html) and VIII (props/e6-f4.html) of the satake-two-levels workspace in /Users/miltonlin/Projects/Trees/subpages/tools/solve-maths/satake-two-levels/ were written while Sakellaridis's Theorem 8.0.2 was known for E6/F4 only conditionally: over p-adic fields, modulo "(I) Axiom 2.2.1 over O", and not at all over F_q((t)). A /solve-maths run (sakellaridis-char-p) has now settled both, with audits. Update the two pages so that they state the new status everywhere, consistently with Proposition VI (another writer is rewriting props/sakellaridis.html in parallel; do not touch it).

WHAT THE RUN ESTABLISHED (all audited; link the run's node pages ../../sakellaridis-char-p/nodes/<id>.html from props/):
1. (A3a) — the new label of Sakellaridis's Axiom 2.2.1 (rank-one models over O, with his scheme structure and the complement clause) — holds for the model M_θ over every discrete valuation ring with 2 invertible, mixed and equal characteristic, p = 3 included (A2-8; audit A6-9). The 45 Borel orbits B ẇ x0 are all the orbits, all of maximal rank; YP_α/R(P_α) ≅ PGL2\PGL2 (90 pairs) or B2\PGL2 = P^1_O (180 pairs).
2. So every hypothesis of Theorem 8.0.2 holds for M_θ over every p-adic F, p odd, any ramification (S4, S4b for the others; for ramified F the paper's normalizations are checked in A4-7, audit A5-5, and [Sa08] is stated for every characteristic-0 local field, root check R-3).
3. Over F = F_q((t)), p odd: the hypotheses (A1ₚ), (A2), (A3b), (A3c), (A4)(i),(ii),(iv), (A5) hold (A3-12; audit A5-13), and Theorem 8.0.2 holds for M_θ by transfer from the totally ramified fields Q_q(p^{1/e}) (close local fields: A4-2, A4-5, A4-6, A4-8; audits A5-1, A5-3, A5-4, A5-6). The isomorphism C_K ≅ S with φ0 ↦ 1 is unique, and the image of 1_{Kx_κ} is the same polynomial P_κ as over p-adic fields (it depends only on q). The Cartan decomposition K\X(F_q((t))) ≅ Λ_S^+ is proved twice (A3-8, A4-5).
4. Hence VII(b) holds unconditionally, over F_q((t)) and over every p-adic F, p odd: no single function generates C_K; C_K = H_Kφ0 ⊕ C·1_{O_{3ω1∨}}; C_K/H_Kφ0 is the character q^{ρ−ω4}. The second generator uses P_{3ω1∨}, which comes from the proof of Theorem 8.0.2 (p. 64) and is the same over F_q((t)) (A4-8, step 5).
5. Hence VIII's function half holds over F_q((t)): sheaves hold over F̄_q (unchanged, from D0–D2) and functions fail over F_q((t)) — the divergence is now on one field. The old "gap" paragraph of VIII (no comparison of C_K between p-adic and Laurent-series fields) is resolved by item 3.
6. Caveat to record in VIII, in one or two sentences next to D0: two agents of the run found independently, and the audit confirmed (A3-1, A4-3, A5-7), that Chen–Yi prove their Prop. 17(i) — the orbit parametrization behind D0 — by citing Gaitsgory–Nadler, Thm 8.2.9, and Nadler 2004, Thm 4.2, which are over C. For E6/F4 the function-level parametrization over F_q((t)) is now proved directly (A3-8, A4-5).

RELABELLING (as on the VI page): (A1) characteristic-0 field and group; (A1ₚ) the same with F = F_q((t)); (A2) integral model; (A3a) rank-one models over O = Axiom 2.2.1; (A3b) Cartan decomposition = Axiom 2.4.1; (A3c) Iwahori orbits = Axiom 2.4.2; (A4), (A5) unchanged. Links to definitions: sakellaridis.html#hyp-a1, #hyp-a1p, #hyp-a2, #hyp-a3a, #hyp-a3b, #hyp-a3c, #hyp-a4, #hyp-a5 (the VI writer creates these anchors). Replace "(I)" and "Axiom 2.2.1 over O" by "(A3a)" (first mention: "(A3a), rank-one models over 𝒪 (Sakellaridis's Axiom 2.2.1)"). On VII, the hypothesis "(I)" becomes a proved input with its status, and "(Sak)" can stay as a label for "Theorem 8.0.2 holds for M_θ at F", now proved for F_q((t)) and every p-adic F (cite Proposition VI and the run).

TITLES: VII becomes "VII · E6/F4: C_K needs two generators" (<title> and page head); state in the lead that (a) is algebra for every q and (b) holds over F_q((t)) and every p-adic field, p odd, by Proposition VI. VIII keeps its title; its lead says the function half now holds over F_q((t)), the same field family as the sheaf half's F̄_q.

FILES YOU OWN (edit only these): props/e6-f4-module.html, props/e6-f4.html, props/assets/e6-f4-module-graph.js, e6-f4-module-literature.js, e6-f4-module-glossary.js, e6-f4-module-sources.js, e6-f4-graph.js, e6-f4-literature.js, e6-f4-glossary.js, e6-f4-sources.js, props/sources/e6-f4-index.json, e6-f4-module-index.json and the files prepare_sources.py writes for these two slugs, props/pdf/e6-f4-module.tex/.pdf and e6-f4.tex/.pdf. Do not edit data.json, props/sakellaridis*, props/assets/glossary.js, style.css, any other page or any build script; leave the <nav class="site-nav">…</nav> blocks exactly as they are.

HOW: read the proof-concept-graph skill (/Users/miltonlin/Projects/Trees/.claude/skills/proof-concept-graph/SKILL.md, references/ui-design.md) for the page contract; keep each page's shell, panels and style. Update the G panel text (lead, hypotheses, proposition, steps, boxed summary, scope notes), the graph nodes whose status changes (open/conditional → proved; the "what remains open" node becomes a proved input node or is removed), the glossary entries that mention Axiom 2.2.1 or (I), and each PDF (update the .tex, compile with tectonic, delete cached draft-<slug>-*.png|txt, re-run `uv run --with pymupdf python3 props/assets/prepare_sources.py <slug>`). New statements cite the run's node pages; no new literature extract is required, but keep the existing ones valid.

STYLE: plain, short sentences; every symbol defined or recallable; statuses "proved · cited", "proved · this run, audited". VERIFY: KaTeX renders with no .katex-error (headless Chrome screenshots at desktop and phone width), the graph works, links resolve, the PDFs compile. Report back in under 250 words.

WORKING DISCIPLINE: keep each response short; prefer many small edits or python3 scripts over retyping whole files; never produce a single response longer than about 12,000 words, thinking included. Do not commit with git.