WIP: Remove blanket section exposure across Lean Pool - #529

Draft

Vilin97 wants to merge 50 commits into

mainfrom

feature/reduce-blanket-exposure

Commits on Sep 25, 2026

Begin removing blanket section exposure
Vilin97
committed
f7e0dbc
Reduce blanket exposure in eight validated projects
Vilin97
committed
8bbe46e
Reduce section exposure in fourteen verified projects
Vilin97
committed
83802f2
Remove blanket exposure in twenty-three verified projects
Vilin97
committed
614f631
Validate exposure reduction in eleven more projects
Vilin97
committed
a1985df
Remove blanket exposure from four more verified projects
Vilin97
committed
be0a686
Narrow exposure in interaction trees and geometry projects
Vilin97
committed
d8166ca
Remove blanket exposure from four further verified projects
Vilin97
committed
eaa90f3
Narrow exposure in graph counting and combinatory algebras
Vilin97
committed
a8a0d1e
Narrow exposure in computability and Selberg sieve projects
Vilin97
committed
6d1df03
Remove blanket exposure in four arithmetic and probability projects
Vilin97
committed
afd6587
Narrow exposure in four analytic and algebraic projects
Vilin97
committed
e797ca4
Narrow exposure in Komlos discrepancy and circuit categories
Vilin97
committed
b47b1ed
Narrow exposure in covering, PCF, and spectral positivity projects
Vilin97
committed
db218b2
Narrow exposure in Brouwer and circuit complexity proofs
Vilin97
committed
f745834
Reduce exposure in three combinatorics and arithmetic projects
Vilin97
committed
192a235
Place Frieze projection lemmas after constructor definitions
Vilin97
committed
4f26b7b
Narrow exposure in Demazure operators and finite distance bounds
Vilin97
committed
ddc4628
Use public construction equations in Anderson and Pauli bounds
Vilin97
committed
eb4ef2a
Use projection equations for Demazure products
Vilin97
committed
41cceb0
Narrow computational exposure in complex analysis
Vilin97
committed
8207eca
Expose arithmetic formulas used by downstream proofs
Vilin97
committed
f29119e
Reduce exposure in Diophantine and sieve projects
Vilin97
committed
3ff5bbb
Narrow exposure in temporal logic and counting projects
Vilin97
committed
112e65a
Remove blanket exposure from three-chain geometry
Vilin97
committed
57dabce

Commits on Sep 26, 2026