Machine Native Reasoning

Download original file

This is the original source text. Reading it does not run or verify the program.

Read the typeset paper

1 {
2   "schema": "komorebi.machine_reasoning.reviewed_core.admission.v1",
3   "status": "PASS",
4   "version": "1.0.0",
5   "completed_utc": "2026-10-25T17:55:52.053385+00:00",
6   "scope": "All 27 selected source results of Reviewed Core v0.2; not the expanded 1155-page monograph.",
7   "counts": {
8     "selected_source_results": 27,
9     "selected_source_total": 27,
10     "pending_source_results": 0,
11     "production_modules_per_gate": 79,
12     "kernel_replays_per_gate": 78,
13     "controls_per_gate": 188,
14     "new_controls": 7,
15     "axiom_audited_declarations": 3018,
16     "elaborated_theorem_constants": 2364,
17     "authored_declarations": 1927,
18     "authored_theorems": 1273,
19     "new_authored_declarations": 86,
20     "new_supporting_theorems": 51,
21     "unchanged_source_inputs_per_gate": 501,
22     "matched_upstream_artifacts_per_gate": 13440,
23     "preserved_predecessor_files": 80,
24     "commands_per_gate": 372,
25     "production_objects_identical": 79,
26     "comparison_checks": 663
27   },
28   "new_modules": [
29     {
30       "file": "MachineTheory/PartitionOccupancy.lean",
31       "sha256": "ed6e2a088abf68b0fb53da4ea7e6f400e026b32e10408123a32295295accb88b",
32       "lines": 222,
33       "authored_declarations": 28,
34       "authored_theorems": 17
35     },
36     {
37       "file": "MachineTheory/OccupancyBinary.lean",
38       "sha256": "8af6469782ebe0344428f6fa88e34043502e57516933811ddf256054b4f69105",
39       "lines": 133,
40       "authored_declarations": 13,
41       "authored_theorems": 8
42     },
43     {
44       "file": "MachineTheory/OccupancyExamples.lean",
45       "sha256": "18f2a6e59fc08ae2421d3bc330ac670e2cd9f2b5b0cd3c9c39092e387f5729ab",
46       "lines": 228,
47       "authored_declarations": 45,
48       "authored_theorems": 26
49     }
50   ],
51   "actual_axiom_union": [
52     "Classical.choice",
53     "Quot.sound",
54     "propext"
55   ],
56   "primary": {
57     "path": "evidence/final19",
58     "report_sha256": "55d5b2a544434c59a1f2a1f3b0af27995abd1da0839c4e66a721db0b5e7bd1a0",
59     "seconds": 739.2923423680004
60   },
61   "fresh": {
62     "path": "evidence/fresh19",
63     "report_sha256": "35d120b6e69e8b4c7a9f6be989aede2a18fcdb1826d1ae5610086dcd896f6ac8",
64     "seconds": 725.2832252999979
65   },
66   "supervisors": [
67     {
68       "path": "evidence/final19_supervisor.json",
69       "sha256": "0b7482dd54d45ca861780c54e3947f95eed96d82648b006286afea27ad73117e",
70       "receipt": {
71         "argv": [
72           "/opt/codex/runtimes/codex-primary-runtime/dependencies/python/bin/python3",
73           "/workspace/scratch/6a8ff46cf015/mnr_work/Machine_Native_Reasoning_Lean_Core25/scripts/verify.py",
74           "--runtime",
75           "/workspace/scratch/6a8ff46cf015/mnr_runtime/Komorebi_Portable_Lean_4.34.0-rc2",
76           "--out",
77           "evidence/final19"
78         ],
79         "started_at": 1792949479.875747,
80         "ended_at": 1792950219.2606218,
81         "status": "completed",
82         "exit_code": 0,
83         "supervisor_wall_limit": 1800
84       }
85     },
86     {
87       "path": "evidence/fresh19_supervisor.json",
88       "sha256": "3aed9a0ef061fbbb919e0e39e36060de5f7bc933da7d28e3d4d414f7764c9b58",
89       "receipt": {
90         "argv": [
91           "/opt/codex/runtimes/codex-primary-runtime/dependencies/python/bin/python3",
92           "/workspace/scratch/6a8ff46cf015/mnr_fresh19/scripts/verify.py",
93           "--runtime",
94           "/workspace/scratch/6a8ff46cf015/mnr_runtime/Komorebi_Portable_Lean_4.34.0-rc2",
95           "--out",
96           "evidence/fresh19"
97         ],
98         "started_at": 1792950219.333025,
99         "ended_at": 1792950944.686129,
100         "status": "completed",
101         "exit_code": 0,
102         "supervisor_wall_limit": 1800
103       }
104     }
105   ],
106   "comparison": {
107     "path": "evidence/CORE32_COMPARISON.json",
108     "sha256": "5111b299f77862d63388990b47531d74e30077a17db946b0acd6dacc380727ad"
109   },
110   "source_snapshot_sha256": "727af49876690ee83bb18b46895dea01aae296bfeaf83331221870970e59daf0",
111   "nonproduction_helper_differences": [
112     "Audit.olean"
113   ],
114   "independent_review": {
115     "path": "release/independent_review/CORE32_INDEPENDENT_PROOF_AUDIT.md",
116     "sha256": "6ba42fb7cc5880f6f1dfe08764711395c178d6880b4c961ee3c34e98819c7207",
117     "verdict": "proved as written; semantic review, not a second kernel"
118   },
119   "exact_finite_regression": {
120     "status": "PASS",
121     "assertion_tested": "In the explicitly enumerated finite population, direct future-filter target signatures and attained cell-target occupancy have exactly the same fibres; every occupancy occurs; signature count is 2^r; occupancy readout/update agrees with direct world filtering.",
122     "scope": "Finite exact regression, not a universal proof, novelty claim, or variable-length/average-bit/runtime lower bound.",
123     "domain": {
124       "world_sizes": [
125         0,
126         1,
127         2,
128         3,
129         4,
130         5
131       ],
132       "target_alphabet": [
133         0,
134         1,
135         2
136       ],
137       "partitions": "all canonical restricted-growth partitions",
138       "candidates": "all subsets including empty",
139       "events": "exactly all unions of partition cells"
140     },
141     "levels": [
142       {
143         "worlds": 0,
144         "partitions": 1,
145         "target_maps_per_partition": 1,
146         "families": 1
147       },
148       {
149         "worlds": 1,
150         "partitions": 1,
151         "target_maps_per_partition": 3,
152         "families": 3
153       },
154       {
155         "worlds": 2,
156         "partitions": 2,
157         "target_maps_per_partition": 9,
158         "families": 18
159       },
160       {
161         "worlds": 3,
162         "partitions": 5,
163         "target_maps_per_partition": 27,
164         "families": 135
165       },
166       {
167         "worlds": 4,
168         "partitions": 15,
169         "target_maps_per_partition": 81,
170         "families": 1215
171       },
172       {
173         "worlds": 5,
174         "partitions": 52,
175         "target_maps_per_partition": 243,
176         "families": 12636
177       }
178     ],
179     "checks": {
180       "signature_occupancy_classification_candidates": 425232,
181       "current_readout": 425232,
182       "event_update": 3661286,
183       "event_readout": 3661286,
184       "realization_and_exact_count_families": 14012,
185       "full_preimage_realizations": 267114,
186       "empty_candidate": 14012
187     },
188     "boundary_controls": {
189       "empty_worlds": {
190         "worlds": 0,
191         "cells": 0,
192         "attained_pairs": 0,
193         "signatures": 1
194       },
195       "one_cell_constant_target": {
196         "worlds": 3,
197         "cells": 1,
198         "attained_pairs": 1,
199         "signatures": 2
200       },
201       "multiple_targets_per_cell_and_repeated_targets": {
202         "worlds": 4,
203         "cells": 2,
204         "attained_pairs": 4,
205         "signatures": 16
206       },
207       "unattained_target_value": {
208         "unused_value": 2,
209         "attained_pairs": 3
210       },
211       "splitting_cell_invalidates_sufficiency": {
212         "worlds": 2,
213         "candidates": [
214           1,
215           2
216         ],
217         "extra_event": 1
218       },
219       "missing_singleton_events_loses_lower_bound": {
220         "signatures": 2,
221         "old_occupancies": 4
222       },
223       "four_cell_eight_world_sensor": {
224         "worlds": 8,
225         "cells": 4,
226         "attained_pairs": 4,
227         "signatures": 16,
228         "candidate_bits": 8,
229         "occupancy_bits": 4,
230         "too_few_bit_capacity": 8,
231         "current_target_set_loses_correction": true
232       },
233       "too_few_bits_exhaustive_encodings": {
234         "r": [
235           1,
236           2,
237           3
238         ],
239         "b": [
240           0,
241           1,
242           2
243         ],
244         "rejected_assignments": 65553
245       },
246       "sensor_two_event_sequences": 65536
247     },
248     "inputs_before": {
249       "scripts/core32_exact.py": "770d8ac1d3f0a1db0fd8e4d5d70bc89c6eb3925735728241873e038f7c61a1db",
250       "source/core_v0.2.tex": "a15f192322357893c2bb9b2427aac2a02b0753e558b42c0460a6288006ddbe6b",
251       "MachineTheory/Correction.lean": "7085f9f708cd33d2dcc025e6eaed93be4f451656bb445faeb02c49160cb47a2e",
252       "release/NEXT_CORE32_SPEC.md": "3c71ccb23cfbadfcbe87025421e6bd45156c6af09b7a12e770a2e272b00c21fc"
253     },
254     "inputs_after": {
255       "scripts/core32_exact.py": "770d8ac1d3f0a1db0fd8e4d5d70bc89c6eb3925735728241873e038f7c61a1db",
256       "source/core_v0.2.tex": "a15f192322357893c2bb9b2427aac2a02b0753e558b42c0460a6288006ddbe6b",
257       "MachineTheory/Correction.lean": "7085f9f708cd33d2dcc025e6eaed93be4f451656bb445faeb02c49160cb47a2e",
258       "release/NEXT_CORE32_SPEC.md": "3c71ccb23cfbadfcbe87025421e6bd45156c6af09b7a12e770a2e272b00c21fc"
259     },
260     "software": {
261       "python": "3.12.14 (main, Aug 25 2026, 14:00:49) [Clang 22.1.3 ]",
262       "platform": "Linux-6.18.55-x86_64-with-glibc2.39"
263     },
264     "command_template": "python3 scripts/core32_exact.py --out OUTPUT"
265   },
266   "finite_counter_interpretation": {
267     "sensor_two_event_sequences": "65,536 candidate/sequence combinations: 256 candidate subsets times 256 ordered pairs of the 16 admitted events. The historical key name is not a count of distinct event sequences.",
268     "too_few_bits_exhaustive_encodings": "65,553 assignments across (r,b)=(1,0),(2,1),(3,2); not enumeration of all encodings for the four-pair sensor."
269   },
270   "remaining_selected_source_results": [],
271   "remaining_expanded_publication_work": "Recover Machine_Native_Reasoning_Prose_Refined_Source.zip and its matching PDF, then audit and rebuild that separate expanded edition.",
272   "boundary": [
273     "75 inherited substantive modules and five original source-book files unchanged",
274     "No whole-expanded-book formalization",
275     "No learned-model performance or compiled memory implementation claim",
276     "Pinned upstream cache authenticated and reused, not rebuilt",
277     "Same Lean kernel, not a second implementation",
278     "Linux x86-64 with shipped executable-path adapter; no native Windows run",
279     "Latest expanded monograph not recovered or rebuilt; authenticated selected core reader provided separately"
280   ]
281 }

Back to source controls

Back to Machine Native Reasoning