import AutoSamplingTheory.TechnicalLemmas.Geometry.UnitSphereAngularCost import AutoSamplingTheory.TechnicalLemmas.InformationTheory.BoundedDensityPerturbation import AutoSamplingTheory.TechnicalLemmas.Geometry.QuadraticFeatureLawGradient import AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialDifferentiation import AutoSamplingTheory.TechnicalLemmas.Geometry.QuadraticFeatureTangentGradient import AutoSamplingTheory.TechnicalLemmas.Measure.BochnerMeanTransport import AutoSamplingTheory.TechnicalLemmas.Analysis.JointEmpiricalSegmentRisk import AutoSamplingTheory.TechnicalLemmas.Analysis.ProbabilitySegmentRisk import AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialAveraging import AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRisk import AutoSamplingTheory.TechnicalLemmas.Probability.GaussianPolynomialRidge import AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BoundedPerturbation import AutoSamplingTheory.TechnicalLemmas.Geometry.SphereRayleigh import AutoSamplingTheory.TechnicalLemmas.Geometry.SphereGradient import AutoSamplingTheory.TechnicalLemmas.Geometry.CurveExtension import AutoSamplingTheory.TechnicalLemmas.Geometry.AffineGradient import AutoSamplingTheory.Core import AutoSamplingTheory.TechnicalLemmas.Analysis.Integrability import AutoSamplingTheory.TechnicalLemmas.Analysis.SubgradientMethod import AutoSamplingTheory.TechnicalLemmas.Analysis.GradientAECongruence import AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrder import AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature import AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoPositiveWeights import AutoSamplingTheory.TechnicalLemmas.Analysis.HessianSecantOperator import AutoSamplingTheory.TechnicalLemmas.Analysis.MonotoneProximalMap import AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoMomentum import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Laplacian import AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Taylor import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Generator import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CanonicalLogSobolev import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.LogSobolev import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecay import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ForcedSemigroupDecay import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BakryEmeryInterpolation import AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinates import AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexity import AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavity import AutoSamplingTheory.TechnicalLemmas.Geometry.MetricCurve import AutoSamplingTheory.TechnicalLemmas.Geometry.StrongConvexity import AutoSamplingTheory.TechnicalLemmas.InformationTheory.DonskerVaradhan import AutoSamplingTheory.TechnicalLemmas.InformationTheory.KLDensity import AutoSamplingTheory.TechnicalLemmas.InformationTheory.Renyi import AutoSamplingTheory.TechnicalLemmas.InformationTheory.TiltedLogRatio import AutoSamplingTheory.TechnicalLemmas.InformationTheory.TiltedKL import AutoSamplingTheory.TechnicalLemmas.InformationTheory.QuadraticTiltFisher import AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinLipschitzMoment import AutoSamplingTheory.TechnicalLemmas.Measure.Gibbs import AutoSamplingTheory.TechnicalLemmas.Measure.GibbsIntegral import AutoSamplingTheory.TechnicalLemmas.Measure.GibbsLogConcavity import AutoSamplingTheory.TechnicalLemmas.Measure.KantorovichDual import AutoSamplingTheory.TechnicalLemmas.Measure.Product import AutoSamplingTheory.TechnicalLemmas.Measure.RadonNikodym import AutoSamplingTheory.TechnicalLemmas.Probability.ConditionalKernel import AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope import AutoSamplingTheory.TechnicalLemmas.Probability.KernelInvariance import AutoSamplingTheory.TechnicalLemmas.Probability.KernelL2 import AutoSamplingTheory.TechnicalLemmas.Probability.KernelRetainedReversibility import AutoSamplingTheory.TechnicalLemmas.Measure.Transport import AutoSamplingTheory.TechnicalLemmas.Probability.LawMap import AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNonaccumulation import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhysicalTimeCover import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhysicalTimeMeasurability import AutoSamplingTheory.ExampleCases.ProximalBPS.IdealHalfTurnKernel import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualSmallTimeContinuity import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedTestContinuity import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualOuterBoundedL2Continuity import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseTransitionKernel import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteFirstEventLaw import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteHistoryTailLaw import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualConditionalNextWaitSurvival import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualConditionalNextWaitDensity import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteHistoryExtension import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualAbsoluteNextEventTime import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualOrderedPrefix import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathDensity import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedPathExpansion import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseReversalVolume import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualEndpointTimeReversal import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedGibbsSurvival import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedStateReversal import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathReversal import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedWeightedDensity import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualWeightedSector import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseNormalization import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNormalizedEndpointSector import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCountableEndpointLaw import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedGibbsDuality import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2Expectation import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2FlipDuality import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPositionL2Averaging import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2StrongContinuity import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualKernelL2Realization import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHalfTurnReversibility import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualAugmentedKernelInvariance import AutoSamplingTheory.TechnicalLemmas.ProbabilityDistributions.Gaussian import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses /-! # Technical lemma memory registry The registry is the compiled Lean side of ASTIS technical lemma memory. It records which reusable lemmas exist locally, what upstream/source material motivated them, and which proof backend they support. -/ namespace AutoSamplingTheory namespace TechnicalLemmas inductive LemmaMemoryStatus where | formalizedLocal | portCandidate | sourceGap | referenceOnly deriving Repr, DecidableEq /-- Metadata for a lemma-memory entry. The executable proof is the declaration named in `localDecl`; this structure is only the retrieval record used by agents and documentation exports. -/ structure LemmaMemoryEntry where key : String localDecl : String upstreamDecl : String upstreamFile : String status : LemmaMemoryStatus tags : List String saldUse : String note : String deriving Repr, DecidableEq def sltSourceAnchor (file decl note : String) : SourceAnchor := sourceAnchor ("slt-" ++ file ++ "-" ++ decl) "externalLean" "https://github.com/YuanheZ/lean-stat-learning-theory" (file ++ ":" ++ decl) note def analysisMemory : List LemmaMemoryEntry := [ { key := "optlib-subgradient-norm", localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.SubgradientMethod.norm_le_of_supportsAt", upstreamDecl := "Lipschitz_to_bounded_subgradient", upstreamFile := "Optlib/Algorithm/SubgradientMethod.lean@5da27c5f95aa6a8a45b8c14b968ade4c13ff18c3:80-118", status := LemmaMemoryStatus.formalizedLocal, tags := ["convex", "subgradient", "Lipschitz", "optimisation"], saldUse := "Bounds supplied supporting vectors inside the actual subgradient energy estimate", note := "Native Lean 4.33.0 port over existing SupportsAt; no subgradient existence or random-oracle claim. Compilation, source review and integration are separately recorded." }, { key := "optlib-subgradient-energy", localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.SubgradientMethod.sum_weighted_gap_le", upstreamDecl := "subgradient_method_converge (extracted weighted intermediate)", upstreamFile := "Optlib/Algorithm/SubgradientMethod.lean@5da27c5f95aa6a8a45b8c14b968ade4c13ff18c3:171-232", status := LemmaMemoryStatus.formalizedLocal, tags := ["convex", "subgradient", "energy", "optimisation"], saldUse := "Actual update telescopes weighted gaps; consumed by the finite best-iterate theorem", note := "Retains the terminal distance. Nonnegative steps and empty horizon explicitly generalize the source intermediate; not a claim of full Optlib or Chewi chapter completion." }, { key := "optlib-subgradient-best", localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.SubgradientMethod.exists_gap_le", upstreamDecl := "subgradient_method_converge", upstreamFile := "Optlib/Algorithm/SubgradientMethod.lean@5da27c5f95aa6a8a45b8c14b968ade4c13ff18c3:137-232", status := LemmaMemoryStatus.formalizedLocal, tags := ["convex", "subgradient", "finite-horizon", "optimisation"], saldUse := "Finite best-iterate guarantee for a supplied nonsmooth subgradient run and arbitrary comparator", note := "Positive steps and nonempty horizon justify division. Native index witness replaces attained finite sInf; no minimizer, iterate convergence, stochastic oracle or sampling rate is claimed." }, { key := "quadratic-probability-segment", localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.ProbabilitySegmentRisk.quadratic_feature_probability_segment", upstreamDecl := "Original actual probability and Gaussian feature regularity supplement", upstreamFile := "Pinned Mathlib probability, Gaussian moments, L2 representatives and Bochner calculus", status := LemmaMemoryStatus.formalizedLocal, tags := ["probability", "L2", "risk", "shared"], saldUse := "Generic probability-law calculus and feature averaging; no model completion", note := "Actual two-probability-law endpoint calculus and integrable potential pairings. Independent fresh compilation and whole-module current-context semantic review accepted. Final root/reader gates and postmerge purification separate. No spatial gradient regularity, SDE or stochastic convergence claim." }, { key := "joint-empirical-segment-risk", localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.JointEmpiricalSegmentRisk.joint_empirical_probability_segment_derivative", upstreamDecl := "Original actual probability and Gaussian feature regularity supplement", upstreamFile := "Pinned Mathlib probability, Gaussian moments, L2 representatives and Bochner calculus", status := LemmaMemoryStatus.formalizedLocal, tags := ["probability", "L2", "risk", "shared"], saldUse := "Generic probability-law calculus and feature averaging; no model completion", note := "Actual joint empirical loss and endpoint derivative using only selected finite feature lists. Independent fresh compilation and whole-module current-context semantic review accepted. Final root/reader gates and postmerge purification separate. No spatial gradient regularity, SDE or stochastic convergence claim." }, { key := "analysis.quadratic-feature-risk-1", localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.empirical_squared_feature_risk_derivatives", upstreamDecl := "Samplinglib original quadratic feature-risk supplement v1, interface 1", upstreamFile := "AutoSamplingTheory/TechnicalLemmas/Analysis/QuadraticFeatureRisk.lean", status := LemmaMemoryStatus.formalizedLocal, tags := ["quadratic-risk", "empirical-measure", "L2", "optimisation"], saldUse := "Reusable squared-loss, genuine integral and indexed replacement calculations", note := "Compiled generic library interface. Exact hypotheses, actual integrals and remaining global-law boundaries are exposed in the authored lesson. Current public context-bound independent semantic reviews are accepted; serialized stabilization remains pending; no stochastic algorithm or model theorem is claimed." }, { key := "analysis.quadratic-feature-risk-2", localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.empirical_squared_risk_eq_L2_norm", upstreamDecl := "Samplinglib original quadratic feature-risk supplement v1, interface 2", upstreamFile := "AutoSamplingTheory/TechnicalLemmas/Analysis/QuadraticFeatureRisk.lean", status := LemmaMemoryStatus.formalizedLocal, tags := ["quadratic-risk", "empirical-measure", "L2", "optimisation"], saldUse := "Reusable squared-loss, genuine integral and indexed replacement calculations", note := "Compiled generic library interface. Exact hypotheses, actual integrals and remaining global-law boundaries are exposed in the authored lesson. Current public context-bound independent semantic reviews are accepted; serialized stabilization remains pending; no stochastic algorithm or model theorem is claimed." }, { key := "analysis.quadratic-feature-risk-3", localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.empirical_law_squared_risk_eq_L2_norm", upstreamDecl := "Samplinglib original quadratic feature-risk supplement v1, interface 3", upstreamFile := "AutoSamplingTheory/TechnicalLemmas/Analysis/QuadraticFeatureRisk.lean", status := LemmaMemoryStatus.formalizedLocal, tags := ["quadratic-risk", "empirical-measure", "L2", "optimisation"], saldUse := "Reusable squared-loss, genuine integral and indexed replacement calculations", note := "Compiled generic library interface. Exact hypotheses, actual integrals and remaining global-law boundaries are exposed in the authored lesson. Current public context-bound independent semantic reviews are accepted; serialized stabilization remains pending; no stochastic algorithm or model theorem is claimed." }, { key := "analysis.quadratic-feature-risk-4", localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.empirical_squared_loss_replacement", upstreamDecl := "Samplinglib original quadratic feature-risk supplement v1, interface 4", upstreamFile := "AutoSamplingTheory/TechnicalLemmas/Analysis/QuadraticFeatureRisk.lean", status := LemmaMemoryStatus.formalizedLocal, tags := ["quadratic-risk", "empirical-measure", "L2", "optimisation"], saldUse := "Reusable squared-loss, genuine integral and indexed replacement calculations", note := "Compiled generic library interface. Exact hypotheses, actual integrals and remaining global-law boundaries are exposed in the authored lesson. Current public context-bound independent semantic reviews are accepted; serialized stabilization remains pending; no stochastic algorithm or model theorem is claimed." }, { key := "analysis.quadratic-feature-risk-5", localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.quadratic_feature_mean_calculus", upstreamDecl := "Samplinglib original quadratic feature-risk supplement v1, interface 5", upstreamFile := "AutoSamplingTheory/TechnicalLemmas/Analysis/QuadraticFeatureRisk.lean", status := LemmaMemoryStatus.formalizedLocal, tags := ["quadratic-risk", "empirical-measure", "L2", "optimisation"], saldUse := "Reusable squared-loss, genuine integral and indexed replacement calculations", note := "Compiled generic library interface. Exact hypotheses, actual integrals and remaining global-law boundaries are exposed in the authored lesson. Current public context-bound independent semantic reviews are accepted; serialized stabilization remains pending; no stochastic algorithm or model theorem is claimed." }, { key := "analysis.quadratic-feature-risk-6", localDecl := "AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticFeatureRisk.joint_empirical_squared_risk_replacement", upstreamDecl := "Samplinglib original quadratic feature-risk supplement v1, interface 6", upstreamFile := "AutoSamplingTheory/TechnicalLemmas/Analysis/QuadraticFeatureRisk.lean", status := LemmaMemoryStatus.formalizedLocal, tags := ["quadratic-risk", "empirical-measure", "L2", "optimisation"], saldUse := "Reusable squared-loss, genuine integral and indexed replacement calculations", note := "Compiled generic library interface. Exact hypotheses, actual integrals and remaining global-law boundaries are exposed in the authored lesson. Current public context-bound independent semantic reviews are accepted; serialized stabilization remains pending; no stochastic algorithm or model theorem is claimed." }, { key := "pbps.actualAugmentedKernelInvariance" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualAugmentedKernelInvariance.actual_augmented_kernel_invariant" upstreamDecl := "Actual augmented PBPS one-step invariant kernel" upstreamFile := "arXiv2609.06905v1 Proposition3.4, equation3.11 and Algorithm2" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "kernel", "invariance", "conditional", "Tonelli"] saldUse := "Actual normalized augmented kernel for the planned PBPS Theorem3.5 convergence route; no SALD claim" note := "Independent source/compiler verification at6fbb3f42689e294cbb3f994fee26455baf4afef9; accepted audit ASTIS-RT-20261017-PBPSActualAugmentedKernelInvariance. Original six analytic inputs and exactly source fixed rho in(0,1). Retain the SAME literal actual Z/R/H and every-y conditional reversibility. Derive normalized Gibbs/augmentation probability and the same explicit conditional R, lift fiber invariance through measurable-section Tonelli, construct the fixed probability mixture and compose after Gaussian reflection to obtain exact eq3.11 and K.Invariant J. Three private declarations are implementation, not additional leaves. Exceptional-clock representative is justified parameterwise AE, not by a uniform null event. No process restart/semigroup, augmented all-L2 realization, hypocoercivity or convergence rate, implementation error/caps/actual cost, initialization/composition, PURIFIED or full-paper claim." }, { key := "pbps.actualHalfTurnReversibility" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHalfTurnReversibility.actual_half_turn_reversible" upstreamDecl := "Actual PBPS conditional half-turn detailed balance" upstreamFile := "arXiv2609.06905v1 Proposition3.2, A.1 bounded duality and A.2 independent-reference averaging" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "kernel", "reversibility", "Fubini", "conditional"] saldUse := "Actual augmented PBPS one-step invariance and half-turn operator consumer; no SALD claim" note := "Independent source/compiler verification atcffd16e6a5613cd924bee9dc18ab0af6e5f67a3f; accepted audit ASTIS-RT-20261017-PBPSActualHalfTurnReversibility. Under exactly the original six analytic binders, retain the SAME globally measurable actual returned-position kernel, raw process and local initialization outputs, and prove every-y all-measurable-rectangle detailed balance. Identify raw process witnesses, absorb momentum flips on position tests, derive finite signed Fubini and convert indicator pairings to ENNReal fluxes internally. Planned paper consumer: actual augmented one-step kernel in Proposition3.4. No temporal Markov/restart/semigroup, augmented all-L2 realization, hypocoercivity, simulation errors/caps, actual expected costs, warm start, composition or complete paper. Private adapters are not additional leaves." }, { key := "pbps.actualKernelL2Realization" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualKernelL2Realization.actual_kernel_l2_realization" upstreamDecl := "Actual PBPS invariant phase kernel and real-L2 realization" upstreamFile := "arXiv2609.06905v1 Appendix A.1 and Definition D.2, fixed-time observable realization only" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "L2", "kernel", "invariance", "representative"] saldUse := "Same-process PBPS transition/operator bridge; no SALD claim" note := "Independent source/compiler verification at52d523aca2aa825fa23d0fc997592b9128468bd2; accepted audit ASTIS-RT-20261016-PBPSActualKernelL2Realization. Original six analytic assumptions only. Identify the joint phase probability kernel with the SAME raw process Z using covered-arc/fallback equality, derive invariant fixed-parameter state fibers, and identify every canonical real-L2 representative with its kernel expectation AE, including fiber integrability. Derive AE order positivity and fixed real constant classes internally, retaining prior zero-time continuity, flip and Gaussian averaging. No process Markovness/restart, Chapman--Kolmogorov/semigroup, adjoint-density statement, independent-reference half-turn, hypocoercivity, simulation errors, actual expected cost, composition or complete paper." }, { key := "pbps.actualL2StrongContinuity" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2StrongContinuity.actual_l2_strong_continuity" upstreamDecl := "Actual PBPS real-L2 strong continuity at zero" upstreamFile := "arXiv2609.06905v1 Appendix A.1 Proposition A.1(ii), zero-time density argument only" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "L2", "strong-continuity", "dense-core"] saldUse := "Actual same-process PBPS semigroup prerequisite; no SALD claim" note := "Independent exact-commit verification eb5f3e75d062428f8ddb219d9dcd3caf56c799ae and accepted source-blind audit ASTIS-RT-20261015-PBPSActualL2StrongContinuity. Under the original six analytic assumptions, preserve the same actual Z, phase family A, flip J and Gaussian position averaging. Identify bounded-continuous-core representatives, prove their L2 norm-square zero-time limit using the actual clock law, then extend by bounded-continuous density and the closed locus of an equicontinuous contraction family. Every real L2 observable and rank0 included. This adds only zero-time strong continuity: no restart, Chapman--Kolmogorov, semigroup, positive-time continuity, kernel/L2 realization, positivity/constants, independent-reference averaging, hypocoercivity, simulation error, actual expected cost, composition or full-paper completion." }, { key := "pbps.actualPositionL2Averaging" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPositionL2Averaging.actual_position_l2_averaging" upstreamDecl := "Actual PBPS Gaussian momentum averaging and position L2 contraction" upstreamFile := "arXiv2609.06905v1 Appendix A.1(iii) final averaging proof" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "L2", "Gaussian-average", "self-adjoint"] saldUse := "Actual PBPS position averaging; no SALD claim" note := "Independent science 86e2da02b6b1a855916adcd46363e34d8a6ecb5b. Under the original six assumptions, retain the same108 global actual process Z, phase family A and canonical flip J. Construct the position lift B and Gaussian adjoint M=B*. For every arbitrary MemLp phase representative, derive Gaussian section integrability, output L2 membership and the literal Gaussian mean class. Prove JB=B and MJ=M, then K_T=M A_T B is selfadjoint, norm at most1 and K_0=id. Identify its literal Gaussian-outer clock-inner position expectation, with both nested AE integrability statements. Rank0 included. No new source premise. Markov positivity/constants, strong continuity, restart/semigroup, separate kernel witnesses, independent-reference averaging, hypocoercivity, errors, actual expected costs, composition and all four complete papers remain open." }, { key := "pbps.actualL2FlipDuality" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2FlipDuality.actual_l2_flip_duality" upstreamDecl := "Actual PBPS full real-L2 momentum-flip adjoint identity" upstreamFile := "arXiv2609.06905v1 Appendix A.1 Eq A.3 and density extension" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "L2", "adjoint", "momentum-flip"] saldUse := "Actual same-process full real-L2 flip duality; no SALD claim" note := "Independent science 25a3e47e3e171f2d5584a6568ce685c6f546e529. Under the original six assumptions, the same global actual PBPS process and the same real L2 expectation family from107 retain all path, Borel, Gibbs, bounded-duality, integrability, contraction and initialization conclusions. The canonical momentum-flip pullback J is an involutive L2 isometry and A_T.adjoint = J A_T J for every nonnegative T, on all real L2 classes. Gaussian reflection and product maps prove phase preservation. Bounded simple representatives give the signed pairing; continuity and two-variable density extend it to all L2, then adjoint uniqueness closes Eq A.3. No new source premise. Restart/Markov/semigroup, strong continuity, separate kernel witnesses, actual position averaging, hypocoercivity, errors, actual expected costs, composition and four complete papers remain open." }, { key := "pbps.actualL2Expectation" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2Expectation.actual_l2_expectation_contraction" upstreamDecl := "Actual PBPS L2 expectation contraction and zero-time identity" upstreamFile := "arXiv2609.06905v1 Appendix A.1 expectation operator and L2 domain toward Eq A.3" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "L2", "expectation", "contraction"] saldUse := "Actual same-process L2 expectation contraction; no SALD claim" note := "Independent science 2b657840a2f21c5d8001c83e4625a1ab13ef70ba. Under the original six assumptions, the same global jointly measurable actual PBPS Z retains live arcs, fallback, parameterwise initialization, Gibbs preservation and bounded flip duality. Every Borel test has a joint Borel total clock expectation; a uniform finite bound proves every section L1. For each y,r an internally constructed real L2 contraction family A_T realizes the literal clock expectation of every MemLp representative, with almost-everywhere section L1, output L2 membership, exact quotient identity, square-integral contraction and A_0=id. Actual106, normalization103 and UnitExponentialProduct are the three producers. Adjoint pullbacks, product L1, signed Fubini and indicator uniqueness are internal dependencies. Representative independence is a consequence of universal quotient identification; the planned direct-AE route remains an unselected alternative. Full L2 flip identity A.3, restart/Markov/semigroup, separate kernel witness identification, strong continuity, hypocoercivity, errors, actual expected costs, composition and all four papers remain open." }, { key := "pbps.actualBoundedGibbsDuality" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedGibbsDuality.actual_bounded_gibbs_duality" upstreamDecl := "Actual PBPS bounded signed Gibbs duality and fixed-time invariance" upstreamFile := "arXiv2609.06905v1 Appendix A.1 final bounded signed bilinear identity and Gibbs stationarity" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "Gibbs", "endpoint", "reversal"] saldUse := "Actual bounded duality and fixed-time invariance; no SALD claim" note := "Independent science edc917ec4c792bfe1308eee35a5d183c3768703c. Under the original six assumptions, one global jointly measurable actual PBPS process retains its exact arc/fallback/zero-time contract. For every y,r,T its endpoint pushes the actual Gibbs phase law times countable exponential clocks to the same Gibbs phase law. For every pair of bounded Borel real F,G, both outer tests are integrable and integral F op(G) equals integral (G composed R) op(F composed R). Actual105, actual normalization103 and UnitExponentialProduct are the three direct producers. Momentum symmetry and signed Fubini are internally discharged. The selected direct-marginal proof and printed F=1 route have separate independently admitted source graph alternatives. L2 operators/domains, restart/Markovness, separate kernel witness identification, hypocoercivity, errors, actual expected costs, full composition and all four full papers remain open." }, { key := "pbps.actualCountableEndpointLaw" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCountableEndpointLaw.actual_countable_endpoint_law" upstreamDecl := "Actual PBPS countable endpoint probability and reversal" upstreamFile := "arXiv2609.06905v1 Appendix A.1 A7 and nonnegative Gibbs averaging before A8" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "Gibbs", "endpoint", "reversal"] saldUse := "Actual countable endpoint law; no SALD claim" note := "Independent science a6060928c393d3efe4c85d4cab2b9af166ab6b37. Under the original six assumptions, one global jointly measurable actual clock process Z retains the exact arc/fallback/zero-time contract. For every y,r,T, its Gibbs-initialized endpoint law Q is the countable sum of all actual normalized fixed-count endpoint sectors, is a probability, and is preserved by J(z0,zT)=(RzT,Rz0). Actual93, normalization103, UnitExponentialProduct and sector reversal104 are the four direct producers. Fixed-initial measurable count fibers, jointly measurable sector integrals and nonnegative Tonelli close assembly without a joint-count premise or signed uniform domination. Signed bilinear duality, marginal phase invariance, restart/Markovness, hypocoercivity, implementation errors, expected costs, full composition and all four full papers remain open." }, { key := "pbps.actualNormalizedEndpointSector" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNormalizedEndpointSector.actual_normalized_endpoint_sector_reversal" upstreamDecl := "Actual normalized PBPS endpoint-pair sector reversal" upstreamFile := "arXiv2609.06905v1 Appendix A.1 fixed-count reversal and Eq3.1 averaging" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "Gibbs", "endpoint", "reversal"] saldUse := "Actual normalized endpoint-pair sector; no SALD claim" note := "Independent science 1a0fb58a061845fc5ac7623e4d62b5e301d7eb78. Under the original six assumptions and every y,r,n,T, the actual density q_n times terminal survival weights the product of the normalized phase law and strict-simplex measure. Its pushforward through B(z,t)=(z,Gamma(z,t)(T)) is preserved by J(z0,zT)=(RzT,Rz0). Four actual public parents supply finite-count density measurability, endpoint reversal, unnormalized weighted substitution and phase normalization. Same reversal witness, simplex sigma-finiteness and normalized-sector preservation are derived internally. No additional premise or claim that a fixed-count sector is a probability measure. Countable assembly, signed bilinear identity, process invariance, Markovness, hypocoercivity, errors, expected costs and whole-paper/composition remain open." }, { key := "pbps.actualPhaseNormalization" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseNormalization.actual_phase_gibbs_normalization" upstreamDecl := "Actual PBPS phase Gibbs normalization" upstreamFile := "arXiv2609.06905v1 conditional energy and Eq3.1" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "Gibbs", "normalization", "Gaussian"] saldUse := "Actual conditional position-momentum phase law; no SALD claim" note := "Independent science 030f4f70feb3641cafca981ee81c48a2687db1ee. Under the original six analytic assumptions, for every y the actual position Gibbs factor is integrable with positive Zx, and the phase partition is Zphase=ofReal(Zx*(sqrt(2*pi))^dim), positive and finite. The normalized phase withDensity is a probability measure exactly equal to the canonical tilted position law times stdGaussian momentum. Includes rank zero; no minimizer, critical point, normalizer or integrability premise. Existing shared Hessian, Gibbs tail, Gaussian integral/density and Gibbs normalization producers are consumed. Analytically independent of weighted sector102; both are parents only of later normalized averaging. No process invariance, countable assembly, Markovness, hypocoercivity, error, expected cost, main result or composition." }, { key := "pbps.actualWeightedSector" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualWeightedSector.actual_weighted_sector_lintegral" upstreamDecl := "Actual PBPS weighted finite-sector substitution" upstreamFile := "arXiv2609.06905v1 Eq3.1 and Appendix A1 A7/A8 sector substitution" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "weighted-sector", "reversal", "lintegral"] saldUse := "Actual finite PBPS weighted sector substitution; no SALD claim" note := "Independent science 320ad09ccfd3bc05a9ec3d909c9c19d236c9a232. Original six analytic assumptions and actual density rho=q*terminal survival. On the phase-first Lebesgue times strict-simplex measure mu, actual endpoint/time reversal Theta satisfies integral W(q)F(Theta(q)) dmu=integral W(q)F(q) dmu for every measurable ENNReal F, where W=ofReal(exp(-U))*rho. Three actual public parents93/97/101 supply joint density measurability, measure preservation and weight matching; all ingredients are derived internally. Explicit nonnegative-test extension permits infinite integrals and includes n=0,T=0,rank0,zero normals/rates. No normalization, invariant probability, Markovness, hypocoercivity, error, cost, main result or composition." }, { key := "pbps.actualPrescribedWeightedDensity" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedWeightedDensity.actual_prescribed_weighted_density_balance" upstreamDecl := "Actual PBPS weighted prescribed density matching" upstreamFile := "arXiv2609.06905v1 Eq3.1 and Appendix A1 A7/A8 weighted density" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "weighted-density", "reversal", "finite-path"] saldUse := "Actual finite PBPS weighted density matching; no SALD claim" note := "Independent science 4713623d3edbc5d258e563e8521271c316f0dc8c. Original six analytic assumptions and exact actual density rho=q*terminalweight. One reversed event-time map yields both w(z)dReal(z,t)=w(RA)dReal(RA,rho(t)) and ofReal(w(z))*rho(z,t)=ofReal(w(RA))*rho(RA,rho(t)). Four public actual parents94/98/99/100 discharge density bridge, Gibbs survival, incoming product and reflected survival. Includes n=0,T=0,rank0,zero normals/rates; no rate division. No weighted sector/integral invariance, normalized invariant probability, Markovness, hypocoercivity, errors, costs, main results or composition." }, { key := "pbps.actualPrescribedPathReversal" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathReversal.actual_prescribed_path_reversal_and_survival" upstreamDecl := "Actual PBPS path reversal and survival-integral substitution" upstreamFile := "arXiv2609.06905v1 Appendix A1 A8 off-event reversal and survival substitution" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "reversal", "survival", "finite-path"] saldUse := "Actual finite PBPS path reversal and survival substitution; no SALD claim" note := "Independent science d9850090b15210e29ecd9b932f02c358d2c9e786. Original six analytic assumptions and literal actual path definitions. On 0<=s<=T away from finitely many reversed event times, barGamma(s)=R Gamma(T-s). Both actual scalar rates are interval integrable and their survival integrals agree. Actual state reversal, path interpolation, harmonic flow, phase reversal and prescribed-density integrability discharge all private premises. Endpoints, n=0,T=0,rank0,zero normals/rates included. No genuine-jump pointwise equality, weighted density/sector, invariant probability, Markovness, hypocoercivity, errors, costs, main results or composition." }, { key := "pbps.actualPrescribedStateReversal" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedStateReversal.actual_prescribed_state_reversal_and_rate_product" upstreamDecl := "Actual PBPS finite-state reversal and incoming-rate product" upstreamFile := "arXiv2609.06905v1 Appendix A1 A5 and A8 finite incoming-state reversal" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "reversal", "incoming-rates", "finite-path"] saldUse := "Actual finite PBPS paired-state reversal and rate product; no SALD claim" note := "Independent science ce675a4cfad2d35cc8c4fec2c26979728742ac27. Original six analytic assumptions and actual path definitions. Reversing the strict event tuple gives barPost_j=R(arrive_(n-j)) and barArrive_j=R(post_(n-j)) on all n+1 arcs; products of the n incoming event rates agree. Actual phase reversal and endpoint laws discharge all private premises. Includes n=0,T=0,rank0,zero normals and rates. No all-time right-continuous path equality, survival time substitution, weighted density equality, invariant probability, Markovness, hypocoercivity, errors, expected costs, main results or composition." }, { key := "pbps.actualPrescribedGibbsSurvival" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedGibbsSurvival.actual_prescribed_gibbs_survival_balance" upstreamDecl := "Actual PBPS finite-path energy and Gibbs/survival balance" upstreamFile := "arXiv2609.06905v1 Appendix A1 A4 and its integrated Gibbs/survival identity" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "energy", "Gibbs", "survival", "finite-path"] saldUse := "Actual finite PBPS target-energy and survival balance; no SALD claim" note := "Independent science 530a58f7c036a67787956b20d2d390890ec2fec7. Under the original six analytic assumptions, both actual prescribed-path rate integrals are finite and U_y(A)-U_y(z)=Iplus-Iminus, hence exp(-U_y(z))*exp(-Iplus)=exp(-U_y(A))*exp(-Iminus). The reverse rate uses momentum reversal along the same path. Actual flow, bounce, finite-count path and endpoint laws discharge all private premises. Includes n=0,T=0,rank0,zero normals and zero rates. No reverse-event density matching, weighted Theta preservation, invariant probability, Markovness, hypocoercivity, errors, actual expected costs, main results or composition." }, { key := "pbps.actualEndpointTimeReversal" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualEndpointTimeReversal.actual_endpoint_time_reversal_laws" upstreamDecl := "Actual PBPS finite endpoint and event-time reversal" upstreamFile := "arXiv2609.06905v1 Appendix A1 endpoint/time substitution surrounding A8" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "endpoint", "simplex", "reversal", "volume"] saldUse := "Actual finite PBPS endpoint/time change of variables; no SALD claim" note := "Independent science 7089dfb0698c50d3ffd0180fb58d06bb32e5d7dd. Under the original six analytic assumptions, rho(t)_i=T-t_(n-1-i) is a measurable involution preserving exact strict-simplex comap volume m. A=Gamma(T) equals the final flow after the recursive post-bounce state, is jointly Borel and preserves phase volume ell for each event tuple. A(R A(z,t),rho t)=Rz. Theta(z,t)=(R A(z,t),rho t) is jointly Borel, involutive and preserves ell tensor m. Includes n=0, T=0, rank0 and zero normals. Actual OrderedPrefix, FiniteCountPath and PhaseReversalVolume supply dependencies internally. Gibbs-weight balance, stationary averaging/invariance, restart/Markovness, hypocoercivity, implementation errors, expected costs, main results and actual-input composition remain open." }, { key := "pbps.actualPhaseReversalVolume" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseReversalVolume.actual_phase_reversal_volume_laws" upstreamDecl := "Actual PBPS phase product-volume and reversal laws" upstreamFile := "arXiv2609.06905v1 Appendix A1 flow A5 A6 and elementary A8 mechanics" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "volume", "reflection", "reversal", "integrability"] saldUse := "Actual PBPS phase-volume changes of variables; no SALD claim" note := "Independent science 2f2e2c01856c902b07406db87026c50639454d71. Under the original six analytic assumptions, the literal harmonic flow, state-dependent bounce and momentum reversal preserve canonical phase product volume. Joint Borel maps, both flow inverses, bounce/reversal involutions, R Phi_u R=Phi_-u, R S=S R, rate(R S z)=rate(z), and the real integrable-test A6 identity are proved. Covers rank0, zero normals and all real times without an unscaled isometry claim. Volume and regularity are derived, not provider assumptions. Finite prescribed endpoint/time reversal, stationary averaging, invariance, Markovness, hypocoercivity, implementation errors, expected costs, main results and actual-input composition remain open." }, { key := "pbps.actualBoundedPathExpansion" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedPathExpansion.actual_bounded_path_functional_expansion" upstreamDecl := "Actual PBPS bounded real path functional expansion" upstreamFile := "arXiv2609.06905v1 Appendix A1 A7" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "path", "density", "integrability", "summation"] saldUse := "Actual PBPS bounded path expectations; no SALD claim" note := "Independent science 5df604f6c9ddab63e552272b2e9056752616621e. Under the six original analytic assumptions, the literal stopped-clock process satisfies the full A7 expectation expansion for every bounded real functional measurable for the coordinate-product path sigma algebra. Every weighted finite-simplex term is integrable and the signed component integrals are absolutely summable. Actual finite-count joint laws and the whole-path density identity are consumed internally. Covers n=0,T=0,rank0,zero rates and infinite waits. ASTIS uses countable probability-partition integration as an alternative to the printed rate-cap/factorial proof. No Skorokhod assertion, unbounded-test/cost transfer, restart/Markovness, invariance, hypocoercivity, implementation error, main result or actual-input composition completion." }, { key := "pbps.actualPrescribedPathDensity" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathDensity.actual_prescribed_path_density_rewrite" upstreamDecl := "Actual PBPS prescribed-path hazard and density identity" upstreamFile := "arXiv2609.06905v1 Appendix A1 A7 prescribed trajectory ingredient" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "path", "hazard", "left-limit", "density"] saldUse := "Finite PBPS prescribed-path density consumer; no SALD claim" note := "Independent science ad3b80a339bf1cf0dd88685f202632a92eeb0797. Under exactly the six original analytic assumptions and the literal actual93 prescribed interpolation, every finite strict event tuple has integrable path rate, an exact n+1-arc hazard integral sum, incoming phase and rate left limits, and rho=ofReal(exp(-whole-path hazard integral) times product of incoming jump rates). Terminal survival, n=0, T=0, rank0 and zero rates are retained. No additional path/integrability/limit provider. This deterministic ingredient does not yet compose the actual finite-count measure with the printed density or sum full A7. Restart/Markovness, invariance, hypocoercivity, implementation errors, expected cost, paper mains, actual-input composition and four-paper completion remain OPEN." }, { key := "pbps.actualFiniteCountPath" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath.actual_finite_count_path_law" upstreamDecl := "Actual PBPS finite-count complete-history and coordinate-path law" upstreamFile := "arXiv2609.06905v1 Appendix A1 A7 finite-count ingredient and Appendix A2" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "actual-input", "finite-count", "history", "path-law"] saldUse := "Actual PBPS finite path-law substrate; no SALD claim" note := "Independent science 8ec33d055fb8a9b3ba376d4113e388b00882026f. Six source analytic assumptions and actual stopped iid exponential-clock recursion unchanged. For every finite n and deterministic finite nonnegative horizon T, the unnormalized joint complete-history/coordinate-product-path law on N(T)=n is the pushforward of ordered-prefix density times terminal survival. One jointly measurable actual phase supplies pointwise interpolation on raw survived events, fixed-T endpoint nullity, measurable count, AE finite cardinalities, raw disjointness and full-probability union. All nonnegative tests measurable for the stated sigma algebras and count-sector mass identities are proved. No extra probability, density, measurability, nonexplosion or integrability provider. Hazard stitching, pre-jump left limits, infinite full A7, Skorokhod compatibility, restart/Markovness, invariance/hypocoercivity, errors/cost/main/composition/four-paper completion remain OPEN." }, { key := "pbps.actualOrderedPrefix" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualOrderedPrefix.actual_ordered_prefix_law" upstreamDecl := "Actual PBPS strict ordered-prefix complete-history law" upstreamFile := "arXiv2609.06905v1 Appendix A1 A1 A2 A7 finite iteration ingredient and Appendix A2" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "actual-input", "ordered-simplex", "finite-history", "density"] saldUse := "Actual PBPS finite path-law substrate; no SALD claim" note := "Independent science a4599f28131fcf91d6b0754003facbc46e23ad2e. With the six original analytic hypotheses, canonical iid Exp(1) product P and literal stopped recursion, every finite n and T>=0 has a strict ordered-prefix complete-history law. Delta_n(T) is the open ordered time simplex with actual subtype comap of product Lebesgue measure. K gives all n+1 live time/state records; q is the product of n pre-bounce rates and elapsed segment survivals. Derive joint Borel K/q, actual history/observer/guard measurability, nonnegative real product, pointwise full-history reconstruction, H_*(P restricted to B)=K_*(q m), all nonnegative extended Borel test identities and integral q=P(B)<=1. Covers n0/T0/rank0/stopped/top/zero-input boundaries without new density or integrability providers. No terminal survival: not an exactly-n count law or full A7. Terminal survival/path/count assembly, restart/Markovness, invariance/hypocoercivity/errors/unbounded costs/main/composition/four-paper Goal remain OPEN." }, { key := "pbps.actualAbsoluteNextEventTime" localDecl := "AutoSamplingTheory.ExampleCases.ProximalBPS.ActualAbsoluteNextEventTime.actual_absolute_next_event_time_law" upstreamDecl := "Actual PBPS next absolute-event-time law" upstreamFile := "arXiv2609.06905v1 Appendix A1 A1 A2 A7 coordinate ingredient and Appendix A2" status := LemmaMemoryStatus.formalizedLocal tags := ["PBPS", "actual-input", "absolute-time", "finite-history", "density"] saldUse := "Actual PBPS ordered event-time iteration substrate; no SALD claim" note := "Independent science d62f7b2c89e749953a36d8922124865a4651e55e. Under the six original analytic assumptions, actual U reads the next stopped/live record. For each deterministic depth and every Borel finite-valued history horizon b, derive Borel observers/absolute append, all-prefix preservation, strict event equality Brel=B, actual guarded U=a+wait and complete-history append. The actual old-history/U law restricted to B has density D(h,u)=1_(a(h) entry.status == LemmaMemoryStatus.formalizedLocal).length end TechnicalLemmas end AutoSamplingTheory