WIP: Import markovprocess

[Vilin97]

Import the complete production Lean development from https://github.com/scottnarmstrong/markovprocess at dbade0d12c4f84179441a9df7d7147df7a8bcaa0 into LeanPool.MarkovProcess. This preserves the substantive modules and proved solution bridges, including supporting results beyond the headline theorem.

This PR preserves the complete production import. Validation of the required module-system migration against Lean/Mathlib 4.34.0 is in progress. No checks or gate settings are changed.

• 250 upstream Lean files retained, plus directory indexes and the generated project card.
• Original author/license attribution is retained; project metadata records the pinned upstream source.
• Pending: warning-free targeted build, style and Lean linters, metadata and quality checks, axiom/environment audit, and independent review.

The omitted upstream files are duplicate open statement surfaces and non-production build/diagnostic harnesses:

• Audit/BrownianMotion/Challenge.lean — Independent duplicate open statement surface; proved statements are retained.
• Audit/BrownianMotion/Solution.lean — Diagnostic/audit harness; production declarations retained.
• Audit/BrownianMotion/SolutionBasic.lean — Diagnostic/audit harness; production declarations retained.
• Audit/ContinuousMarkovProcess/Challenge.lean — Independent duplicate open statement surface; proved statements are retained.
• Audit/ContinuousMarkovProcess/Solution.lean — Diagnostic/audit harness; production declarations retained.
• Audit/ContinuousMarkovProcess/SolutionBasic.lean — Diagnostic/audit harness; production declarations retained.
• docs/ConsumerGuide.lean — Documentation consumer examples or documentation build module.
• lakefile.lean — Lake configuration.

Before the module-system migration, GitHub pool, project, documentation, metadata, and content-separation checks passed at 771190e64c. Independent review remains pending.

Current checkpoint 75775e2b7 preserves all 266 Lean files and passes recursive source/header/file/proof-size checks. It repairs the instance and data visibility boundaries reported by CI, including the public finite-time kernels, one-point resolvent, time reindexing and exhaustion metric. Private proof lemmas remain inside proposition-valued proof blocks. Fresh exact-head compilation and final declaration/style/index/metadata/axiom/environment checks, aggregate CI and independent review remain pending.

The existing ready-for-review state is preserved. Do not merge.

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.

[Vilin97]

Automation disposition: needs-maintainer

Reviewed exact head 771190e64c61056d0478c5087feea9e1155335cf for this draft pooled-project/content import, WIP: Import markovprocess. The changed tree is a substantial source import (for example LeanPool/MarkovProcess.lean) with the pinned upstream source, project metadata, and generated index present. Observed exact-head required checks have no failures; profile evidence is not posted for this head.

No concrete author-actionable defect was established in this bounded review that would justify an ordinary change request. The PR is still marked draft, so protected merge is not permitted. Maintainer decision required: confirm the headline result's significance, faithfulness, novelty, source/provenance and scope, then ask the author to mark the PR ready (or give scope direction). This is a maintainer disposition, not an approval.

[Vilin97]

/review

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Low risk] Adds a new mathematical library module for Markov processes.

Do not merge yet: the exact-head validation and independent review identified in the PR remain pending.

Summary

The PR imports the Markov-process formalization, its project entry points, and catalog record. Since the previous review, the only change is a proof refactor in FiveEighthsTheorem; no new actionable issue was established. Exact-head build, audit, and independent review remain pending.

_{Reviews (16) · Last reviewed commit: "Merge remote-tracking branch 'origin/mai..."}

[Vilin97]

🤖 LLM review (gpt-6-astra, 5 rubrics)

Reviewed head: 6a555676c88c970df308f9c1ccae7274adcd7ccf

Verdict: ✅ approve — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	The headline proves the card’s claimed existence and uniqueness without assuming the continuous-path construction.
Novelty	✅ pass	Independent searches of pinned Mathlib and the existing pool found no duplicate of MarkovProcess.existsUnique_continuousProcess.
Significance	✅ pass	This is a substantial, coherent graduate-level probability development with clear headline results and no evident generated-bulk maintenance burden.
Sources	✅ pass	The pinned upstream source states the advertised theorem with matching hypotheses, and the import explicitly credits the prior formalization.
Code quality (advisory)	✅ pass	The code is competently organized around reusable kernel, semigroup, and path APIs; no material maintainability issue warrants a finding.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	A jointly measurable conservative Feller transition semigroup on a nonempty locally compact complete separable metric space with its Borel sigma-algebra, and a uniform displacement-moment bound with p > 0, q > 1 and finite M for every time increment and starting point; these match the card’s stated assumptions. Continuous-path regularity is derived from this bound, and the heat-semigroup example witnesses the hypotheses.
Matches cited source	✅ matches
Fit	✅ good_fit
Level	graduate
Branch	probability and stochastic processes
Mode	theory_building
Code quality	3 / 5

Statement check: MarkovProcess.existsUnique_continuousProcess proves existence and uniqueness of a probability kernel into continuous paths whose evaluations at every finite set of nonnegative real times equal the iterated transition laws.

The project constructs the unique continuous-path process associated with a conservative Feller semigroup satisfying Kolmogorov moment bounds, and develops strong Markov properties, Brownian motion, Yosida generation, and Trotter–Kato convergence.

---

Tokens: 4,273,837 in / 32,187 out across 5 model calls · Tier: codex-subscription · Effort: xhigh · Billing: Codex subscription quota (no API credits) · Estimated cost: $87.8908 (Standard API equivalent; uncached input)
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

Changes requested by automated review

Reviewed exact current head 2e410f117f1e909a7fc4d71f31b1b81e411c7d69.

The exact-head Build pool/project checks fail in the MarkovProcess import after the module-system migration. In addition, Greptile's current-head P1 finding is material: the card claims an independent comparator audit but the cited Audit/ContinuousMarkovProcess/comparator.json artifact is absent. Port the closure, either add the claimed audit evidence or remove that claim, regenerate the index, and rerun all gates.

Acceptance condition: repair the named defect on a new head and make all required protected checks green. Do not change repository policy or add waivers.

[Vilin97]

Changes requested by automated review

Reviewed head 5d36a8f9724eef15d47fe45b579bfa43e55de8b6. Substantial Feller/conservative semigroup construction under the stated moment bounds.

1. Complete the pinned-toolchain integration. The exact-head build fails. Its concrete error includes:

   error: LeanPool.lean:1:0: cannot import non-`module` LeanPool.MarkovProcess from `module`
   

   The file/dependency audit finds 266 changed Lean files without the required module form. Repair the affected dependency closure, regenerate the module index, and obtain a warning-free full pool build plus the unchanged linter, quality and axiom gates. A project-only or previous-head build does not resolve this failure.

2. Resolve the substantive source/interface defect. The card asserts a comparator audit at Audit/ContinuousMarkovProcess/comparator.json, but that artifact is not in this import. Link a verifiable upstream audit at the pinned revision or remove the unsupported certification claim; do not present it as pool CI evidence.

Review coverage: complete changed-file inventory and full diff retained; 266 changed project files, 47,671 lines, import reachability and executable trust-token scan; advertised endpoints and supporting definitions examined with bounded implementation sampling and existing review findings reconciled. Potential reusable value: Kernel, filtration and continuous-modification infrastructure. Source/provenance and prior-art evidence were considered separately from CI; these findings do not assert that every proof line was manually read. Earlier automated scores are advisory and are not approval of this failing head.

[Vilin97]

{
"reviewed_head": "5c38e7be7af67592b763dcfa0b074a7a1754336e",
"scope": "Resolution of unsupported audit prose only",
"finding_resolved": "The summary no longer claims that the imported theorem was independently checked using the absent Audit/ContinuousMarkovProcess/comparator.json. The mathematical description, hypotheses, source pin, provenance and all Lean files remain unchanged.",
"validation": "Parsed registry comparison proves that removing this one sentence is the sole metadata change. Required-field, value and generated-card checks and git diff --check pass. No compiler or linter settings changed.",
"remaining_work": "This comment does not approve the unfinished module migration or certify an external comparator run. Final-head integration and CI remain with the module-repair owner and maintainer."
}

[Vilin97]

Published the reviewed helper-sharing repair at 58d30282ff90c105ac1f3ddaa5c4f378b67ea390, preserving the incoming module-boundary repairs through 75775e2b7 and current main.

The new finite-product measure module supplies the existing coordinate-polynomial integrability and measurability proofs to six consumers. Kernel operator proofs reuse the existing almost-everywhere fiber-integrability lemmas; deletion/concatenation reuse the existing product-kernel reindex identities. Existing public theorem statements and mathematical hypotheses are retained. Two independent source reads found no weakening of the Feller/Kolmogorov construction or its Brownian example. The four newer importer files contain proposition proof wrappers and one helper visibility change; their complete contents are preserved.

Validation completed: scoped source/header/size checks, acyclic project import graph, unchanged existing public headers, all 218 current-main project cards plus this project's complete card, and the actual mk_all --module --check command. The scoped compiler/linter/API-axiom check is still queued behind the shared VM build lock; fresh CI is pending. This review does not claim a successful full build, compiled trust audit, or final acceptance. The duplicate-helper finding is addressed in source; keep final validation and merge pending until the current checks pass.

[Vilin97]

Focused validation for 58d30282ff90c105ac1f3ddaa5c4f378b67ea390 has now passed. Recommendation: accept once the complete current required CI and current-main integration pass.

All 25 changed/necessary prerequisite modules compiled without warnings under the unchanged repository options. Four scoped declaration-linter batches and four scoped style batches passed, as did the actual generated-index check. An importing-module probe checked all six newly shared public helpers; each proof closure uses only propext, Classical.choice, and Quot.sound.

This completes validation of the helper-sharing repair described in the preceding review. The prior positive mathematical assessment carries forward across the reviewed module-port changes, with the same Feller/Kolmogorov assumptions and continuous-path law conclusions. The duplicate polynomial-measure and kernel-integration proofs are now shared without changing existing public statements. The earlier unsupported local-comparator claim remains removed.

The local check was scoped to the affected dependency closure; it was not a full-project rebuild or whole-pool linter. Fresh complete CI remains required, and main has advanced by the separately merged attribution-only PR #531.

[Vilin97]

Reviewed current head 6a555676c88c970df308f9c1ccae7274adcd7ccf after the normal merge of main 0e9b057b.

The only delta from the validated revision is the main-branch attribution update in NOTICE and NOTICE.extra.yml. All Lean source, project cards, dependency pins and checks remain byte-identical. The actual pinned mk_all --module --check passes.

The completed focused compilation, linter and trust checks and prior source review therefore carry forward. Acceptance remains conditional on the fresh required CI checks for this head; no redundant local compilation was launched.

[Vilin97]

Daily disposition: needs maintainer — protected merge operation

Reviewed exact head bb8c4fc1ef417d9eaf33b5be8c151825f0b7fafd. The continuous-path Markov kernel is constructed uniquely for conservative Feller semigroups on nonempty locally compact Polish spaces under the explicit Kolmogorov bound. The unsupported audit-artifact assertion has been removed. The layered kernel/filtration API has concrete downstream consumers; the old numeric 3/5 had no residual actionable quality finding. The complete source/dependency review and recovered repairs were reconciled through the lossless main integration; fresh protected CI remains the integration authority.

Build project: pending/not yet reported, Content / non-content separation: SUCCESS, Documentation preflight: SUCCESS. These are observed check states, not an assertion that unfinished checks passed.

The remaining authority boundary is operational: this repository has allow_auto_merge=false, and GitHub rejected enablePullRequestAutoMerge with “Auto merge is not allowed for this repository.” The maintainer must make protected queuing available through an authorized repository-setting decision, or remove this label and perform a normal squash merge after the required checks and current-base integration pass. This cycle does not change repository settings or bypass protection. No unresolved substantive author-actionable finding justifies another change request or closure; the label is not for draft status, missing profiling, or an old advisory score.