ASSUMPTION_REVIEW_BLOCK07.md
Machine Native Reasoning
ASSUMPTION_REVIEW_BLOCK07.md
1 # Block07 — assumption and statement review
2
3 **Source:** Reviewed Core0.2, Core5.1, unchanged printed pages17–18.
4
5 | Obligation | Formal location and reviewed boundary |
6 |---|---|
7 | Finite choices | Finite experiment, report, artifact and resource-coordinate types are explicit. State uncertainty is a finite support. No finite menu is inferred from unrestricted program expressibility. |
8 | Nonempty state support | `Allowed`, `Terminal`, `valid_nonempty`. An empty support is not success by vacuous acceptance. |
9 | Uniform admissibility | A single root experiment is permitted in every currently possible state. Its guards do not select a different experiment using a hidden state. |
10 | Actual state effects | `update`, `mem_update`, `actual_next_mem`. Support is an image of pre-report candidates under the actual transition. An origin target needs an immutable tag. |
11 | Report/branch agreement | `Valid`, `valid_child`. A possible report needs a valid child. An impossible report has no stored child. An empty child frontier prevents success through that root. |
12 | Fixed audience | `AudienceBridge.attach`, `sensor_accept_iff`. Installed recipient procedures, permission, outcome flags and local limits are not relaxed by inquiry synthesis. |
13 | Terminal resource charge | `terminalCost` is the declared componentwise charge. `ChargesBounded` transfers an upper bound to primitive executions. `ExactCharges` adds exact worst-case attainment. |
14 | All online coordinates | `Profile` has the product order. Maximum is componentwise. Different coordinates may be attained on different branches, but all bounds refer to the same tree. |
15 | Complete storage | One stored record for each query and terminal node. Sum over all present children, not maximum, expected count, or selected-path count. Not a byte or DAG-storage optimum. |
16 | Pareto reduction | Finite minimal-element existence plus monotone composition. Every retained profile has a witness, and every valid profile is dominated by a retained one. No independent-coordinate optimizer supplies a fictitious witness. |
17 | Executable finite recurrence | `compute_eq_solve` proves the concrete reducer equals the mathematical recurrence. Exact small-instance `decide` proofs remain inside the Lean kernel. No claim of practical scaling. |
18 | Mathematical witnesses | Classical choice occurs in simultaneous child selection and abstract minimal-profile arguments. Computable profile enumeration and finite concrete trees are separately supplied; no efficient extracted global witness compiler is claimed. |
19 | Four-case all-horizon result | A checked finite fixed-point table plus `closed_family_dominates` and horizon padding. Not extrapolation from a tested list of horizons. |
20 | Predecessor preservation | The exact source book and all24 preceding substantive modules remain byte-identical. The aggregate imports, admission map, driver and package version are intentionally extended. |
21
22 ## Source statement fidelity
23
24 The complete source conclusion is retained: exact nondominated profiles, concrete witness existence, feasibility of one online/storage budget, and completeness of pruning dominated children. The source's positive-cost, scalar or finite-state cases are specializations of the implemented nonnegative vector/finite-support model. The finite case guards are Boolean decision tables. Arbitrary predicates can be attached mathematically using classical decidability; that does not provide a computable checker for arbitrary external programs.
25
26 No source-book theorem has been rewritten. Stronger execution and fixed-point lemmas are supporting results, not additional promotions in the27-result book ledger. Core5.3 is not promoted.
27
28 ## Assurance boundary
29
30 The finite field/type definitions are exact. Actual proof terms, not the number of supporting declarations or examples, justify the universal results. The cumulative gate audits transitive axioms and replays every substantive local module. The pinned imported environment is reused, not rebuilt from upstream source. Interpretation of an external experiment or recipient still requires evidence that the supplied model describes it.