AutoSamplingTheory.SALD.guidedResidualIdentityContract

Data definition / provenance and workflow record

Meaning and type

The result has data type AutoSamplingTheory.SALD.GuidedResidualIdentityContract. A value of this type stores descriptions; it is not a proof of the statements in those descriptions.

def guidedResidualIdentityContract : GuidedResidualIdentityContract

Construction and field-by-field explanation

Construct a data record from explicit fields and the audited defaults shown below.

This Lean definition constructs provenance or workflow data. It does not prove the mathematical statements stored as text. Status labels, named dependencies and citations are data, not compilation, proof or source certificates.

sourceStatement : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldGuidedResidualSource — audited data reference, not expanded and not a compiled dependency edge

sourceProof : AutoSamplingTheory.SourceAnchor (explicit)

Nested provenance data.

AutoSamplingTheory.SALD.saldGuidedResidualProofSource — audited data reference, not expanded and not a compiled dependency edge

basePath : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

p_t has transport velocity u_t: partial_t p_t + div(p_t*u_t)=0.

guideTilt : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

Z_t=int p_t(x)*exp(-f_t(x)) dx and pi_t(x)=Z_t^(-1)*p_t(x)*exp(-f_t(x)).

guideTransportDerivative : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

g_t(x)=partial_t f_t(x)+nabla f_t(x)^T*u_t(x).

normalizerDerivative : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

dot Z_t/Z_t = -E_{pi_t}[g_t], obtained by differentiating Z_t and integrating div(p_t*u_t)*exp(-f_t) by parts.

residualIdentity : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

partial_t pi_t + div(pi_t*u_t) = -pi_t*(g_t-E_{pi_t}[g_t]).

meanZeroStatement : String (explicit)

Descriptive text even when field names say formula, theorem, inequality, derivative, source gap, or proof.

int (g_t-E_{pi_t}[g_t]) * pi_t dx = 0.

requiredRegularity : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. differentiability of t -> p_t, f_t, and Z_t
2. positive finite normalizer Z_t
3. transport equation for p_t with velocity u_t
4. integration-by-parts or boundary decay for div(p_t*u_t)*exp(-f_t)
5. integrability of g_t under pi_t

sourceGaps : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. the source proof uses differentiation under the integral for Z_t and pi_t without an explicit dominated-convergence hypothesis
2. boundary conditions for the integration-by-parts step are implicit
3. positivity and finiteness of Z_t are used as part of the guided-density vocabulary

dependencies : List String (explicit)

Ordered descriptive/naming checklist, not logical conjunction or compiler dependency list.

Ordered data items

1. TransportVelocityContract
2. GuidedTiltContract

status : AutoSamplingTheory.ProofStatus (explicit)

Stored workflow tag; honor the exact default but do not infer mathematical certification.

AutoSamplingTheory.ProofStatus.obligation — stored label only; no proof certification

def guidedResidualIdentityContract : GuidedResidualIdentityContract where
  sourceStatement := saldGuidedResidualSource
  sourceProof := saldGuidedResidualProofSource
  basePath := "p_t has transport velocity u_t: partial_t p_t + div(p_t*u_t)=0."
  guideTilt := "Z_t=int p_t(x)*exp(-f_t(x)) dx and pi_t(x)=Z_t^(-1)*p_t(x)*exp(-f_t(x))."
  guideTransportDerivative := "g_t(x)=partial_t f_t(x)+nabla f_t(x)^T*u_t(x)."
  normalizerDerivative := "dot Z_t/Z_t = -E_{pi_t}[g_t], obtained by differentiating Z_t and integrating div(p_t*u_t)*exp(-f_t) by parts."
  residualIdentity := "partial_t pi_t + div(pi_t*u_t) = -pi_t*(g_t-E_{pi_t}[g_t])."
  meanZeroStatement := "int (g_t-E_{pi_t}[g_t]) * pi_t dx = 0."
  requiredRegularity := [
    "differentiability of t -> p_t, f_t, and Z_t",
    "positive finite normalizer Z_t",
    "transport equation for p_t with velocity u_t",
    "integration-by-parts or boundary decay for div(p_t*u_t)*exp(-f_t)",
    "integrability of g_t under pi_t"
  ]
  sourceGaps := [
    "the source proof uses differentiation under the integral for Z_t and pi_t without an explicit dominated-convergence hypothesis",
    "boundary conditions for the integration-by-parts step are implicit",
    "positivity and finiteness of Z_t are used as part of the guided-density vocabulary"
  ]
  dependencies := [
    "TransportVelocityContract",
    "GuidedTiltContract"
  ]
  status := ProofStatus.obligation