Repository navigation

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

Draft

Vilin97 wants to merge 435 commits into

mainfrom

feature/reduce-blanket-exposure

Draft

WIP: Remove blanket section exposure across Lean Pool#529
Vilin97 wants to merge 435 commits into
mainfrom
feature/reduce-blanket-exposure

This pull request is big! We're only showing the most recent 250 commits

Commits on Oct 2, 2026
- Expose OperatorTheory definitions used by exported proofs
  Vilin97
  committed
  3639881
- Expose OperatorTheory predicates and auxiliary definitions
  Vilin97
  committed
  25b1e26
- Merge current main for new project exposure migration
  Vilin97
  committed
  0bb8228
- Replace blanket exposure in NandakumarRamanaRao modules
  Vilin97
  committed
  cc170c0
- Expose NRR definitions used by imported proofs
  Vilin97
  committed
  e824c0a
- Expose two Crouzeix definitions required by shard 05
  Vilin97
  committed
  59ee854
- Expose NRR definitions explicitly unfolded across modules
  Vilin97
  committed
  b5816cf
- Keep exposed power-cell declarations within style width
  Vilin97
  committed
  fea1bd8
- Expose imported definitions used by cross-module proofs
  Vilin97
  committed
  0f5b021
- Expose NRR definitions used by imported rfl proofs
  Vilin97
  committed
  27c2521
- Merge current main for BrillNoetherGraphs exposure migration
  Vilin97
  committed
  6363cbf
- Replace blanket exposure in BrillNoetherGraphs modules
  Vilin97
  committed
  399d33b
- Expose BrillNoetherGraphs definitions unfolded across modules
  Vilin97
  committed
  8daaa69
- Expose BrillNoetherGraphs definitions used by imported reductions
  Vilin97
  committed
  7d25ca1
- Expose BrillNoetherGraphs definitions used by imported reflexivity proofs
  Vilin97
  committed
  389b109
- Expose additional BrillNoetherGraphs proof dependencies
  Vilin97
  committed
  170609f
- Expose NRR definitions required by shard 03 and fix ZeroSum proof
  Vilin97
  committed
  4bb5db9
- Expose OddSphereDegree definitions required by module proofs
  Vilin97
  committed
  14a35b7
- Expose Crouzeix boundary phase contractive predicate
  Vilin97
  committed
  865b312
- Expose ZeroSum relabel and prove permutation compatibility explicitly
  Vilin97
  committed
  0c3dfb2
- Expose Brill definitions named by imported dsimp proofs
  Vilin97
  committed
  4fd8963
- Expose NRR convex body definitions required by exported equations
  Vilin97
  committed
  66ff5d0
- Expose NRR projective and homology definitions from shard 04
  Vilin97
  committed
  3f74588
- Merge remote-tracking branch 'origin/main' into HEAD
  Vilin97
  committed
  0ba6712
- Remove blanket exposure from RegtsSevenster modules
  Vilin97
  committed
  04c57dc
- Expose Brill definitions required by exported module proofs
  Vilin97
  committed
  e1e2d50
- Expose smooth closed ball approximation for exhaustion proofs
  Vilin97
  committed
  7cb6733
- Expose RegtsSevenster definitions used across modules
  Vilin97
  committed
  1748f35
- Expose Regts core definitions required by module proofs
  Vilin97
  committed
  dc74f9f
- Expose Regts downstream definitions used by imported proofs
  Vilin97
  committed
  7c03ad7
- Expose NRR definitions required by exported module equations
  Vilin97
  committed
  261cb83
- Expose Regts Deligne providers required by module proofs
  Vilin97
  committed
  6aa4c73
- Expose Brill reduction providers across module boundaries
  Vilin97
  committed
  f0100da
- Prove NRR cochain cast by degree equality under modules
  Vilin97
  committed
  fcc9c20
- Expose remaining Regts doubling providers across modules
  Vilin97
  committed
  b069759
- Expose Regts tensor unit for exported monoidal proofs
  Vilin97
  committed
  01bfbe0
- Remove redundant Regts exposure warnings
  Vilin97
  committed
  658ef80
- Merge current main into exposure reduction candidate
  Vilin97
  committed
  c85dd53
- Reduce TuttePath blanket exposure to used definitions
  Vilin97
  committed
  4e22f41
- Expose Brill AspPerm identity for imported simplification
  Vilin97
  committed
  5b1b1bc
- Expose TuttePath singleton for exported endpoints
  Vilin97
  committed
  01cf47c
- Reduce NashEmbedding blanket exposure for explicit cross-module reductions
  Vilin97
  committed
  742e195
- Merge remote-tracking branch 'origin/main' into feature/pr529-nash-d89-prep-20261002
  Vilin97
  committed
  4f84f8d
- Reduce ParameterFreeGradient blanket exposure sections
  Vilin97
  committed
  1f5a391
- Expose ParameterFreeGradient definitions used by cross-module unfold
  Vilin97
  committed
  9754295
- Expose ParameterFreeGradient definitions used by cross-module simp
  Vilin97
  committed
  6db516d
- Expose O3 definitions used by qualified reductions
  Vilin97
  committed
  d457d93
- Expose NashEmbedding predicate wrappers and fix attribute placement
  Vilin97
  committed
  31824c6
- Expose ParameterFreeGradient wrappers required by full project build
  Vilin97
  committed
  a6a0ec4
- Expose Nash providers required by dependent module proofs
  Vilin97
  committed
  bad683b
- Expose ParameterFreeGradient providers found by full import recheck
  Vilin97
  committed
  4086c36
- Expose Nash Gram and sequence operators for exported proofs
  Vilin97
  committed
  8caa6ad
- Expose OperatorTheory providers for full project imports
  Vilin97
  committed
  e6b5d9f
- Expose ParameterFreeGradient recurrence and guard providers
  Vilin97
  committed
  7c02495
- Merge branch 'feature/pr529-nash-d89-prep-20261002' into HEAD
  Vilin97
  committed
  4f0802c
- Expose Nash rapid-decay and Gunther data providers
  Vilin97
  committed
  65680d9
- Expose definitions needed by parameter-free gradient imports
  Vilin97
  committed
  1c7e753
- Expose local finite-data and kernel definitions
  Vilin97
  committed
  fc5b6a6
- Expose downstream parameter-free gradient carriers
  Vilin97
  committed
  3eeddf5
- Expose Nash free-map dimension and predicate
  Vilin97
  committed
  5575f2c
- Expose parameter-free gradient controller interfaces
  Vilin97
  committed
  a6dd6d5
- Expose Nash pointwise frame independence
  Vilin97
  committed
  2cc983e
- Expose gradient phase witnesses and trace interfaces
  Vilin97
  committed
  17dd198
- Expose NRR definitions required by downstream module proofs
  Vilin97
  committed
  03473dc
- Expose Regts providers needed across module boundaries
  Vilin97
  committed
  0b96a05
- Expose Nash Gram definitions for the final torus proof
  Vilin97
  committed
  459e5e7
- Repair scoped ParameterFreeGradient exposure dependencies
  Vilin97
  committed
  8138e14
- Merge reviewed Nash and ParameterFreeGradient module exposure repairs
  Vilin97
  committed
  306ed38
- Expose NRR definitions unfolded by importing modules
  Vilin97
  committed
  deab7ea
- Expose Regts definitions unfolded by importing modules
  Vilin97
  committed
  a1e2c61
- Reconcile current main with reviewed module exposure repairs
  Vilin97
  committed
  d0af73e
- Expose ParameterFreeGradient definitions unfolded by importers
  Vilin97
  committed
  aecf032
- Expose Regts definitions used by imported rewrite steps
  Vilin97
  committed
  346824b
- fix: expose canonical cell lower graph for continuity proofs
  Vilin97
  committed
  aadbbc7
- fix: expose Brill graph definitions required by fresh CI
  Vilin97
  committed
  cde2a0d
- fix: expose compact Nash differential and metric casts
  Vilin97
  committed
  764503a
- refactor: replace OrderClosures blanket exposure with body providers
  Vilin97
  committed
  ee4c94a
- fix: resolve Regts diagnostic providers and coefficient inference
  Vilin97
  committed
  c447c95
- fix: resolve BrillNoetherGraphs fresh full import diagnostics
  Vilin97
  committed
  a733f4c
- fix: resolve NashEmbedding fresh full import diagnostics
  Vilin97
  committed
  b36bcdf
- fix: resolve ParameterFreeGradient fresh full import diagnostics
  Vilin97
  committed
  a7a84b4
- fix: resolve OrderClosures fresh full import diagnostics
  Vilin97
  committed
  3855168
- Merge current main while preserving scoped exposure repairs
  Vilin97
  committed
  d109f00
- Expose Regts providers required by completed full-root diagnostics
  Vilin97
  committed
  dad7ce8
- Replace Sendov blanket exposure with explicit proof providers
  Vilin97
  committed
  46a5d07
- Expose diagnosed pullback and predicate reduction providers
  Vilin97
  committed
  dcdc88c
- Expose verified NRR exported reflexivity providers
  Vilin97
  committed
  1cb2b6e
- Expose traced Brill providers and close the retained reflexivity goal
  Vilin97
  committed
  8924707
- Combine retained order-completeness attribute elements
  Vilin97
  committed
  d74a740
- Expose Sendov finite packing reflexivity providers
  Vilin97
  committed
  ef2135c
- Expose diagnosed separator and reviewed NRR wrapper bodies
  Vilin97
  committed
  3cad874
- fix: expose predicate and ideal bodies required by project proofs
  Vilin97
  committed
  90e9675
- fix: expose Regts bodies required by skein and Deligne proofs
  Vilin97
  committed
  419ab01
- fix: expose graph constructors and predicates used by Brill proofs
  Vilin97
  committed
  2136a45
- Merge remote-tracking branch 'origin/main' into HEAD
  Vilin97
  committed
  3203768
- Expose NRR imported proof dependencies and zero-sum equivalence
  Vilin97
  committed
  4475510
- Expose Sendov packing bridge recursion bodies
  Vilin97
  committed
  28fbc21
- Expose gradient and order-closure proof body dependencies
  Vilin97
  committed
  abde9fd
- Expose Brill graph and subdivision proof body dependencies
  Vilin97
  committed
  fd2ff5c
- Expose Regts imported algebra and skein proof dependencies
  Vilin97
  committed
  45d1370
- Merge remote-tracking branch 'origin/main' into HEAD
  Vilin97
  committed
  6b12146
- Reduce clique-tree exposure to six required definition bodies
  Vilin97
  committed
  09c0ea2
- Expose Sendov kernel certificate arithmetic dependencies
  Vilin97
  committed
  9b4c805
- Expose chordal predicates needed by clique-tree proofs
  Vilin97
  committed
  f7550c7
- Expose NRR prime-model and polyhedron proof dependencies
  Vilin97
  committed
  213801c
- Expose Brill graph and certificate proof dependencies
  Vilin97
  committed
  3e2635a
- Expose gradient trajectories and order convergence proof bodies
  Vilin97
  committed
  61a6fd1
- Expose seven concrete NRR model and evaluation providers
  Vilin97
  committed
  19b922f
- Expose concrete Regts providers and close reflexive PowTriangle goal
  Vilin97
  committed
  f19cada
- Expose NRR identity and orthant predicates for imported proofs
  Vilin97
  committed
  112e635
- Expose concrete PFG execution and Order completeness providers
  Vilin97
  committed
  a21e27b
- Expose concrete Brill subdivision and finite atlas providers
  Vilin97
  committed
  12ef2e7
- Expose standard simplex body for public NRR instances
  Vilin97
  committed
  7003262
- Expose NRR subtype bodies required by public finite instances
  Vilin97
  committed
  1d3c89c
- Expose concrete analytic bridge and Order predicate providers
  Vilin97
  committed
  756a668
- Expose four NRR facet shuffle equivalence providers
  Vilin97
  committed
  4b0c00a
- Expose thirty Regts coherence and skein providers
  Vilin97
  committed
  2d1a5d7
- Expose NRR terminal cancellation propositions and source subtype
  Vilin97
  committed
  66ef904
- Expose twenty seven Brill subdivision and factorization providers
  Vilin97
  committed
  fec00d4
- Expose thirty PFG certificate and ordinal stage providers
  Vilin97
  committed
  7dce747
- Expose eight NRR maximal flag reduction providers
  Vilin97
  committed
  36c75b4
- Expose six PFG and OrderClosures imported reduction providers
  Vilin97
  committed
  fab8d63
- Expose forty Regts coherence and skein reduction providers
  Vilin97
  committed
  55d76f1
- Expose NRR prime orbit cycle record for representative types
  Vilin97
  committed
  70180ed
- Expose concrete Brill graph and divisor reduction providers
  Vilin97
  committed
  9892577
- Expose PFG trial horizon budget and record projections
  Vilin97
  committed
  471af93
- Expose NRR affine regularity zero witnesses and orbit counts
  Vilin97
  committed
  fa71390
- Expose PFG controller and remaining trial contract carriers
  Vilin97
  committed
  87195be
- Expose NRR order complex model point projection
  Vilin97
  committed
  366331b
Commits on Oct 3, 2026
Commits on Oct 4, 2026
- Expose three reviewed Brill coverage predicates
  Vilin97
  committed
  ec067f6
- Expose reviewed odd unit padding for imported conversion
  Vilin97
  committed
  31d63f5
- Expose two reviewed Brill proof predicates
  Vilin97
  committed
  2855eef
- Expose nine reviewed Stafford provider bodies
  Vilin97
  committed
  e30052c
- Expose three reviewed Regts coordinate bodies
  Vilin97
  committed
  e591cbf
- Expose seven reviewed Brill provider bodies
  Vilin97
  committed
  e2710a9
- Expose three reviewed Stafford provider bodies
  Vilin97
  committed
  5f82d29
- Expose the two reviewed Regts braiding word bodies
  Vilin97
  committed
  5ffd4eb
- Expose the reviewed PairStage scalar map bodies
  Vilin97
  committed
  4006cdb
- Expose the reviewed Regts model permutation wrapper
  Vilin97
  committed
  ba4fd98
- Expose five reviewed Stafford pair-stage provider bodies
  Vilin97
  committed
  e06cd6b
- fix: expose sector and iterated Weyl definition wrappers
  Vilin97
  committed
  5f28b8e
- fix: expose diagonal colour partner for imported reflexivity
  Vilin97
  committed
  0ef2dcd
- fix: expose Stafford definition wrappers needed by unchanged proofs
  Vilin97
  committed
  9dc253e
- fix: expose block flag alias for unchanged inverse identity
  Vilin97
  committed
  4e51cbb

Commits

Commits on Oct 2, 2026

Commits on Oct 3, 2026