ASSUMPTION_REVIEW_BLOCK13.md
Machine Native Reasoning
ASSUMPTION_REVIEW_BLOCK13.md
1 # Core 7.4 assumption and source review
2
3 Source: `source/core_v0.2.tex:848–858`, Reviewed Core 0.2, proposition 7.4.
4
5 Primary mathematical verdict: **proved as written**, under its standard measurable probability interpretation. This is a review of the argument. Final kernel evidence is recorded separately.
6
7 | Obligation | Treatment |
8 |---|---|
9 | Actual selected false-acceptance event | The premise concerns that event, with candidate selection already incorporated. |
10 | Probability measure | Total mass one is explicit. |
11 | Event measurability | Explicit for each event used in the conditional-to-marginal bridge. |
12 | Pre-attempt information | Each conditioning measurable space lies below the ambient space. |
13 | Conditional validity | Almost-sure bound on Mathlib conditional expectation of the actual event indicator. |
14 | Deterministic budget | A real sequence independent of the outcome. |
15 | Nonnegative finite series | Nonnegativity and `Summable` are explicit. |
16 | Countable scope | Natural-indexed events, not a finite surrogate. |
17 | Stopped process | Event containment and measure monotonicity. Measurable gates give probability events. Arbitrary gates have the stated outer-measure interpretation. |
18 | Independence | Not assumed or needed. |
19 | Filtration monotonicity | Not needed for this implication once each conditional bound holds. |
20 | Evaluator calibration | External application obligation, not established here. |
21 | Adaptive random spending | Outside this deterministic-budget theorem. |
22 | Confidence conditional on retention | Not supplied by the stopped-event bound. |
23
24 Dependency chain: event measurability → integrable indicator → conditional-integral identity → marginal domination → countable subadditivity → summed deterministic budget. Stopping then uses event inclusion.
25
26 No source claim has been weakened to obtain a finite example. The real-series summability hypothesis spells out the finite-total premise already present in the source. No manuscript mathematical token was changed.
27
28 A separate read-only agent reconstructed the source proof and boundary cases before reviewing the new code. That offers a second reasoning pass in the same model family. It is not independent peer review or a second implementation of Lean's kernel. The code review and executable evidence must be assessed separately.