Reader route · verification
Audit the claim, theorem, and dependency separately.
FormalSLT treats public prose as a map to checked declarations, not as a substitute for them. This route makes the proof boundary and publication boundary explicit.
Claim contract
- Proved
- A theorem elaborated by Lean in the referenced build.
- Proved composition
- A proved public capstone composed from checked mechanisms, with its assumptions still visible in the theorem type. This is a proof-role description, not a literature-fidelity label.
- Conditional
- A public application claim that materially relies on a supplied certificate or explicitly unproved proposition, not merely an ordinary theorem hypothesis.
- Open
- A generalization or desired endpoint that is not claimed as complete.
- Literature fidelity
REPRODUCTION,SPECIALIZATION, andDERIVED VARIANTare tracked independently in the literature ledger.
A compiled finite checker, numerical receipt, or polished paper is evidence for its own proposition only. None is silently promoted to theorem closure, novelty, or a public release.
Audit sequence
- Open the exact endpoint in generated documentation.
- Read every explicit argument and inherited typeclass assumption.
- Follow the source link pinned to the commit in this deployment.
- Check the example receipt containing
#checkand#print axioms. - Separate theorem status from release, paper, and prior-art status.
The public capstone axiom audit is intended to report only propext, Classical.choice, and Quot.sound. That profile concerns logical dependencies; it does not remove the mathematical premises in a theorem type.
Pressure points
- Simultaneous is not automatically sequential
The IID endpoint shares an event across sample sizes, but its proof route and claim are distinct from the forward e-process endpoint.
- Finite joint posterior is already checked
Model and strategy posterior PMFs may be selected after the path on the common event. This does not yet provide a computable evaluator, a countably supported strategy posterior, or automatic competition with all legal strategies.
- Strategy selection retains a fixed-catalog boundary
The countable mixture weights and legal predictable strategies are fixed before observation. The common event allows later atom selection with an explicit weight cost; it does not validate a strategy invented after seeing its scored outcome.
- The observable oracle has monitored-risk semantics
The selected finite-state bound concerns posterior-averaged conditional loss along the observed trajectory. It is not a stationary, future, or deployment-risk theorem without a separate bridge.
- Adaptive selection has a catalog boundary
Posterior and atom selection occur within a common event; new score families learned from outcomes are outside this endpoint.
- Stationarity uses explicit contraction data
The finite-depth correction assumes a known finite-state kernel, invariant PMF, and oscillation bound.
- Invariant-law uniqueness is conditional
Finite-state existence supplies a canonical invariant PMF. Uniqueness follows only if the selected transferred contraction coefficient is strictly below one.
Next step
Use the exact source, not a floating branch.
The deployed theorem index rewrites every source location to the full commit SHA that generated this site.