Drop the spurious `s 0 = 0` hypothesis from `stepDoleans_sub_one_mem_range`

[raphaelrrcoelho]

context

MathFin/Foundations/DoleansStepRepresentation.lean:362:

theorem stepDoleans_sub_one_mem_range (hBmeas : ∀ t, Measurable (B t))
    ...
    (_hs0 : s 0 = 0) (hsN : s N = T) :

_hs0 is genuinely unused. it was underscored during the program to clear a lake lint unused-argument
error, and underscoring silenced the linter without addressing that the theorem does not need the
hypothesis. the shipped statement is therefore weaker than what is proved.

this is the same class as the spurious-guard finding of 2026-07-31, recorded at docs/patterns.md:1031:
used-by-this-proof is not needed-by-this-theorem, and no gate catches the difference. an underscored
binder type-checks exactly as happily as a load-bearing one.

it was correctly out of scope for the task-6b cleanup pass, which was behaviour-preserving only. this is
a statement change.

task

drop _hs0 from the signature. re-prove. update the one call site
(Foundations/MartingaleRepresentation.lean:142) and the docstring at :74.

check the neighbouring binders while there: hsN : s N = T is used, but the same underscore-instead-of-
drop reflex may have been applied elsewhere in the program's four modules.

acceptance criteria

• _hs0 gone from the signature, not renamed.
• the call site in MartingaleRepresentation.lean updated and the file still builds.
• lake build MathFin && lake lint green; ledger re-verified for the entries importing these
  modules.

pointers

• MathFin/Foundations/DoleansStepRepresentation.lean:359-362,
  Foundations/MartingaleRepresentation.lean:142.
• docs/patterns.md:1031 for the guard rule this is an instance of.