ASSUMPTION_REVIEW_BLOCK08.md
Machine Native Reasoning
ASSUMPTION_REVIEW_BLOCK08.md
1 # Assumption review — Block 08
2
3 **New source admission: Core 5.3, label `r:lowerbound`.** The book and all 30 preceding substantive modules are unchanged.
4
5 | Formal object | Required premise and checked boundary |
6 |---|---|
7 | `Tree E Bool C h` | Literal finite report tree. `Bool` is the binary alphabet. A horizon is not the actual depth. |
8 | `Model.Valid` | Nonempty current support, uniformly permitted experiment, actual post-state update, exactly the live children, common successful terminal. |
9 | `Scope.immutable` | The complete modeled state is unchanged. A destructive reset fails this condition even if its eventual repair is valid. |
10 | `Scope.singleton` | A fixed repair succeeds in at most one modeled state. Existence of a successful repair for every case is supplied by the actual successful tree; unused labels need not work. |
11 | `Scope.query_cost` | One scalar natural-number unit per query. No cost of compilation or scope validation is included in this online measure. |
12 | `Scope.terminal_cost` | One unit on every nonempty support. The proof does not impose an invalid empty-support maximum identity. |
13 | Leaves and records | Every possible case reaches a singleton leaf, no impossible leaves are installed, unary queries stay counted. |
14 | `Nat.clog` | Exact natural ceiling logarithm characterized by a power inequality, including n=1. No approximate real log. |
15 | `profile` to `execute` | A maximizing live branch supplies an actual initial-state witness. Lower bound is not merely a loose profile overestimate. |
16 | Frontier closure | Validity and simultaneous attainment of both coordinates are essential. Only one coordinate or a correct tree shape is insufficient. |
17 | Finite scope gate | State, action and artifact types finite. The guard examines exact table fields and all finite support-dependent terminal costs, not names or old cache labels. |
18 | Negative scope result | Means not admitted by this restricted theorem; does not imply infeasibility or falsity of every claim about the revised model. |
19 | Larger horizons | The same certified tree is padded without inserting queries, so all larger finite horizons share the singleton frontier. |
20 | Stronger lower-bound scope | Total permissions and a repair for every state are not necessary for a lower bound on an already successful valid tree. The source assumptions are included. |
21
22 The general source proof was not weakened. Binary tree edge counting and logarithmic information bounds are established elementary mathematics, not priority claims. Same-kernel checking validates formal terms under the pinned imported environment; it does not certify model adequacy or independent origin.