Underlying Lean Graph of Libraries

Reuse a branch

A thin assembly adds a consumer edge, not a duplicate proof.

Close a leaf

A new analytic lemma discharges an open interface.

Add topology

A proof connects branches that were previously formalized only in isolation.

Expose a gap

An unknown matching theorem stays visible; ASTIS never invents a source statement.

Theorem Fidelity Checker

Original theorem → Lean → blind reconstructed theorem is compared slot by slot, not by wording.

Lean Theorem Denoiser

Source repair proposals stay separate from the pinned theorem until independent review accepts the exact repair.

Conceptual Mirror Audit

A recurring mechanism is retained under stable family/bridge ids, with translated hypotheses and a failure boundary, without becoming a Lean theorem edge.

Overview Graph

Where are the source libraries, shared prerequisite stages, and active frontier families?

Lean Branches Graph

Which declarations and modules are present, with what compiled evidence and reference signals?

Functor Hypergraph

Which mathematical ideas recur across fields, what hypotheses are translated, and where does the analogy stop?

Transport control → proxy warmness → high accuracy

A nearby Renyi-warm witness is enough for accuracy under the same implemented probability kernel; expected cost requires a different, actual-input bound.

Do not conflate: W2 proximity is not Renyi warmness; the actual law is not its proxy; TV closeness alone does not transfer unbounded costs.

Reflection coupling and discrete modified-L2 decay

Use a conditional-expectation projection to separate macro and micro modes. An involution couples them; a half-turn estimate and corrected energy propagate microscopic damping to macroscopic control.

Do not conflate: The conditional PDMP, discrete augmented chain, and continuous-time Langevin theorem have different operators and domains. Reuse requires adapters, not renaming a generator.

Metric gradient flow → dissipation → exponential decay

The state space changes, but the same proof skeleton can survive: choose an energy and a metric, identify its metric gradient, write energy dissipation, then use a PL-shaped inequality to turn dissipation into exponential convergence.

Do not conflate: Wasserstein/Otto calculus needs rigorous first-variation and flow hypotheses; W2 is not globally a classical smooth finite-dimensional Riemannian manifold.

Second-order curvature → first-order/growth controls

Strong convexity is not merely a faster convergence assumption. It is a lower-curvature statement that produces a quadratic lower model and, after the right geometry is chosen, often yields growth or PL-like coercivity.

Compiled substrates

• AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder
  Compiled Euclidean first-order quadratic lower model produced by strong convexity. Bound only to transport:curvature-growth. This module is a substrate for the Euclidean curvature-to-growth pattern only. It does not certify Riemannian, Wasserstein, Bakry-Emery, PL, Poincare, or LSI arrows.

Do not conflate: Euclidean Hessian bounds, geodesic convexity, displacement convexity, and Bakry-Emery curvature are related patterns but not interchangeable hypotheses.

PL / LSI mirror: objective gap versus gradient dissipation

Optimization PL bounds the objective gap by a squared gradient. For Langevin, LSI bounds KL by relative Fisher information, which is the squared Wasserstein gradient norm of KL in the smooth formal picture. Both turn the same dissipation identity into exponential gap decay.

Do not conflate: LSI is a functional inequality for measures/densities, not literally the Euclidean PL theorem; constants and factors of two depend on normalization.

Poincare / chi-square mirror: quadratic gap versus Dirichlet dissipation

For density ratio rho, chi-square is the squared L2 distance of rho from 1. Poincare controls this quadratic gap by Dirichlet energy, and reversible semigroup dissipation then gives exponential chi-square decay.

Do not conflate: Poincare/chi-square and LSI/KL are parallel dissipation templates but different inequalities and generally different strengths.

Quadratic regularization: proximal minimizer or Gibbs draw

Optimization and sampling can consume the same regularized energy differently: one chooses its minimizer, the other samples from its normalized exponential.

Do not conflate: Sharing an energy does not make the proximal map and restricted Gaussian oracle equivalent outputs.

Conditional influence and local-to-global mixing

Control dependence under all feasible pinnings, then lift local spectral or factorization bounds to a global sampler. Reuse matrix/probability algebra without identifying this condition with strong convexity.

Do not conflate: One covariance matrix is not spectral independence; neither is Euclidean strong convexity or generating-polynomial log-concavity without a proved bridge.

Target-invariance correction

Construct a target-invariant transition from a proposal; density and finite-state adapters share one accepted-flux idea.

Do not conflate: No mixing theorem or universal efficiency improvement.

High-dimensional scaling and diffusion limits

Transport the analysis only through a proved asymptotic limit with its own clock.

Do not conflate: Weak convergence is not finite-time uniform mixing.

Augmented state and marginal invariance

Prove invariance on an enlarged space and recover the desired marginal.

Do not conflate: HMC is not always nonreversible; geometry must preserve volume conventions.

Ideal versus implemented Markov kernels

Keep perturbation error and ideal mixing as separately proved terms.

Do not conflate: Fixed-step numerical samplers can retain a target bias.