THEOREM_MAP.json
Machine Native Reasoning
THEOREM_MAP.json
This is the original source text. Reading it does not run or verify the program.
1 [
2 {
3 "kind": "proposition",
4 "title": "A record determines a target exactly on its fibres",
5 "label": "r:factor",
6 "number": "1.1",
7 "printed_page": "1",
8 "source_lines": [
9 98,
10 106
11 ],
12 "check_group": "r:factor",
13 "admission_edition": "0.1",
14 "status": "KERNEL_CHECKED_BLOCK01",
15 "lean_modules": [
16 "MachineTheory.Behavior"
17 ],
18 "lean_endpoints": [
19 "Komorebi.MachineTheory.decoder_exists_iff",
20 "Komorebi.MachineTheory.no_decoder_of_collision"
21 ]
22 },
23 {
24 "kind": "theorem",
25 "title": "Evidence-initialized behavioral state",
26 "label": "r:behavior",
27 "number": "1.2",
28 "printed_page": "2",
29 "source_lines": [
30 146,
31 157
32 ],
33 "check_group": "r:behavior",
34 "admission_edition": "0.1",
35 "status": "KERNEL_CHECKED_BLOCK01",
36 "lean_modules": [
37 "MachineTheory.Behavior"
38 ],
39 "lean_endpoints": [
40 "Komorebi.MachineTheory.evidence_initialized_predictor_iff",
41 "Komorebi.MachineTheory.Predictor.record_sufficient",
42 "Komorebi.MachineTheory.Predictor.minimal_initialized_card",
43 "Komorebi.MachineTheory.canonical_initialized_card"
44 ]
45 },
46 {
47 "kind": "proposition",
48 "title": "Exact accounting of the discarded excursion",
49 "label": "r:packet",
50 "number": "2.1",
51 "printed_page": "4",
52 "source_lines": [
53 183,
54 192
55 ],
56 "check_group": "r:packet",
57 "admission_edition": "0.1",
58 "status": "KERNEL_CHECKED_BLOCK01",
59 "lean_modules": [
60 "MachineTheory.Transfer"
61 ],
62 "lean_endpoints": [
63 "Komorebi.MachineTheory.split_encoding_comp",
64 "Komorebi.MachineTheory.hidden_return_identity",
65 "Komorebi.MachineTheory.compressed_comp_iff_no_return",
66 "Komorebi.MachineTheory.split_projector_idempotent",
67 "Komorebi.MachineTheory.compression_projector_idempotent"
68 ]
69 },
70 {
71 "kind": "theorem",
72 "title": "Forward transport of a reusable method",
73 "label": "r:transport",
74 "number": "2.3",
75 "printed_page": "5",
76 "source_lines": [
77 204,
78 218
79 ],
80 "check_group": "r:transport",
81 "admission_edition": "0.1",
82 "status": "KERNEL_CHECKED_BLOCK01",
83 "lean_modules": [
84 "MachineTheory.Transfer"
85 ],
86 "lean_endpoints": [
87 "Komorebi.MachineTheory.forward_transport",
88 "Komorebi.MachineTheory.forward_output",
89 "Komorebi.MachineTheory.invariant_forward_transport",
90 "Komorebi.MachineTheory.invariant_forward_output"
91 ]
92 },
93 {
94 "kind": "theorem",
95 "title": "A common observable quotient",
96 "label": "r:common",
97 "number": "2.4",
98 "printed_page": "5",
99 "source_lines": [
100 233,
101 250
102 ],
103 "check_group": "r:common",
104 "admission_edition": "0.1",
105 "status": "KERNEL_CHECKED_BLOCK17",
106 "lean_modules": [
107 "MachineTheory.CommonQuotient",
108 "MachineTheory.CommonQuotientInterface",
109 "MachineTheory.DiscrepancyClosure",
110 "MachineTheory.CommonQuotientExamples"
111 ],
112 "lean_endpoints": [
113 "Komorebi.MachineTheory.CommonQuotient.source_core24",
114 "Komorebi.MachineTheory.CommonQuotient.source_core24_reference",
115 "Komorebi.MachineTheory.CommonQuotient.agreement_iff_invisible",
116 "Komorebi.MachineTheory.CommonQuotient.agreement_iff_commonModel",
117 "Komorebi.MachineTheory.CommonQuotient.switching_output",
118 "Komorebi.MachineTheory.CommonQuotient.stage_finrank_eq"
119 ],
120 "admission_boundary": "Valid only with completed current-source final17/fresh17 gates and production comparison. The finite catalogue, distinguished reference, every initial vector and every word are retained. Current release report supplies actual admission."
121 },
122 {
123 "kind": "proposition",
124 "title": "When complete packets are genuine probability components",
125 "label": "r:positive-packets",
126 "number": "2.5",
127 "printed_page": "6",
128 "source_lines": [
129 267,
130 279
131 ],
132 "check_group": "r:positive-packets",
133 "admission_edition": "0.2",
134 "status": "KERNEL_CHECKED_BLOCK18",
135 "lean_modules": [
136 "MachineTheory.PositivePackets",
137 "MachineTheory.CoordinatePackets",
138 "MachineTheory.PacketTransport",
139 "MachineTheory.PositivePacketExamples"
140 ],
141 "lean_endpoints": [
142 "Komorebi.MachineTheory.PositivePackets.source_core25",
143 "Komorebi.MachineTheory.PositivePackets.sum_positive_weights_one",
144 "Komorebi.MachineTheory.PositivePackets.Coordinate.source_core25_coordinate",
145 "Komorebi.MachineTheory.PositivePackets.Coordinate.classification_iff",
146 "Komorebi.MachineTheory.PositivePackets.Transport.source_coordinate_change"
147 ]
148 },
149 {
150 "kind": "theorem",
151 "title": "Minimal exact memory for a correction contract",
152 "label": "r:memory",
153 "number": "3.1",
154 "printed_page": "8",
155 "source_lines": [
156 314,
157 325
158 ],
159 "check_group": "r:memory",
160 "admission_edition": "0.1",
161 "status": "KERNEL_CHECKED_BLOCK01",
162 "lean_modules": [
163 "MachineTheory.Correction"
164 ],
165 "lean_endpoints": [
166 "Komorebi.MachineTheory.EvidenceAlgebra.signature_congruence",
167 "Komorebi.MachineTheory.EvidenceAlgebra.memory_readout_continuation",
168 "Komorebi.MachineTheory.EvidenceAlgebra.memory_universal_property",
169 "Komorebi.MachineTheory.EvidenceAlgebra.memory_minimal_card",
170 "Komorebi.MachineTheory.EvidenceAlgebra.signature_empty"
171 ]
172 },
173 {
174 "kind": "corollary",
175 "title": "The size of partition correction memory",
176 "label": "r:occupancy",
177 "number": "3.2",
178 "printed_page": "9",
179 "source_lines": [
180 335,
181 340
182 ],
183 "check_group": "r:occupancy",
184 "admission_edition": "0.1",
185 "status": "KERNEL_CHECKED_BLOCK19",
186 "lean_modules": [
187 "MachineTheory.PartitionOccupancy",
188 "MachineTheory.OccupancyBinary",
189 "MachineTheory.OccupancyExamples"
190 ],
191 "lean_endpoints": [
192 "Komorebi.MachineTheory.PartitionCorrection.partition_correction_memory",
193 "Komorebi.MachineTheory.PartitionCorrection.signature_eq_iff_occupancy_eq",
194 "Komorebi.MachineTheory.PartitionCorrection.occupancy_realize",
195 "Komorebi.MachineTheory.PartitionCorrection.fromOccupancy_bijective",
196 "Komorebi.MachineTheory.PartitionCorrection.memoryEquiv_remember",
197 "Komorebi.MachineTheory.PartitionCorrection.card_memory",
198 "Komorebi.MachineTheory.PartitionCorrection.fixed_bits_necessary",
199 "Komorebi.MachineTheory.PartitionCorrection.bits_finite_continuation",
200 "Komorebi.MachineTheory.PartitionCorrection.bits_readout_continuation",
201 "Komorebi.MachineTheory.PartitionCorrection.nonempty_cells_iff_surjective",
202 "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_signature_count",
203 "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_no_three_bit_memory"
204 ]
205 },
206 {
207 "kind": "theorem",
208 "title": "When a report preserves every Bayesian correction",
209 "label": "r:bayes",
210 "number": "3.4",
211 "printed_page": "9",
212 "source_lines": [
213 364,
214 385
215 ],
216 "check_group": "r:bayes",
217 "admission_edition": "0.1",
218 "status": "KERNEL_CHECKED_BLOCK02",
219 "lean_modules": [
220 "MachineTheory.Bayes"
221 ],
222 "lean_endpoints": [
223 "Komorebi.MachineTheory.Bayes.ReportingModel.all_iff_full_support_prior",
224 "Komorebi.MachineTheory.Bayes.ReportingModel.all_iff_exists_full_support",
225 "Komorebi.MachineTheory.Bayes.ReportingModel.all_iff_reconstruction",
226 "Komorebi.MachineTheory.Bayes.ReportingModel.reconstructs_of_full_support",
227 "Komorebi.MachineTheory.Bayes.ReportingModel.preservesAll_of_reconstructs"
228 ]
229 },
230 {
231 "kind": "theorem",
232 "title": "Least refinement closed under prediction and correction",
233 "label": "r:joint-refinement",
234 "number": "3.5",
235 "printed_page": "11",
236 "source_lines": [
237 405,
238 422
239 ],
240 "check_group": "r:joint-refinement",
241 "admission_edition": "0.2",
242 "status": "KERNEL_CHECKED_BLOCK02",
243 "lean_modules": [
244 "MachineTheory.BayesianLumping",
245 "MachineTheory.Refinement"
246 ],
247 "lean_endpoints": [
248 "Komorebi.MachineTheory.BayesianLumping.likelihood_constant_on_fibres",
249 "Komorebi.MachineTheory.BayesianLumping.fixed_positive_coarse_iff",
250 "Komorebi.MachineTheory.Refinement.step_rel_iff",
251 "Komorebi.MachineTheory.Refinement.bounded_stabilization",
252 "Komorebi.MachineTheory.Refinement.stopIndex_bound",
253 "Komorebi.MachineTheory.Refinement.stable_iff_prediction",
254 "Komorebi.MachineTheory.Refinement.admissible_iff",
255 "Komorebi.MachineTheory.Refinement.least_prediction_correction_refinement"
256 ]
257 },
258 {
259 "kind": "theorem",
260 "title": "One quotient for reports, posteriors, and feedback",
261 "label": "r:instrument",
262 "number": "3.6",
263 "printed_page": "12",
264 "source_lines": [
265 445,
266 466
267 ],
268 "check_group": "r:instrument",
269 "admission_edition": "0.2",
270 "status": "KERNEL_CHECKED_BLOCK01",
271 "lean_modules": [
272 "MachineTheory.Instrument",
273 "MachineTheory.Feedback"
274 ],
275 "lean_endpoints": [
276 "Komorebi.MachineTheory.Instrument.quotient_exists_iff",
277 "Komorebi.MachineTheory.Instrument.quotient_unique",
278 "Komorebi.MachineTheory.Instrument.instrument_iff_reports_and_posteriors",
279 "Komorebi.MachineTheory.Instrument.quotient_feedback_law",
280 "Komorebi.MachineTheory.Instrument.totalHistoryMass_eq",
281 "Komorebi.MachineTheory.Instrument.positive_history_posterior_dist",
282 "Komorebi.MachineTheory.Instrument.stopped_feedback",
283 "Komorebi.MachineTheory.Instrument.stoppedAndSurvivingMass_eq"
284 ]
285 },
286 {
287 "kind": "proposition",
288 "title": "A whole-history bound with an explicit conditioning cost",
289 "label": "r:history-bound",
290 "number": "3.8",
291 "printed_page": "13",
292 "source_lines": [
293 483,
294 503
295 ],
296 "check_group": "r:history-bound",
297 "admission_edition": "0.2",
298 "status": "KERNEL_CHECKED_BLOCK04",
299 "lean_modules": [],
300 "lean_endpoints": [
301 "Komorebi.MachineTheory.ApproximateHistory.whole_history_bound",
302 "Komorebi.MachineTheory.ApproximateHistory.observed_history_bound",
303 "Komorebi.MachineTheory.ApproximateHistory.conditional_final_bound",
304 "Komorebi.MachineTheory.ApproximateHistory.history_event_positive",
305 "Komorebi.MachineTheory.Variation.condition_bound"
306 ]
307 },
308 {
309 "kind": "theorem",
310 "title": "A decision bound for one actual approximation chain",
311 "label": "r:risk",
312 "number": "4.1",
313 "printed_page": "15",
314 "source_lines": [
315 533,
316 550
317 ],
318 "check_group": "r:risk",
319 "admission_edition": "0.1",
320 "status": "KERNEL_CHECKED_BLOCK05",
321 "lean_modules": [
322 "MachineTheory.ResponseDecision",
323 "MachineTheory.DecisionHistory",
324 "MachineTheory.ResponseExamples"
325 ],
326 "lean_endpoints": [
327 "Komorebi.MachineTheory.ResponseDecision.decision_error_global",
328 "Komorebi.MachineTheory.ResponseDecision.metric_minimizers_exist",
329 "Komorebi.MachineTheory.ResponseDecision.regret_to_minimum",
330 "Komorebi.MachineTheory.ResponseDecision.unique_minimizer_transfer",
331 "Komorebi.MachineTheory.ResponseDecision.risk_threshold"
332 ],
333 "formalization_note": "Bounded metric response error plus total variation on the same finite world set; actual finite minimizers, capped regret, strict-gap uniqueness and risk threshold. Direct conditional-history and stored-record composition included as supporting results."
334 },
335 {
336 "kind": "theorem",
337 "title": "A common artifact for fixed recipients",
338 "label": "r:recipient",
339 "number": "4.2",
340 "printed_page": "16",
341 "source_lines": [
342 565,
343 574
344 ],
345 "check_group": "r:recipient",
346 "admission_edition": "0.1",
347 "status": "KERNEL_CHECKED_BLOCK06",
348 "lean_modules": [
349 "MachineTheory.Recipient",
350 "MachineTheory.RecipientExecution",
351 "MachineTheory.RecipientExamples"
352 ],
353 "lean_endpoints": [
354 "Komorebi.MachineTheory.Recipient.encoder_exists_iff",
355 "Komorebi.MachineTheory.Recipient.cardinality_budget_iff",
356 "Komorebi.MachineTheory.Recipient.minimum_image_eq_cover",
357 "Komorebi.MachineTheory.Recipient.minimum_common_artifact",
358 "Komorebi.MachineTheory.RecipientExecution.Audience.common_artifact_iff"
359 ]
360 },
361 {
362 "kind": "theorem",
363 "title": "Exact joint feasibility for explicit controllers",
364 "label": "r:inquiry",
365 "number": "5.1",
366 "printed_page": "17",
367 "source_lines": [
368 611,
369 618
370 ],
371 "check_group": "r:inquiry",
372 "admission_edition": "0.1",
373 "status": "KERNEL_CHECKED_BLOCK07",
374 "lean_modules": [],
375 "lean_endpoints": [
376 "Komorebi.MachineTheory.HardInquiry.Model.exact_frontier",
377 "Komorebi.MachineTheory.HardInquiry.Model.joint_budget_iff",
378 "Komorebi.MachineTheory.HardInquiry.Model.solve_witness",
379 "Komorebi.MachineTheory.HardInquiry.Model.backup_dominates",
380 "Komorebi.MachineTheory.HardInquiry.Model.compute_eq_solve",
381 "Komorebi.MachineTheory.HardInquiry.Model.execution_sound",
382 "Komorebi.MachineTheory.HardInquiry.Model.worst_coordinate_attained",
383 "Komorebi.MachineTheory.HardInquiry.Model.profile_records",
384 "Komorebi.MachineTheory.HardInquiry.AudienceBridge.recipient_inquiry",
385 "Komorebi.MachineTheory.HardExamples.four_frontier_all",
386 "Komorebi.MachineTheory.HardExamples.four_no_mixed_budget",
387 "Komorebi.MachineTheory.HardControls.sensor_recipient_execution"
388 ]
389 },
390 {
391 "kind": "theorem",
392 "title": "A candidate attaining both lower bounds is optimal",
393 "label": "r:lowerbound",
394 "number": "5.3",
395 "printed_page": "18",
396 "source_lines": [
397 635,
398 642
399 ],
400 "check_group": "r:lowerbound",
401 "admission_edition": "0.1",
402 "status": "KERNEL_CHECKED_BLOCK08",
403 "lean_modules": [],
404 "lean_endpoints": [
405 "Komorebi.MachineTheory.BinaryDiagnosis.binary_lower_bounds",
406 "Komorebi.MachineTheory.BinaryDiagnosis.records_exact",
407 "Komorebi.MachineTheory.BinaryDiagnosis.actual_run_lower_bound",
408 "Komorebi.MachineTheory.BinaryDiagnosis.checked_candidate_closes_frontier",
409 "Komorebi.MachineTheory.BinaryDiagnosis.admitted_frontier",
410 "Komorebi.MachineTheory.BinaryDiagnosis.admitted_budget"
411 ]
412 },
413 {
414 "kind": "theorem",
415 "title": "The same compressed belief supports the same inquiry",
416 "label": "r:belief-planning",
417 "number": "5.4",
418 "printed_page": "20",
419 "source_lines": [
420 664,
421 675
422 ],
423 "check_group": "r:belief-planning",
424 "admission_edition": "0.2",
425 "status": "KERNEL_CHECKED_BLOCK03",
426 "lean_modules": [],
427 "lean_endpoints": [
428 "Komorebi.MachineTheory.Planning.optimal_value_characterization",
429 "Komorebi.MachineTheory.Planning.ExactMap.value_eq",
430 "Komorebi.MachineTheory.Planning.ExactMap.firstValue_eq",
431 "Komorebi.MachineTheory.Planning.ExactMap.optimalFirst_iff",
432 "Komorebi.MachineTheory.Planning.ExactMap.feasible_iff",
433 "Komorebi.MachineTheory.Planning.ExactMap.evaluate_eq",
434 "Komorebi.MachineTheory.Planning.ExactMap.common_minimizing_tree",
435 "Komorebi.MachineTheory.BeliefPlanning.compressed_belief_planning",
436 "Komorebi.MachineTheory.BeliefPlanning.common_optimal_inquiry",
437 "Komorebi.MachineTheory.BeliefPlanning.constructed_quotient_planning",
438 "Komorebi.MachineTheory.Planning.ExactMap.optimalStop_iff"
439 ]
440 },
441 {
442 "kind": "proposition",
443 "title": "Uniform model error controls a changed policy",
444 "label": "r:policy-error",
445 "number": "5.6",
446 "printed_page": "22",
447 "source_lines": [
448 712,
449 730
450 ],
451 "check_group": "r:policy-error",
452 "admission_edition": "0.2",
453 "status": "KERNEL_CHECKED_BLOCK04",
454 "lean_modules": [],
455 "lean_endpoints": [
456 "Komorebi.MachineTheory.ApproximateDecision.same_policy_error",
457 "Komorebi.MachineTheory.ApproximateDecision.uniform_policy_regret",
458 "Komorebi.MachineTheory.ApproximateDecision.minimizing_policies_exist",
459 "Komorebi.MachineTheory.ApproximateDecision.history_policy_error",
460 "Komorebi.MachineTheory.ApproximateDecision.history_selected_policy_regret"
461 ]
462 },
463 {
464 "kind": "proposition",
465 "title": "What finite counterexamples establish",
466 "label": "r:cegis",
467 "number": "6.1",
468 "printed_page": "23",
469 "source_lines": [
470 742,
471 747
472 ],
473 "check_group": "r:cegis",
474 "admission_edition": "0.1",
475 "status": "KERNEL_CHECKED_BLOCK09",
476 "lean_modules": [
477 "MachineTheory.Synthesis",
478 "MachineTheory.SynthesisTrace",
479 "MachineTheory.SynthesisProtocol",
480 "MachineTheory.SynthesisBudget"
481 ],
482 "lean_endpoints": [
483 "Komorebi.MachineTheory.Synthesis.counterexample_guided_synthesis",
484 "Komorebi.MachineTheory.Synthesis.accepted_first",
485 "Komorebi.MachineTheory.Synthesis.exhaustion_iff",
486 "Komorebi.MachineTheory.Synthesis.truthful_call_bound",
487 "Komorebi.MachineTheory.Synthesis.truthful_outcome",
488 "Komorebi.MachineTheory.Synthesis.no_unbounded_truthful_calls",
489 "Komorebi.MachineTheory.Synthesis.resume_bounded",
490 "Komorebi.MachineTheory.Synthesis.bounded_completion_sound"
491 ]
492 },
493 {
494 "kind": "theorem",
495 "title": "Ordered semantic compression preserves the teacher trace",
496 "label": "r:ordered",
497 "number": "6.2",
498 "printed_page": "23",
499 "source_lines": [
500 759,
501 766
502 ],
503 "check_group": "r:ordered",
504 "admission_edition": "0.1",
505 "status": "KERNEL_CHECKED_BLOCK09",
506 "lean_modules": [
507 "MachineTheory.SynthesisQuotient"
508 ],
509 "lean_endpoints": [
510 "Komorebi.MachineTheory.Synthesis.ordered_compression",
511 "Komorebi.MachineTheory.Synthesis.representative_search_complete",
512 "Komorebi.MachineTheory.Synthesis.teacher_work_preserved",
513 "Komorebi.MachineTheory.Synthesis.prepare_value"
514 ]
515 },
516 {
517 "kind": "proposition",
518 "title": "A sound prefix exclusion",
519 "label": "r:prefix",
520 "number": "6.4",
521 "printed_page": "24",
522 "source_lines": [
523 781,
524 788
525 ],
526 "check_group": "r:prefix",
527 "admission_edition": "0.1",
528 "status": "KERNEL_CHECKED_BLOCK10",
529 "lean_modules": [],
530 "lean_endpoints": [
531 "Komorebi.MachineTheory.PrefixScan.integer_completion_iff",
532 "Komorebi.MachineTheory.OrderedCompiler.prefix_exclusion",
533 "Komorebi.MachineTheory.OrderedCompiler.source_prefix_certificate",
534 "Komorebi.MachineTheory.OrderedCompiler.admitted_search_sound_complete",
535 "Komorebi.MachineTheory.OrderedCompiler.admitted_failure_iff_empty_frontier"
536 ]
537 },
538 {
539 "kind": "theorem",
540 "title": "Selective reuse with complete dependencies",
541 "label": "r:dependencies",
542 "number": "7.1",
543 "printed_page": "26",
544 "source_lines": [
545 809,
546 814
547 ],
548 "check_group": "r:dependencies",
549 "admission_edition": "0.1",
550 "status": "KERNEL_CHECKED_BLOCK11",
551 "lean_modules": [
552 "MachineTheory.DependencyGraph",
553 "MachineTheory.Revision",
554 "MachineTheory.RevisionReplay",
555 "MachineTheory.RevisionAdmission",
556 "MachineTheory.RevisionExamples",
557 "MachineTheory.RevisionControls"
558 ],
559 "lean_endpoints": [
560 "Komorebi.MachineTheory.Dependency.System.selective_reuse",
561 "Komorebi.MachineTheory.Dependency.System.restoration",
562 "Komorebi.MachineTheory.Dependency.System.admitted_reuse_and_restoration",
563 "Komorebi.MachineTheory.Dependency.closure_iff_reach"
564 ]
565 },
566 {
567 "kind": "proposition",
568 "title": "Which gains survive every admitted price?",
569 "label": "r:prices",
570 "number": "7.3",
571 "printed_page": "27",
572 "source_lines": [
573 835,
574 840
575 ],
576 "check_group": "r:prices",
577 "admission_edition": "0.1",
578 "status": "KERNEL_CHECKED_BLOCK12",
579 "lean_modules": [],
580 "lean_endpoints": [
581 "Komorebi.MachineTheory.ResourcePrices.all_nonnegative_prices_iff",
582 "Komorebi.MachineTheory.ResourcePrices.finite_price_minimum",
583 "Komorebi.MachineTheory.ResourcePrices.listed_hull_minimizer",
584 "Komorebi.MachineTheory.ResourcePrices.saving_net",
585 "Komorebi.MachineTheory.PriceExamples.priced_scan",
586 "Komorebi.MachineTheory.PriceExamples.robust_reuse_threshold",
587 "Komorebi.MachineTheory.PriceRevision.restored_negative_real_saving"
588 ]
589 },
590 {
591 "kind": "proposition",
592 "title": "A conditional error budget for a lineage",
593 "label": "r:lineage",
594 "number": "7.4",
595 "printed_page": "28",
596 "source_lines": [
597 848,
598 858
599 ],
600 "check_group": "r:lineage",
601 "admission_edition": "0.1",
602 "status": "KERNEL_CHECKED_BLOCK13",
603 "lean_modules": [
604 "MachineTheory.Lineage",
605 "MachineTheory.LineageExamples"
606 ],
607 "lean_endpoints": [
608 "Komorebi.MachineTheory.Lineage.conditional_marginal_bound",
609 "Komorebi.MachineTheory.Lineage.finite_lineage_bound",
610 "Komorebi.MachineTheory.Lineage.lineage_bound",
611 "Komorebi.MachineTheory.Lineage.lineage_ennreal_bound",
612 "Komorebi.MachineTheory.Lineage.selected_lineage_bound",
613 "Komorebi.MachineTheory.Lineage.stopped_selected_lineage_bound",
614 "Komorebi.MachineTheory.Lineage.divergent_real_total_not_union_bound"
615 ]
616 },
617 {
618 "kind": "proposition",
619 "title": "Target-relative joint reconstruction",
620 "label": "r:reconstruction",
621 "number": "8.1",
622 "printed_page": "29",
623 "source_lines": [
624 873,
625 878
626 ],
627 "check_group": "r:reconstruction",
628 "admission_edition": "0.1",
629 "status": "KERNEL_CHECKED_BLOCK14",
630 "lean_modules": [],
631 "lean_endpoints": [
632 "Komorebi.MachineTheory.JointReconstruction.finite_joint_reconstruction",
633 "Komorebi.MachineTheory.JointReconstruction.exists_decoder_iff_ker_le",
634 "Komorebi.MachineTheory.JointReconstruction.exists_decoder_extending_imageDecoder",
635 "Komorebi.MachineTheory.JointReconstruction.full_state_iff_injective",
636 "Komorebi.MachineTheory.JointReconstruction.ker_stackRecords",
637 "Komorebi.MachineTheory.JointReconstruction.stacked_decoder_iff"
638 ]
639 },
640 {
641 "kind": "theorem",
642 "title": "A quotient that preserves legal operations",
643 "label": "r:governance",
644 "number": "8.2",
645 "printed_page": "29",
646 "source_lines": [
647 888,
648 898
649 ],
650 "check_group": "r:governance",
651 "admission_edition": "0.1",
652 "status": "KERNEL_CHECKED_BLOCK15",
653 "lean_modules": [],
654 "lean_endpoints": [
655 "Komorebi.MachineTheory.LegalQuotient.finite_source_legal_quotient",
656 "Komorebi.MachineTheory.LegalQuotient.exists_quotient_iff",
657 "Komorebi.MachineTheory.LegalQuotient.representativeQuotient_factors",
658 "Komorebi.MachineTheory.LegalQuotient.quotient_unique",
659 "Komorebi.MachineTheory.LegalQuotient.ofEnabled_reconstruct",
660 "Komorebi.MachineTheory.LegalQuotient.finite_legal_quotient_sequences",
661 "Komorebi.MachineTheory.LegalQuotient.Factors.execute_map",
662 "Komorebi.MachineTheory.LegalQuotient.Factors.labels_eq",
663 "Komorebi.MachineTheory.LegalQuotient.Factors.lift_execution"
664 ]
665 },
666 {
667 "kind": "theorem",
668 "title": "Safe continuation that retains an ending strategy",
669 "label": "r:ending",
670 "number": "8.3",
671 "printed_page": "30",
672 "source_lines": [
673 918,
674 927
675 ],
676 "check_group": "r:ending",
677 "admission_edition": "0.1",
678 "status": "KERNEL_CHECKED_BLOCK16_RECOVERY",
679 "lean_modules": [
680 "MachineTheory.FiniteFixedPoints",
681 "MachineTheory.SafeEnding",
682 "MachineTheory.SafeEndingPolicies",
683 "MachineTheory.SafeEndingExamples"
684 ],
685 "lean_endpoints": [
686 "Komorebi.MachineTheory.SafeEnding.ending_stabilizes",
687 "Komorebi.MachineTheory.SafeEnding.running_stabilizes",
688 "Komorebi.MachineTheory.SafeEnding.endRank_zero_iff",
689 "Komorebi.MachineTheory.SafeEnding.rank_action",
690 "Komorebi.MachineTheory.SafeEnding.ending_region_iff",
691 "Komorebi.MachineTheory.SafeEnding.safe_continuation_iff",
692 "Komorebi.MachineTheory.SafeEnding.source_core83",
693 "Komorebi.MachineTheory.SafeEnding.command_rank_bound",
694 "Komorebi.MachineTheory.SafeEnding.command_rank_arrival",
695 "Komorebi.MachineTheory.SafeEnding.running_has_infinite_path",
696 "Komorebi.MachineTheory.SafeEnding.ending_prefix_extends"
697 ],
698 "assurance_note": "Admission requires completed current-source final16/fresh16 gates and production comparison. Full-history strategies, deadlock, observable command, first-arrival safety and first-entry rank are explicit. The source hold-at-goal assumption is unnecessary for first-arrival semantics."
699 }
700 ]
Other PDFs for this work
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: e0315bcc86c626406a4fd8cfd74edd0a970f205a7ea2d9a554f2d01d99fdfa6b