Samplinglib · Current Progress

Seven routes, one collaboration board.

SampleWiki, Riemannian Optimization, Optimisation, Statistical Optimal Transport, Discrete Sampling, and higher-order sampling advance in parallel on one page. Each theorem-sized task is a Frontier Cell; lower-level mathematics is shared only after a reuse/compatibility audit, so collaborators can move independently without rebuilding the same Lean foundation.

Dependency-first frontier route

SampleWiki Route

Immediate priority: extend the verified Chewi spine until useful frontier sampling results can enter the same theorem graph with exact source fidelity.

Partially formalized · source fidelity separateOpen SampleWiki ↗

Route milestones

active01

Dependency-first Chewi spine

Continue the shortest prerequisite route through the Chewi textbook graph toward useful SampleWiki results.

active02

Source fidelity + theorem insertion

Audit frontier statements against primary papers, then attach verified declarations to the existing theorem graph.

planned03

Proximal / LMC / ULD / MALA foundations

Prioritize reusable analytic roots that unlock multiple frontier cases rather than isolated terminal proofs.

planned04

Frontier result closure

Advance the highest-value reachable SampleWiki cells once their shared parents are stable.

Registered Frontier Cells

ASTIS-SW-SPHMC-rgo-fiber-w2-contractionblocked

SPHMC restricted-Gaussian fiber Wasserstein contraction

For alpha>0 and eta>0, prove that the normalized restricted-Gaussian fibers R_eta,y(dx) proportional to exp(-V(x)-||x-y||^2/(2 eta)) dx of an alpha-strongly convex potential satisfy W2(R_eta,y,R_eta,y') <= ||y-y'||/(1+alpha eta); then specialize alpha=kappa^{-1} to the exact kappa/(kappa+eta) factor in SPHMC Lemma 4.17.

ASTIS-SW-GAUSSIAN-COMPLEXITY-eigenbasisclaimed

Gaussian complexity: eigenbasis

For each fixed delta in (0,1), there exists d_0(delta) such that for d>=d_0, 2<=kappa<=d^(1-delta), 0<epsilon<=1/10, Q_G>=(delta/256)sqrt(kappa)log d even with disclosed precision spectrum.

ASTIS-SW-GAUSSIAN-COMPLEXITY-signclaimed

Gaussian complexity: sign

For every integer d>=1, kappa>=4 and 0<epsilon<=1/16, Q_G(d,kappa,epsilon)>=(1/256)min(d,sqrt(kappa)log(1+d/(sqrt(kappa)epsilon))) in the exact Section 2 model.

ASTIS-SW-GAUSSIAN-COMPLEXITY-actual-mixture-lawsproved locally

Construct the actual determinant-conditioned Gaussian mixtures

ASTIS-SW-GAUSSIAN-COMPLEXITY-actual-radial-tvproved locally

A radial test bounds mixture TV

For \(n\ge3\), \(\kappa\ge4\), \(\ell\ge0\), let \(A_O=\frac{\kappa+1}{2}I_n-\frac{\kappa-1}{4}(O+O^\top)\), \(\mu\) be normalized full real orthogonal Haar, \(\nu_\pm=2\mu|_{\{\det O=\pm1\}}\), \(\gamma_O=\mathcal N(0,A_O^{-1})\), \(P_\pm=\nu_\pm\mathbin{\mathrm{bind}}\gamma\), and \(p_O(x)=\frac{\sqrt{\det A_O}}{(2\pi)^{n/2}}e^{-x^\top A_Ox/2}\) on Euclidean volume. Set \(t(x)=e^{-\ell\|x\|^2}\) and \(H(\ell)=\int\det(O)\int t(x)p_O(x)\,dx\,d\mu(O)\). Then \(2|H(\ell)|\le\sup_{B\ \mathrm{measurable}}|P_+(B)-P_-(B)|\). Includes zero tilt; all actual law, probability, L1 and supremum conditions are internal.

ASTIS-SW-GAUSSIAN-COMPLEXITY-block-precisionproved locally

Literal source block diagonal diag(A_O1,...,A_Ok,I_(d-kn)), k=floor(d/n), with the exact contiguous finite-coordinate adapter.

ASTIS-SW-GAUSSIAN-COMPLEXITY-column-transportproved locally

Transport the actual Gaussian kernel to the full-Haar first-column law

For natural \(n\ge3\) and real \(\kappa\ge4\), set \(s=\sqrt\kappa\), \(r=(1-1/n)(s-1)/(s+1)\), \(\ell=(4ns+(s-1)^2)/(8n(n-1))\), and \(\beta=(-1)^{n-1}(s-1)^{n-1}(1-1/n)^{n/2}/(s+1)^n\). Let \(\mu\) be normalized Haar probability on full \(O(n)\), \(c(O)=Oe_1\) in genuine Euclidean space and \(\nu=c_*\mu\). Put \(f(y)=((s+1)y_1-(s-1))/(1+r^2-2ry_1)^{n/2}\), using real half-dimension powers. Let \(A_O=((\kappa+1)/2)I-((\kappa-1)/4)(O+O^\top)\), \(\gamma_O=\mathcal N(0,A_O^{-1})\), and \(H_\gamma(\ell)=\mathbb E_\mu[\det(O)\int e^{-\ell\|x\|_2^2}\,d\gamma_O]\). Then \(\nu\) is a probability, \(\|y\|_2=1\) almost surely, \(Q_*\nu=\nu\) for every fixed full orthogonal matrix \(Q\), \(f\in L^1(\nu)\), and \(H_\gamma(\ell)=\beta\int f\,d\nu\). This does not yet identify \(\nu\) with canonical normalized surface measure or give either Poisson integral value.

ASTIS-SW-GAUSSIAN-COMPLEXITY-component-probabilitiesproved locally

Normalize the actual positive and negative determinant Haar priors

ASTIS-SW-GAUSSIAN-COMPLEXITY-determinant-cancellationproved locally

Actual LemmaB6 Eq15 signed normalization expectation for every Borel h with E|h(O_00)| finite, n>=3 and kappa>=4, consuming actual pointwise normalizer and Haar minor cancellation.

ASTIS-SW-GAUSSIAN-COMPLEXITY-factorizationproved locally

For n>=3,kappa>=4 and any real orthogonal O, the literal A_O equals one quarter of M^T M, where M=(sqrt(kappa)+1)I-(sqrt(kappa)-1)O.

+ 221 additional registered cells.

Detailed dependency/audit view

Boumal route

Riemannian Optimization

Formalize Boumal while sharing only mathematically identical geometry foundations with the sampling route. Convention differences stay explicit in adapters.

Partially formalized · source fidelity separateOpen library ↗

Route milestones

scaffold01

Boumal source map

The eleven-chapter public route and source boundaries are established.

planned02

Shared geometry floor

Audit Mathlib and Samplinglib first; Chewi sampling §2.5 is the first explicit cross-route checkpoint.

planned03

Boumal Chapters 1–4

Definitions, embedded first-order geometry, and first-order Riemannian algorithms.

planned04

Boumal Chapters 5–11

Second-order geometry/algorithms, general and quotient manifolds, additional tools, and geodesic convexity.

Registered Frontier Cells

ASTIS-RIEM-sphere-rayleighmerged

Rayleigh sphere gradient and actual critical eigenvectors

For a real symmetric matrix A, let F(x)=xᵀAx on the unit sphere with the metric induced by the Euclidean inner product. The chosen smooth ambient quadratic extension has gradient2Ax. The tangent projector sends u to u−⟨x,u⟩x, so the sphere gradient is2(Ax−⟨x,Ax⟩x). Its vanishing is equivalent to Ax=⟨x,Ax⟩x; thus the stationary unit vectors are exactly eigenvectors of A, and every unit eigenvector is stationary.

ASTIS-RIEM-sphere-rayleigh-stationarymerged

Rayleigh sphere critical points and actual unit eigenvectors

Open Boumal source route

Sinho Chewi · arXiv:2605.07006

Optimisation

Formalize Chewi's public optimization notes section by section, reusing Mathlib/Optlib/CvxLean and exposing exact shared convex/proximal/mirror foundations with sampling.

Partially formalized · source fidelity separateOpen library ↗

Route milestones

scaffold01

Chewi Lectures on Optimization source map

The public formalization spine follows arXiv:2605.07006: §§1–13 plus Appendix A.

planned02

Convexity, flow, descent, acceleration

Formalize §§1–5 while reusing compatible Mathlib/Optlib declarations.

planned03

Non-smooth, Frank-Wolfe, proximal, duality

Formalize §§6–9 and expose exact shared foundations with sampling when statements coincide.

planned04

Mirror, alternating, stochastic, interior-point

Formalize §§10–13 and audit sampling intersections around mirror/proximal/stochastic structure.

Chewi · Niles-Weed · Rigollet

Statistical Optimal Transport Route

Eight chapters and two appendices share the same reader, source-fidelity protocol and canonical Lean floor as the existing libraries.

Partially formalized · source fidelity separateOpen library ↗

Route milestones

scaffold01

Source map and shared entry points

8 chapters + A/B; exact page anchors. Audit convexity, probability and existing coupling code before introducing anything new.

planned02

Chapter 1: transport foundation

Couplings, Wasserstein distance, Brenier and duality. Reuse shared convex/marginal/compactness ingredients.

planned03

Parallel branches after Chapter 1

2–3 statistical estimation; 4 entropic transport; 5→6 flows and sampling; 7→8 metric geometry and barycenters.

planned04

Source omissions and transport review

Use Villani / Santambrogio / AGS for missing analytic details. Separate conceptual correspondence from certified Lean reuse.

Optimisation × Sampling research route

Higher-Order Smoothness × Sampling

Determine when additional potential smoothness yields a real sampling advantage at a fixed oracle and total computational cost. Existing high-order sampling literature is the starting point, not a novelty claim.

research planResearch contract and literature ↗

Route milestones

planned01

Regime and oracle matrix

Separate potential smoothness p, derivative access q, dynamical order k and discretization order r; fix metric, starts and dimension-dependent constants.

planned02

Shared Taylor and stochastic local error

Search existing Taylor, moment and coupling APIs; prove one useful local-error/invariant-target interface before a full rate.

planned03

Mixing plus discretization

Couple an audited local error with a compatible contraction theorem; count derivative evaluations and matrix/tensor work, not iterations alone.

parallel04

Lower bounds remain an independent lane

SampleWiki studies hard instances and information transcripts. Compare the two lanes only after oracle, class, metric and costs match.

Chen · Štefankovič · Vigoda

Discrete Sampling Route

Finite-state Ising/Glauber, hard-core and matroid sampling. Same shared graph and source/mirror gates; not continuous-sampling time discretization.

scaffoldOpen library ↗

Route milestones

scaffold01

Pinned source and Ising entry

12 sections, 72 anchors; read Ising definitions early. Section 12 mixing proofs must be recovered from cited original papers.

planned02

Shared finite probability and kernel floor

Reuse PMF, measures, kernels and finite linear algebra; fix support, feasible pinnings, reversibility and clock before mixing.

planned03

Dirichlet / entropy / local-to-global

Pull §3 forward; prove finite dissipation adapters, uniform conditional-influence bounds and factorization with the exact normalization.

candidate04

Cross-domain conceptual mirrors

PI/chi-square, modified LSI/KL, finite transport geometry and conditional covariance. Independent source review never substitutes for a Lean transport certificate.

Fearnhead · Nemeth · Oates · Sherlock

Markov Chain Monte Carlo Route

General-state kernel construction, scalable MCMC and estimation. Shared with continuous and discrete sampling without identifying a method family with a target class.

scaffoldOpen library ↗

Route milestones

planned01

Kernel → invariance → convergence

§§1.3,2.1 and Roberts–Rosenthal §§2–4; no SDE/RKHS bottleneck for finite MH or Gibbs.

planned02

Diffusions / geometry / estimation branch separately

ULA and MALA reuse shared analysis with exact clock/bias adapters; HMC and PDMP need augmented-state contracts.

scaffold03

Six primary chapters and ten extensions

Every extension has a parent chapter and its own pinned source. No theorem-completion credit.

candidate04

Conceptual bridges with independent review

Metropolis correction, weak limits, lifting, perturbation and block conditionals. Candidate labels never certify formal transport.

All routes · shared prerequisite partial order

Share mathematical cores; keep transports explicit.

First satisfy the front-loaded four-textbook critical path, then select a dependency-ready theorem delta with the largest audited downstream reuse per realistic proof cost. Textbook order is a source order, not necessarily the optimal Lean dependency order.

Convexity, measure theory and calculus start in parallel after contract alignment. Their consumers branch, rather than waiting for every textbook chapter. These are planned reuse audits, not compiler-certified dependency edges.

planned-reuse-audit

Fix statements, spaces and access contracts

Parents: none — start here

Pin measures, spaces, norms, constants, metrics, input access, randomness, output error and source editions before comparing or sharing routes.

Reuse search: Samplinglib Registry; active Frontier Cells; source maps; frontloaded-shared-spine.json

Consumers: all, discrete-sampling, mcmc

planned-reuse-audit

Euclidean, inner-product and matrix floor

Parents: contracts

Coordinates, inner products, norms, symmetric/PSD matrices and quadratic-energy conventions used repeatedly in the first textbook window.

Reuse search: Mathlib inner-product/matrix APIs; TechnicalLemmas/Geometry/EuclideanSpaceCoordinates.lean

Consumers: log-concave-sampling, optimisation, riemannian-optimization, statistical-optimal-transport, discrete-sampling, mcmc

planned-reuse-audit

Measures, integration, maps and kernels floor

Parents: contracts

Probability normalization, pushforwards, products, marginal transfer, finite moments and deterministic-map versus kernel interfaces.

Reuse search: TechnicalLemmas/Measure; Mathlib MeasureTheory and Probability.Kernel

Consumers: log-concave-sampling, statistical-optimal-transport, samplewiki-route, higher-order-sampling, discrete-sampling, mcmc

planned-reuse-audit

Shared probability kernels and composition

Parents: measure

One measurable-kernel, composition and stationarity API with finite PMF adapters. No spatial differentiation is required.

Reuse search: Samplinglib Probability.ConditionalKernel; Mathlib Probability.Kernel and PMF

Consumers: discrete-sampling, log-concave-sampling, statistical-optimal-transport, mcmc

planned-reuse-audit

Scalar decay and contraction recurrence core

Parents: contracts

Scalar differential/recurrence comparison after the consumer proves its own dissipation identity. No manifold, OT, SDE or strong-convexity prerequisite.

Reuse search: Samplinglib FunctionalInequalities.SemigroupDecay; Mathlib scalar Gronwall and finite geometric sums

Consumers: discrete-sampling, log-concave-sampling, optimisation, riemannian-optimization, statistical-optimal-transport, mcmc

planned-reuse-audit

Differentiation, gradients, chain rules and Taylor bounds

Parents: contracts, linear-algebra

Source-neutral normed-space derivative/gradient/chain-rule interfaces; manifold and stochastic adapters remain explicit.

Reuse search: TechnicalLemmas/Analysis/Calculus; TechnicalLemmas/Analysis/Calculus/Taylor.lean; Mathlib calculus

Consumers: log-concave-sampling, optimisation, riemannian-optimization, statistical-optimal-transport, higher-order-sampling, mcmc

planned-reuse-audit

Convexity, strong convexity, subgradients and log-concavity adapters

Parents: contracts, linear-algebra

One Euclidean convex/subgradient/strong-convexity core; log-concavity, geodesic convexity, mixture convexity and displacement convexity are typed adapters or separate statements.

Reuse search: TechnicalLemmas/Analysis/ConvexSubgradient.lean; Geometry/{StrongConvexity,LogConcavity}.lean; Mathlib; Optlib; CvxLean

Consumers: log-concave-sampling, optimisation, statistical-optimal-transport, riemannian-optimization, samplewiki-route, mcmc

planned-reuse-audit

Couplings and minimal Wasserstein metric core

Parents: linear-algebra, measure

Shared coupling membership, marginal bookkeeping, p-moment costs, deterministic couplings and metric identities needed by OT Chapter 1 and Sampling §1.3 before route-local transport code is written.

Reuse search: TechnicalLemmas/Measure/{ProbabilityCouplingCompactness,TransportGluing,DisplacementInterpolationCoupling}.lean; pinned Mathlib Wasserstein audit

Consumers: log-concave-sampling, statistical-optimal-transport, discrete-sampling, mcmc

planned-reuse-audit

Convex conjugacy and duality pulled forward

Parents: measure, convex

Extract only the Fenchel/conjugacy core needed by OT §§1.5-1.6 from Optimization Chapter 9 without pretending Chapter 9 is complete.

Reuse search: Mathlib convex conjugacy; Optlib/CvxLean; Chewi Optimization Ch.9; OT Ch.1 exact hypotheses

Consumers: statistical-optimal-transport, optimisation

planned-reuse-audit

Finite reversible chain / variance / entropy adapters

Parents: kernel-algebra, linear-algebra, scalar-decay

Pull §3 forward: detailed balance, weighted L2 and Dirichlet identities; pair them with shared coercivity/decay without a diffusion chain rule. Fix P^k versus exp(t(P-I)), all rates and periodicity.

Reuse search: Mathlib PMF/Kernel/Matrix; Samplinglib Poincare, Generator, SemigroupDecay; primary §3

Consumers: discrete-sampling, log-concave-sampling, mcmc

planned-reuse-audit

Feasible pinnings and conditional influence/covariance

Parents: kernel-algebra, linear-algebra

Share finite conditional probability and covariance algebra, then prove uniform pinning bounds. Spectral independence is not Euclidean strong convexity.

Reuse search: Mathlib conditional probability, covariance, PSD matrices, SimpleGraph and Matroid; primary §§2,4.1

Consumers: discrete-sampling, optimisation

planned-reuse-audit

Diffusion generator and spatial-calculus adapter

Parents: kernel-algebra, calculus

Consume shared kernel algebra, then prove diffusion generator domains and integration by parts. Finite chains use finite-dirichlet and never wait for this spatial-calculus branch.

Reuse search: Mathlib Probability.Kernel; TechnicalLemmas/StochasticProcesses; FunctionalInequalities

Consumers: log-concave-sampling, samplewiki-route, mcmc

planned-reuse-audit

Minimal first-order manifold adapter

Parents: linear-algebra, calculus

Tangent spaces, differential, Riemannian metric and gradient interfaces. Boumal Chapter 3 may be pulled forward to unblock Sampling §2.5, with exact source dependencies retained.

Reuse search: Mathlib manifold APIs; TechnicalLemmas/Geometry/GeodesicConvexity.lean; ATLAS geometry memory

Consumers: log-concave-sampling, riemannian-optimization

planned-reuse-audit

Empirical measures and concentration floor

Parents: measure, convex

Share empirical-measure bookkeeping, Lipschitz-observable and basic concentration interfaces between Sampling §2.4 and OT Chapter 2; keep chaining, isoperimetry and minimax lower bounds separate unless statements exactly match.

Reuse search: Mathlib probability/concentration; FunctionalInequalities; compatible lean-stat-learning-theory leaves

Consumers: log-concave-sampling, statistical-optimal-transport

planned-reuse-audit

Transport existence, Brenier/duality wrappers and displacement

Parents: convex, coupling-wasserstein, duality

Build source-facing OT theorems on the shared metric/convex floor. Sampling §1.3 consumes the canonical transport core rather than creating a second mini-library.

Reuse search: TechnicalLemmas/Measure transport files; OT Chapter 1; Sampling §1.3; source-specific Brenier/Kantorovich hypotheses

Consumers: log-concave-sampling, statistical-optimal-transport, samplewiki-route

planned-reuse-audit

Gibbs variational principle, KL and functional-inequality energy

Parents: measure, convex

Common entropy/KL/convex core supports Sampling Chapter 2, OT Chapter 4 and proximal/MFLD routes; invariant-law and semigroup claims remain separate.

Reuse search: TechnicalLemmas/InformationTheory; FunctionalInequalities; existing Fisher/entropy APIs; primary proofs

Consumers: log-concave-sampling, samplewiki-route, statistical-optimal-transport, discrete-sampling, mcmc

planned-reuse-audit

Energy-dissipation and geometry-to-flow interfaces

Parents: calculus, convex, transport, entropy

Share scalar energy-dissipation/Gronwall patterns first; connect Euclidean, Riemannian and Wasserstein flows only through explicit adapters whose hypotheses are proved.

Reuse search: Optimization Ch.2; Sampling §§1.4-1.5; existing weak FP/FisherTransport APIs; AGS metric gradient-flow contracts

Consumers: log-concave-sampling, optimisation, riemannian-optimization, statistical-optimal-transport, samplewiki-route, mcmc

planned-reuse-audit

Statistical OT and metric-geometry branches

Parents: transport, concentration

OT Chapters 2-3 empirical/statistical leaves and 7-8 metric geometry branch. Statistical observation count n is never identified with sampling oracle cost.

Reuse search: OT Chapter 2-3 assumptions; Mathlib probability; concentration sources; statistical rather than computational n

Consumers: statistical-optimal-transport, mcmc

planned-reuse-audit

Higher-smoothness sampling upper bounds

Parents: measure, calculus, convex

Fix one potential class and oracle, prove local remainder/moment bounds and invariant target, then combine with an existing compatible contraction theorem.

Reuse search: Nesterov high-order Taylor models; Mou et al.; Shen-Lee; pinned sampling contraction leaves

Consumers: higher-order-sampling

planned-reuse-audit

Sampling oracle lower bounds

Parents: contracts, measure

Separate hard-instance and information-transcript lane. Additional convexity or statistical-testing ingredients are task-specific, not every upper-bound lemma.

Reuse search: SampleWiki exact lower-bound papers; oracle transcript kernels; testing/data-processing APIs

Consumers: samplewiki-route, discrete-sampling

planned-reuse-audit

Compare matched upper and lower contracts

Parents: upper, lower

Only compare identical potential classes, derivative access, error metrics, starts and cost conventions. A cross-domain lower bound requires an explicit reduction.

Reuse search: Common contract schema; no theorem equivalence inferred from a shared label

Consumers: all

planned-reuse-audit

Factorization and model-specific discrete mixing

Parents: finite-dirichlet, conditional-influence, entropy

Separate variance and entropy factorization, gap and mLSI, then audited Ising/hard-core/matroid adapters. §12 cited results require external proof completion.

Reuse search: Primary §§4-12; LPW; Chen-Liu-Vigoda and Blanca et al.; exact graph/temperature/clock contracts

Consumers: discrete-sampling

planned-reuse-audit

MCMC kernel construction and target invariance

Parents: kernel-algebra

General measurable kernels, MH rejection mass/support and conditional-update invariance. Keep path existence and mixing separate.

Reuse search: Existing Probability/ConditionalKernel, StochasticProcesses; pinned Mathlib Kernel; RR §2

Consumers: mcmc, discrete-sampling, log-concave-sampling

planned-reuse-audit

General-state drift, minorisation and coupling

Parents: mcmc-invariance, scalar-decay

Source-specific geometric/uniform ergodicity; finite-state adapter does not require SDEs.

Reuse search: RR §§3–4; pinned Mathlib measures, stopping times and coupling APIs

Consumers: mcmc, discrete-sampling, log-concave-sampling

planned-reuse-audit

Correlated averages and Poisson/CLT layer

Parents: mcmc-ergodicity, linear-algebra

Prove covariance/Poisson/regeneration hypotheses for estimator error, not only marginal mixing.

Reuse search: RR §5; shared covariance and integral interfaces

Consumers: mcmc, statistical-optimal-transport

Explore the Functor Hypergraph · Higher-order sampling research contract

Shared Lean floor

Parallel above; canonical below.

Geometry checkpoint

Chewi sampling §2.5 ↔ Boumal

Riemannian manifolds, tangent-space/differential interfaces, gradients, metrics, and related analysis are candidates for one canonical shared foundation after convention compatibility is proved.

Optimisation checkpoints

Chewi sampling §4.3 / Ch. 8 / Ch. 10 ↔ Chewi Optimisation

Convex analysis, proximal structure, mirror geometry, and stochastic-gradient primitives may be shared. Sampler kernels, invariant-law arguments, and route-specific source theorems remain separate.

Collision rule

Reuse → adapt → shared cell

Exact match → reuse. Near match → canonical core plus explicit adapter. Missing theorem needed by multiple routes → one shared Frontier Cell. Different theorem → keep separate.

ASTIS Harness · collaborative contract

One state machine, one shared Lean floor.

claimed→proved locally→independently verified→stabilized→merged

blocked→smaller child theorem→verified→re-entry

Before proving

Search and classify

Search Samplinglib, Mathlib, active shared cells, and relevant formal upstreams. Record reuse, adapt, missing, or out_of_scope before adding a declaration.

Shared lemma collision

One canonical shared cell

If two routes need the same missing lower-level theorem, record decision: new_canonical_shared, keep the route-local cell at claimed, and open/depend on one route: shared Frontier Cell. Parallel duplicate implementations are rejected by the protocol validator.

Integration

Single stabilization lane

Shared aggregators, root registries, duplicate API resolution, graph regeneration, and final root builds are serialized after independent verification.

Shared-foundation Frontier Cells

ASTIS-SHARED-strong-convex-gibbs-lsi-t2claimed

Finite-dimensional strongly convex Gibbs LSI and Talagrand T2 backend

For a normalized finite-dimensional Gibbs law with sufficiently regular alpha-strongly convex potential, construct the canonical log-Sobolev inequality with constant alpha and derive the matching Talagrand T2 inequality, with explicit probability, P2, RN-density, KL and relative-Fisher domains suitable for the restricted-Gaussian fiber consumer.

ASTIS-SHARED-canonical-fisher-transport-pairingproved locally

Canonical relative score paired with an optimal coupling

For a coupling gamma of finite-second-moment measures mu and nu, the pairing of gradient(logRatio mu pi)(x) with y-x is integrable whenever the existing smooth finite score domain holds. If gamma is quadratic-optimal, the absolute pairing integral is at most sqrt(information mu pi hscore) times wassersteinDistance mu nu toReal. Measurability, integrability and finite real cost identification are proved, not added as pairing premises.

ASTIS-SHARED-gaussian-precision-densityproved locally

Canonical exact volume density of a nondegenerate Gaussian with SPD precision

For every finite natural n and real SPD precision A, canonical multivariateGaussian zero A^-1 equals Euclidean volume.withDensity of the exact real sqrt(det A)/(2pi)^(n/2) exp(-xTAx/2). Includes dimension zero.

ASTIS-SHARED-gradient-ae-congruence-obstructionproved locally

Classical gradients are not invariant under arbitrary a.e. representative changes

Prove that there is no unrestricted rule sending f=g mu-a.e. to gradient f=gradient g mu-a.e. for arbitrary measures and classical Mathlib gradients.

ASTIS-SHARED-local-laplacian-productproved locally

One local-C2 Laplacian product rule for Poisson kernels and compact smooth graphs

Canonical local form of Eq1.19: for a finite-dimensional real inner product space \(E\), including dimensions zero and one, a point \(x\in E\), and real functions \(f,g\) which are C² locally at \(x\), the actual Laplacian and Riesz gradients satisfy \(\Delta(fg)(x)=f(x)\Delta g(x)+2\langle\nabla f(x),\nabla g(x)\rangle+g(x)\Delta f(x)\). The book states the real product rule for C² functions on their open domain in its standing dimension \(n>1\); the displayed canonical form localizes at one point and makes the low-dimensional extension explicit. It asserts no harmonicity or integral value.

ASTIS-SHARED-orthogonal-column-surface-lawproved locally

Canonical full orthogonal Haar column equals normalized Euclidean surface law

Canonical background expansion of the source uniform-sphere sentence: for every positive finite dimension \(n\) and every coordinate \(j\), let \(E=\mathbb R^n\), \(S=\{u:\|u\|_2=1\}\), and \(\mu\) be the actual normalized Haar probability on full \(O(n)\). Let \(\tau\) be the actual Euclidean-volume cone surface measure, \(\tau(B)=n\,\mathrm{vol}\{ru:0<r<1,u\in B\}\), and let \(\sigma=\tau(S)^{-1}\iota_*\tau\) on E. Then the actual pushforward \((O\mapsto Oe_j)_*\mu\) equals \(\sigma\). This explicitly generalizes the source use at its first coordinate with \(n\ge3\); it asserts no conditional residual law, independence, Poisson value, or lower bound.

ASTIS-SHARED-orthogonal-haarproved locally

The full orthogonal Haar probability is constructed by the actual Mathlib Haar measure normalized on the whole compact group, after existence and uniqueness are compiled and independently audited.

ASTIS-SHARED-orthogonal-haar-existsproved locally

For every natural finite n, the full real orthogonal group with inherited matrix topology and its Borel sigma-algebra has exactly one measure that is both Haar and a probability measure.

ASTIS-SHARED-orthogonal-haar-left-invarianceproved locally

For every natural finite n and every real orthogonal matrix Q, the actual orthogonal Haar probability is preserved under O->Q*O.

ASTIS-SHARED-orthogonal-haar-specproved locally

The constructed orthogonal Haar law is a probability Haar measure and every probability Haar measure on the same Borel space equals it.

+ 159 additional registered cells.

Open ASTIS Harness Protocol docs ↗ Claim a Frontier Cell ↗

Read the supporting proofs

Mathematical derivations with optional Lean and source details.

Complete declaration-by-declaration teaching coverage