the written rule at CONTRIBUTING.md:103 says every MathFin/ file header is copyright + license + authors + short docstring + a ## Result section listing the public lemmas.
it lost to an exemplar file four times during the martingale-representation program: implementers were pointed at ItoIntegralCovariation.lean as the shape to copy, and that file has no ## Result section either. the cleanup pass found the move destination ItoIntegralProcessGeneral.lean was missing one too, so the drift predates the program.
a rule that only lives in prose loses to whatever file people are told to imitate. the fix is a presence check next to the existing @[expose] public section gate in tests/test_router.py, which catches exactly this class of "green build, silently wrong file" problem.
scope:
- assert every
MathFin/**/*.lean with a module header has a ## Result section in its module docstring
- allowlist anything genuinely exempt, with the reason inline
- expect a backlog of pre-existing violations; either fix them in the same pass or record the allowlist honestly
raised as [HIGH, cheap] in the 2026-08-07 values review. it has no issue because it is a tests/ change and fell outside that session's enumerated follow-ups.
the written rule at
CONTRIBUTING.md:103says everyMathFin/file header is copyright + license + authors + short docstring + a## Resultsection listing the public lemmas.it lost to an exemplar file four times during the martingale-representation program: implementers were pointed at
ItoIntegralCovariation.leanas the shape to copy, and that file has no## Resultsection either. the cleanup pass found the move destinationItoIntegralProcessGeneral.leanwas missing one too, so the drift predates the program.a rule that only lives in prose loses to whatever file people are told to imitate. the fix is a presence check next to the existing
@[expose] public sectiongate intests/test_router.py, which catches exactly this class of "green build, silently wrong file" problem.scope:
MathFin/**/*.leanwith amoduleheader has a## Resultsection in its module docstringraised as [HIGH, cheap] in the 2026-08-07 values review. it has no issue because it is a
tests/change and fell outside that session's enumerated follow-ups.