test module

`Tests.ProximalBPSConditionalScoreDomain`

0 named declarations scanned from Tests/ProximalBPSConditionalScoreDomain.lean.

Imports

AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomain

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

Tests/ProximalBPSConditionalScoreDomain.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomain

-- Audit the complete curvature, moment and actual-kernel proof. The production
-- directional-score domain is the mathematical input to the pending Poincare
-- step; this axiom query is not a separate mathematical consumer.
#print axioms AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomain.conditional_curvature_and_score_domain