Deriving the Evens–Kahn formula (B9) from the relative Stiefel–Whitney identity (B9-A, N4/N5) #
This file supplies the engine behind the B9-A flip (plan docs/orchestration/b9a-proof-plan.md,
nodes N4/N5): since 2026-07-24, GQ2/Foundations/Axioms.lean proves the same-name theorem
evensKahn_dyadic — byte-identical to the pre-flip axiom — as
evensKahn_dyadic_of_rsw relativeStiefelWhitney_dyadic … (hilbertSymbol_normCriterion_finiteDyadic k htriv).
One declaration:
evensKahn_dyadic_of_rsw— the reusable engine. It takes the relative Stiefel–Whitney statement as an explicit hypothesishrsw(this file stays upstream of the axiom file, so it cannot name the B9 axiom) together with the B11a norm criterionhnorm, and proves the pre-flip B9 conclusion.
The hnorm hypothesis (owner-approved firewall, Q2) #
The engine carries hnorm, the dyadic Hilbert-symbol norm criterion — the exact conclusion of
axiom B11a, hilbertSymbol_normCriterion_finiteDyadic k htriv. It is forced: the degree-2
component evaluates swTwo on the diagonal transfer forms via swTwo_diag, whose Delzant
well-definedness (swTwo_well_defined, plan node N2) consumes the criterion. B11a lives
downstream in GQ2/Foundations/Axioms.lean, so it cannot be imported here; the firewall carries
it as a hypothesis (GQ2/StiefelWhitney.lean's swTwo_diag/swTwo_congr already do), and this
file inherits it one level up. The owner approved this design (Q2,
docs/orchestration/b9a-tickets.md). The degree-1 component needs no such input. At the flip
the hypothesis is discharged from B11a, so the flipped evensKahn_dyadic is byte-identical (no
hnorm) with #print axioms = {relativeStiefelWhitney_dyadic,
hilbertSymbol_normCriterion_finiteDyadic, + std-3} (plan node N2).
No unit-arithmetic bridge is needed #
T1 pinned the diagonalization weights of traceFormOne_isDiagonalization (⟨2, 2d⟩) and
traceFormTwisted_isDiagonalization (⟨2u, 2dn/u⟩ = ⟨twoUnit k*u, twoUnit k*d*n*u⁻¹⟩) to the exact
B9 normal form, so swOne_diag/swTwo_diag land on the B9 kummerClassK arguments syntactically;
the two components close by rw with no (↥k)ˣ associativity/commutativity bridging.
Imports and axiom status #
Imports are strictly upstream of GQ2/Foundations/Axioms.lean (GQ2.TraceForm,
GQ2.StiefelWhitney and their closure supply the B9 vocabulary
kummerClassK/corH1/evensNormH2/twoUnit from GQ2.EvensKahn). This file has no
sorry and no axiom, and since the 2026-07-24 flip its dependencies are sorry-free too:
the Lemma 6.16 diagonalizations (GQ2/TraceForm.lean, T2) and the Delzant well-definedness
(GQ2/StiefelWhitney.lean, T3) are proved, so evensKahn_dyadic_of_rsw carries only the
standard three axioms — the B-axioms enter downstream, when Foundations/Axioms.lean
instantiates hrsw and hnorm.
Citations #
Kahn, Invent. Math. 78 (1984), Théorème 2; Evens, Trans. AMS 108 (1963), Thm 1; Kozlowski, Proc.
AMS 91 (1984), Thm 1.1; Serre, Local Fields [7], Ch. XIV §2 (B11a). Paper: §6, eq. (111),
Lemmas 6.13/6.16. Plan: docs/orchestration/b9a-proof-plan.md nodes N4/N5.
B9 from the relative Stiefel–Whitney identity hrsw, given the B11a norm criterion hnorm.
The reusable engine of this file. From the abstract identity hrsw (the exact statement of
relativeStiefelWhitney_dyadic, taken as a hypothesis so the file stays upstream of the axiom file)
and the norm criterion hnorm, it proves the byte-identical B9 conclusion at a = u + vδ.
Proof (plan node N5): the transfer unit a = u + vδ ∈ k(δ)ˣ is built as a nonzero element of the
field quadExt k δ (its image is β² ≠ 0); finrank_quadExt_eq_two gives [k(δ):k] = 2; hrsw
gives the two Stiefel–Whitney components; the Lemma 6.16 diagonalizations Tr⟨a⟩ ≃ ⟨2u, 2dn/u⟩ and
Tr⟨1⟩ ≃ ⟨2, 2d⟩, via swOne_diag/swTwo_diag, rewrite them into the B9 Kummer-class form.
GQ2/Foundations/Axioms.lean instantiates this at the B9 axiom
relativeStiefelWhitney_dyadic and hnorm := hilbertSymbol_normCriterion_finiteDyadic k htriv,
recovering the byte-identical B9 statement as the same-name theorem.