WIP: Remove blanket section exposure across Lean Pool

LeanPool/ABCExceptions.lean

@@ -23,7 +23,7 @@ Tags: number-theory, analytic-number-theory, abc-conjecture
 MSC: 11D75, 11N37
 -/
 
-@[expose] public section
+public section
 
 /-!
 ## Mathematical overview

LeanPool/ABCExceptions/ForMathlib.lean

@@ -16,4 +16,4 @@ Import-only index for Mathlib-adjacent support files used by the ABC exceptions
 development.
 -/
 
-@[expose] public section
+public section

LeanPool/ABCExceptions/ForMathlib/Misc.lean

@@ -18,7 +18,7 @@ import Mathlib.Data.Nat.SuccPred
 # LeanPool.ABCExceptions.ForMathlib.Misc
 -/
 
-@[expose] public section
+public section
 
 noncomputable section
 

LeanPool/ABCExceptions/ForMathlib/RingTheory.lean

@@ -15,4 +15,4 @@ Import-only index for ring-theoretic support files used by the ABC exceptions
 development.
 -/
 
-@[expose] public section
+public section

LeanPool/ABCExceptions/ForMathlib/RingTheory/Radical.lean

@@ -15,7 +15,7 @@ import Mathlib.RingTheory.Radical.NatInt
 # LeanPool.ABCExceptions.ForMathlib.RingTheory.Radical
 -/
 
-@[expose] public section
+public section
 
 namespace UniqueFactorizationMonoid
 

LeanPool/ABCExceptions/Section2.lean

@@ -21,7 +21,7 @@ import Mathlib.RingTheory.Radical.NatInt
 # LeanPool.ABCExceptions.Section2
 -/
 
-@[expose] public section
+public section
 
 open Finset UniqueFactorizationMonoid
 

LeanPool/ABCExceptions/Section4.lean

@@ -27,7 +27,7 @@ parts of the paper.
 
 -/
 
-@[expose] public section
+public section
 
 noncomputable section
 
@@ -257,6 +257,7 @@ lemma ThueBound.special_two (hd : 4 ≤ d) :
 end
 
 /-- We define `section4Sum i` to be `a i + b i + c i`. -/
+@[expose]
 def section4Sum (a b c : ℕ → ℝ) (i : ℕ) := a i + b i + c i
 local notation "s" => section4Sum a b c
 
@@ -394,6 +395,7 @@ lemma bound_4_point_9_upper (hε : 0 < ε) (f : ℕ → ℝ) (h45 : Bound4Point5
   linear_combination h45.lower + hε
 
 /-- Define `δₛ` to be the sum of the `δ_` values for `a, b, c`. -/
+@[expose]
 def deltaS (d : ℕ) (a b c : ℕ → ℝ) := δ_ d a + δ_ d b + δ_ d c
 local notation "δₛ" => deltaS d a b c
 

LeanPool/ACMax.lean

@@ -31,7 +31,7 @@ The statement decomposes into the equality clause (`algConn_completeBipartite_tw
 and the universal upper-bound clause (`algConn_le_two_of_card`).
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 

LeanPool/ACMax/AHL/AHLAmGm.lean

@@ -37,7 +37,7 @@ average-degree walk-count lower bound.
   i.e. `Λ ≥ (D − n)/n = d_avg − 1`.
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 

LeanPool/ACMax/AHL/AHLMarginals.lean

@@ -35,7 +35,7 @@ Throughout `hδ2 : ∀ v, 2 ≤ G.degree v`.  A directed edge is the `(penultima
   walks is exactly `D = ∑ v, deg v` — the normalization the weighted AM–GM (W7) consumes.
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 

LeanPool/ACMax/AHL/AHLStationary.lean

@@ -51,7 +51,7 @@ finsets with **no** `Dart`-to-walk bridge.  (`Walk.penultimate_concat` is alread
 "penultimate of an extension" fiber fact needs no fresh lemma.)
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 
@@ -168,7 +168,7 @@ omit [DecidableEq V] in
 /-- Unfolding of `nbWeight` on an explicit sigma constructor. -/
 theorem nbWeight_mk {x v : V} (p : G.Walk x v) :
     nbWeight (⟨v, p⟩ : Σ w : V, G.Walk x w) =
-      ∏ j ∈ Finset.Ico 1 p.length, ((G.degree (p.getVert j) : ℝ) - 1)⁻¹ := rfl
+      ∏ j ∈ Finset.Ico 1 p.length, ((G.degree (p.getVert j) : ℝ) - 1)⁻¹ := by rfl
 
 omit [DecidableEq V] in
 /-- **The weight is `1` on short walks.**  For a walk of length `≤ 1` the intermediate range
@@ -216,7 +216,7 @@ theorem nbWeight_concat {x v t : V} (p : G.Walk x v) (hp : ¬ p.Nil) (h : G.Adj
 
 /-- The global sigma finset of all length-`k` non-backtracking walks, tagged by their start: an
 element `⟨x, ⟨v, p⟩⟩` is a length-`k` non-backtracking walk `p : G.Walk x v`. -/
-def nbAll (k : ℕ) : Finset (Σ x : V, Σ v : V, G.Walk x v) :=
+@[expose] def nbAll (k : ℕ) : Finset (Σ x : V, Σ v : V, G.Walk x v) :=
   Finset.univ.sigma fun x => nbWalksFrom G x k
 
 /-- Membership in `nbAll`: `⟨x, ⟨v, p⟩⟩` lies in `nbAll k` iff `p` has length `k` and is
@@ -230,18 +230,18 @@ theorem mem_nbAll {k : ℕ} {t : Σ x : V, Σ v : V, G.Walk x v} :
 /-- **The last-edge marginal** (AHL's `xP = x`, def only).  The total weight of the length-`k`
 non-backtracking walks whose last directed edge is `(u, v)` — i.e. ending at `v` with penultimate
 `u`.  Its value `1` (for `k ≥ 1`, `G.Adj u v`) is the stationarity identity proved in node W3. -/
-noncomputable def nbLastWeight (k : ℕ) (u v : V) : ℝ :=
+@[expose] noncomputable def nbLastWeight (k : ℕ) (u v : V) : ℝ :=
   ∑ t ∈ (nbAll (G := G) k).filter (fun t => t.2.1 = v ∧ t.2.2.penultimate = u), nbWeight t.2
 
 /-- **The end marginal** (def only).  The total weight of the length-`k` non-backtracking walks
 ending at `v`; its value `deg v` (node W4) is the marginal of `nbLastWeight` over the neighbours of
 `v`. -/
-noncomputable def nbEndWeight (k : ℕ) (v : V) : ℝ :=
+@[expose] noncomputable def nbEndWeight (k : ℕ) (v : V) : ℝ :=
   ∑ t ∈ (nbAll (G := G) k).filter (fun t => t.2.1 = v), nbWeight t.2
 
 /-- **The total weight** (def only).  The total weight of all length-`k` non-backtracking walks;
 its value `D = ∑ v, deg v` (node W5) is the normalization `∑_v nbEndWeight k v`. -/
-noncomputable def nbWeightTotal (k : ℕ) : ℝ :=
+@[expose] noncomputable def nbWeightTotal (k : ℕ) : ℝ :=
   ∑ t ∈ nbAll (G := G) k, nbWeight t.2
 
 end ACMax

LeanPool/ACMax/AHL/NBWalk.lean

@@ -42,7 +42,7 @@ The degree-weighted lower bound on the *number* of non-backtracking walks and th
 assembly into the Moore bound are the follow-up counting node; this file lands the foundation only.
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 
@@ -51,7 +51,7 @@ open SimpleGraph
 /-- A walk is **non-backtracking** when it never immediately reverses a step: for every position
 `i` with `i + 2 ≤ w.length`, the vertex two steps ahead differs from the current one.  (For `nil`
 and single-edge walks the condition is vacuous.) -/
-def IsNonBacktracking {V : Type*} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) : Prop :=
+@[expose] def IsNonBacktracking {V : Type*} {G : SimpleGraph V} {u v : V} (w : G.Walk u v) : Prop :=
   ∀ i : ℕ, i + 2 ≤ w.length → w.getVert (i + 2) ≠ w.getVert i
 
 /-- Any walk of length at most `1` (in particular `nil` and a single edge) is non-backtracking:

LeanPool/ACMax/AHL/NBWalkCount.lean

@@ -34,7 +34,7 @@ over `fun v => Finset (G.Walk x v)` is not type-correct — the fibers must be t
 endpoint first, which is exactly what `nbWalksFrom` does).
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 
@@ -126,7 +126,7 @@ theorem card_nbWalksFrom [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (x : V
 
 /-- The one-edge non-backtracking extensions of a bundled walk `s = ⟨u, p⟩`: for each neighbour `t`
 of `u` other than the penultimate vertex of `p`, the walk `p.concat _`. -/
-def nbExtend (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (x : V)
+@[expose] def nbExtend (G : SimpleGraph V) [Fintype V] [DecidableEq V] [DecidableRel G.Adj] (x : V)
     (s : Σ v : V, G.Walk x v) : Finset (Σ v : V, G.Walk x v) :=
   (G.neighborFinset s.1 \ {s.2.penultimate}).image fun t =>
     if h : G.Adj s.1 t then ⟨t, s.2.concat h⟩ else ⟨x, Walk.nil⟩

LeanPool/ACMax/AHL/NBWeighted.lean

@@ -18,7 +18,7 @@ Alon–Hoory–Linial irregular Moore bound chain; the walk-count and average-de
 it live downstream (`AHL.AHLAmGm`, `Band.Sum`).
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 
@@ -28,7 +28,7 @@ variable {V : Type*} [Fintype V] {G : SimpleGraph V} [DecidableEq V] [DecidableR
 
 /-- `mₖ`: the total number of length-`k` non-backtracking walks, summed over all ordered
 start/end pairs.  By definition this is `∑ x, ∑ v, ((G.finsetWalkLength k x v).filter …).card`. -/
-def nbTotalWalks (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : ℕ :=
+@[expose] def nbTotalWalks (G : SimpleGraph V) [DecidableRel G.Adj] (k : ℕ) : ℕ :=
   ∑ x : V, ∑ v : V, ((G.finsetWalkLength k x v).filter IsNonBacktracking).card
 
 end ACMax

LeanPool/ACMax/Band/AssemblyAllRange.lean

@@ -19,7 +19,7 @@ This assembly replaces the split between the finite exact-Moore range and the
 polynomial large-order range by one exact non-backtracking certificate.
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 

LeanPool/ACMax/Band/CertAllRange.lean

@@ -15,7 +15,7 @@ exponent at least eight, the fourth nonconstant term of the binomial expansion
 gives a uniform certificate with no upper bound on the order.
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 

LeanPool/ACMax/Band/CertUniform.lean

@@ -27,7 +27,7 @@ terms and an exact chord identity for a cubic polynomial.  This replaces the fiv
 ratio certificates formerly used by `Band.Assembly`.
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 

LeanPool/ACMax/Band/Final.lean

@@ -22,7 +22,7 @@ The second range combines the direct incidence-capacity proof on
 orders `48` and `49` is harmless.
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 

LeanPool/ACMax/Band/KillSharp.lean

@@ -25,7 +25,7 @@ longer needed: at the longer target the SUM disjunct alone covers every cell of
 `55 ≤ n ≤ 122` (the EDGE disjunct was load-bearing exactly on `77 ≤ n ≤ 81` at the old target).
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 

LeanPool/ACMax/Band/Rows.lean

@@ -26,7 +26,7 @@ a degree-`3`-separated obstruction at `n ≥ 48`. Notation:
 Everything is `sorry`-free and axiom-clean (`[propext, Classical.choice, Quot.sound]`).
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 

LeanPool/ACMax/Band/Subset.lean

@@ -42,7 +42,7 @@ verification.
   `3 ≤ k ≤ L` inside `S`, in the `ZMod k` cyclic-map form.
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 

LeanPool/ACMax/Band/Sum.lean

@@ -33,7 +33,7 @@ buying the extra half-level over the pair form `ahl_irregular_moore`.
   arithmetic instantiates at the extremal `V₉/2`-core.
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 

LeanPool/ACMax/Counting/Cherry.lean

@@ -46,7 +46,7 @@ cut, so any disjoint `3`-block `P` with `2·e(P,N) + leak(P) ≤ 7` closes.
   `Δ ≤ 4`, `e(M) = 2` regime for every `n ≥ 18`.
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 
@@ -494,7 +494,7 @@ theorem residualCore_cherry (n : ℕ) (G : SimpleGraph (Fin n)) (h : ResidualCor
 
 open Classical in
 /-- The **cherry-touching hubs**: hubs adjacent to a cherry vertex. -/
-noncomputable def cherryHubs (G : SimpleGraph V) (x z y : V) : Finset V :=
+@[expose] noncomputable def cherryHubs (G : SimpleGraph V) (x z y : V) : Finset V :=
   (hubSet G).filter (fun w => G.Adj w z ∨ G.Adj w x ∨ G.Adj w y)
 
 open Classical in
@@ -610,7 +610,7 @@ theorem mem_richLowHubs {G : SimpleGraph V} {w : V} :
 open Classical in
 /-- The **bad neighbours** of an apex `t` against a cherry: neighbours of degree `≥ 5`
 or touching the cherry — the vertices that block the SingleVertex pair selection. -/
-noncomputable def badApexNbrs (G : SimpleGraph V) (x z y t : V) : Finset V :=
+@[expose] noncomputable def badApexNbrs (G : SimpleGraph V) (x z y t : V) : Finset V :=
   (G.neighborFinset t).filter (fun w => 5 ≤ G.degree w ∨ w ∈ cherryHubs G x z y)
 
 open Classical in
@@ -753,7 +753,7 @@ private theorem mem_hubTwins {G : SimpleGraph V} {g t : V} :
 open Classical in
 /-- The **iso-twin neighbours** of a hub, as a pinned `def` so that its instances stay
 stable across the `Fin n` / generic-`V` boundary. -/
-noncomputable def isoNbrs (G : SimpleGraph V) (g : V) : Finset V :=
+@[expose] noncomputable def isoNbrs (G : SimpleGraph V) (g : V) : Finset V :=
   G.neighborFinset g ∩ isoTwins G
 
 open Classical in

LeanPool/ACMax/Counting/CherryMShape.lean

@@ -44,7 +44,7 @@ with every other degree-3 vertex an iso twin.
   `Δ ≥ 5` ("fat") side of `ResidualCore` remains open.
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 

LeanPool/ACMax/Counting/CompactCell.lean

@@ -37,7 +37,7 @@ degree excess.
   the large-order reduction. The full theorem is assembled in `Band.Final`.
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 
@@ -51,7 +51,7 @@ open Classical in
 /-- The **slot value function** `σ(d) = (d−3)/(d−2)`: the per-slot worst-case
 surplus of a degree-`d` neighbour used as a leak carrier.  `σ(3) = 0`,
 `σ(4) = 1/2`, `σ(5) = 2/3`, `σ(6) = 3/4`, `σ → 1`. -/
-noncomputable def sigma (d : ℕ) : ℝ := ((d : ℝ) - 3) / ((d : ℝ) - 2)
+@[expose] noncomputable def sigma (d : ℕ) : ℝ := ((d : ℝ) - 3) / ((d : ℝ) - 2)
 
 open Classical in
 /-- The **mass factor** `c_u = 1 + Σ_{w∈N(u)} 1/(deg w − 2)`. -/
@@ -60,7 +60,7 @@ noncomputable def cW (G : SimpleGraph V) (u : V) : ℝ :=
 
 open Classical in
 /-- The **`σ`-sum** `Σσ_u = Σ_{w∈N(u)} σ(deg w)`. -/
-noncomputable def sigS (G : SimpleGraph V) (u : V) : ℝ :=
+@[expose] noncomputable def sigS (G : SimpleGraph V) (u : V) : ℝ :=
   ∑ w ∈ G.neighborFinset u, sigma (G.degree w)
 
 /-! ### `σ` arithmetic (`L-FB-2` real-valued facts) -/
@@ -398,7 +398,7 @@ open Classical in
 each of which is `σ`-usable.  This is the exact *spread* witness: present on every
 diameter-`≥ 4` "buried" world and absent on every diameter-`3` compact cell
 inhabitant. -/
-def HasUsableFarPair (G : SimpleGraph V) : Prop :=
+@[expose] def HasUsableFarPair (G : SimpleGraph V) : Prop :=
   ∃ u v : V, u ≠ v ∧ ¬G.Adj u v ∧ (∀ w : V, ¬(G.Adj u w ∧ G.Adj v w)) ∧
     (∀ w w' : V, G.Adj u w → G.Adj v w' → ¬G.Adj w w') ∧
     sigS G u ≤ 2 ∧ sigS G v ≤ 2
@@ -542,13 +542,13 @@ variable {n : ℕ}
 open Classical in
 /-- The **total degree excess** `X = ∑_{deg v ≥ 5} (deg v − 4)` (ℕ-valued;
 the truncated subtraction is exact since every summand has degree ≥ 5). -/
-noncomputable def excessX (n : ℕ) (G : SimpleGraph (Fin n)) : ℕ :=
+@[expose] noncomputable def excessX (n : ℕ) (G : SimpleGraph (Fin n)) : ℕ :=
   ∑ v ∈ Finset.univ.filter (fun v => 5 ≤ G.degree v), (G.degree v - 4)
 
 open Classical in
 /-- The **radius-3 combinatorial ball** around `u₀`: `u₀` together with its
 neighbours, second neighbours, and third neighbours. -/
-noncomputable def closeSet (G : SimpleGraph (Fin n)) (u₀ : Fin n) : Finset (Fin n) :=
+@[expose] noncomputable def closeSet (G : SimpleGraph (Fin n)) (u₀ : Fin n) : Finset (Fin n) :=
   insert u₀ (G.neighborFinset u₀
     ∪ (G.neighborFinset u₀).biUnion (fun w => G.neighborFinset w)
     ∪ ((G.neighborFinset u₀).biUnion (fun w => G.neighborFinset w)).biUnion
@@ -875,6 +875,6 @@ cover `53 + 6·C₀` (the disjoint-slot 6X covering: heavy counts are dominated
 by their own excess pools) when a light usable vertex exists; the second arm
 `199990` dominates both the all-usable-heavy case (`n + 8 ≤ 5·29877`) and the
 hoarding wall (`199985 = 6·33322 + 53`). -/
-def boundLin (C₀ : ℕ) : ℕ := max ((151 + 11 * C₀) / 2) 520
+@[expose] def boundLin (C₀ : ℕ) : ℕ := max ((151 + 11 * C₀) / 2) 520
 
 end ACMax

LeanPool/ACMax/Counting/CompactLedgers.lean

@@ -51,7 +51,7 @@ same-count hubs with zero internal degree, zero `mCross` and no adjacency shares
 shared twins would assemble a good `K_{2,3}` (`Σ₅deg = 21`), contradicting
 `no_good_K23` (`no_two_saturated_deg6`). -/
 
-@[expose] public section
+public section
 
 namespace ACMax
 

LeanPool/ACMax/Counting/DecoratedC4.lean

@@ -16,7 +16,7 @@ The four-cycle itself misses the order-15 cut inequality by one edge; adjoining
 one parent, or two adjacent parents, supplies exactly the missing slack.
 -/
 
-@[expose] public section
+public section
 
 namespace ACMax