production module

`AutoSamplingTheory.RMFLD`

5 named declarations scanned from AutoSamplingTheory/RMFLD.lean.

Imports

AutoSamplingTheory.SDE

Imported by

AutoSamplingTheory

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

def AutoSamplingTheory.RMFLD.rmfldPaperRoot Partial Not mapped

No declaration docstring.

def rmfldPaperRoot : String := "/home/nitanda_sub/mark/repos/RMFLD/RMFLD_paper"

AutoSamplingTheory/RMFLD.lean:10published source at 0e31a3cda412

def AutoSamplingTheory.RMFLD.rmfldSource Partial Not mapped

No declaration docstring.

def rmfldSource : SourceAnchor :=
  localTexAnchor "rmfld-current" rmfldPaperRoot "RMFLD_paper"
    "Current exploratory RMFLD paper; use exploratoryProof mode and keep conjectural proof routes honest."

AutoSamplingTheory/RMFLD.lean:12published source at 0e31a3cda412

def AutoSamplingTheory.RMFLD.exploratorySeedLabels Partial Not mapped

No declaration docstring.

def exploratorySeedLabels : List String :=
  [
    "thm:general_RMFLD_finite_particle_convergence",
    "thm:SIM_main",
    "thm:finite_particle_postwarmup_convergence",
    "thm:main_theorem_ABCD",
    "thm:actual_expem_one_step_recursion_new"
  ]

AutoSamplingTheory/RMFLD.lean:16published source at 0e31a3cda412

def AutoSamplingTheory.RMFLD.rmfldExploratoryContract Partial Not mapped

No declaration docstring.

def rmfldExploratoryContract : TheoremContract where
  id := "ASTIS.RMFLD.exploratory_seed"
  title := "RMFLD exploratory proof-validation seed"
  mode := "exploratoryProof"
  source := rmfldSource
  targetLean := "AutoSamplingTheory/RMFLD.lean"
  statementSummary := "Index current RMFLD proof targets and maintain proof-route candidates without weakening the paper statements."
  proofStatus := ProofStatus.planned

AutoSamplingTheory/RMFLD.lean:25published source at 0e31a3cda412

def AutoSamplingTheory.RMFLD.rmfldProofDag Partial Not mapped

No declaration docstring.

def rmfldProofDag : List ProofDagBlock :=
  exploratorySeedLabels.map fun label => {
    id := "ASTIS.RMFLD." ++ label
    interface := "Build source-index, obligations, and candidate proof routes for `" ++ label ++ "`."
    source := rmfldSource
    targetLean := "AutoSamplingTheory/RMFLD.lean"
    status := ProofStatus.planned
  }

end RMFLD
end AutoSamplingTheory

AutoSamplingTheory/RMFLD.lean:34published source at 0e31a3cda412