stylistic change of headers

Author: SuvirRathore

README.md

@@ -16,7 +16,7 @@ I audited the statements against Mathlib v4.28.0
 source and the citations against the primary literature. AUDIT.md records the Mathlib
 survey, the errors corrected, and the claims that remain unverified.
 
-## The slice
+## The Slice
 
 Fix a finite field `𝔽_q` of characteristic `p`; a function field `K` over `𝔽_q`
 with algebraic closure `K̄` and absolute Galois group `G_K = Gal(K̄/K)`, carrying
@@ -91,7 +91,7 @@ At `λ₀` one may take `M = E_{λ₀}` and `ρ = ρ₀`, so `ρ₀` is itself o
 companions. No clause asserting this is needed or stated, since once the
 coefficient field varies an equality `ρ_{λ₀} = ρ₀` is type-inappropriate.
 
-## What is proved
+## What is Proved
 
 `charpoly_eq_of_isConj_gl` and `charpoly_eq_of_isConj`: the characteristic
 polynomial of `ρ(g)` depends only on the conjugacy class of `g`. This is not the
@@ -119,7 +119,7 @@ obstructs defining arithmetic Frobenius at the infinite level, since
 `IsArithFrobAt` is stated for monoid actions and needs no finiteness. Existence
 of Frobenius elements is a separate matter, treated under Limitations.
 
-## Absolute irreducibility without algebraic closures
+## Absolute Irreducibility Without Algebraic Closures
 
 Both the hypothesis on `ρ₀` and the conclusion about the companion need absolute
 irreducibility. Formalising that naively means constructing an algebraic closure
@@ -191,9 +191,9 @@ The slice is stated via `G_K` with an unramified-outside-`S` condition rather
 than via `π₁^ét(X ∖ S)`, because no `π₁^ét(X)` is available in Mathlib v4.28.0.
 AUDIT.md records what the library has here and what is missing.
 
-## Why the unramifiedness hypothesis is not redundant
+## A note on the Unramifiedness Hypothesis
 
-It is tempting to drop it. Continuity forces the image into a compact subgroup of
+It is tempting to drop it but continuity forces the image into a compact subgroup of
 `GL_n(E_λ)`, which stabilises a lattice, so the representation modulo each power
 of the maximal ideal factors through a finite extension ramified at finitely many
 places. That gives a finite ramification set at every finite level, but the
@@ -242,7 +242,7 @@ theorems additionally `sorryAx`), and counts the source lines
 consisting of `sorry`, requiring exactly one. AUDIT.md records what each check establishes and what it
 misses.
 
-## Next steps
+## Next Steps
 
 The most self-contained is existence of Frobenius elements in the absolute Galois
 group, which is missing from Mathlib. Beyond