CLAUSE_CORRESPONDENCE.json
Machine Native Reasoning
CLAUSE_CORRESPONDENCE.json
This is the original source text. Reading it does not run or verify the program.
1 {
2 "schema": "komorebi.core32.clause-correspondence.v1",
3 "status": "PASS",
4 "source_label": "r:occupancy",
5 "source_theorem_number": "3.2",
6 "source_file": "source/core_v0.2.tex",
7 "source_lines": [
8 335,
9 340
10 ],
11 "source_sha256": "a15f192322357893c2bb9b2427aac2a02b0753e558b42c0460a6288006ddbe6b",
12 "raw_api_file": "checks/CheckOccupancyAPI.lean",
13 "raw_api_sha256": "a18b2940d67a0fb19dbd1a3686babf034985ead372ea12d7bd1c5ea5926088c8",
14 "primary_axiom_record_sha256": "30333c1f79d7e93cb167e607cb96c277f46690a8a8ab61519224552893fb8923",
15 "secondary_axiom_record_sha256": "30333c1f79d7e93cb167e607cb96c277f46690a8a8ab61519224552893fb8923",
16 "primary_gate_receipt": {
17 "path": "evidence/final19/report.json",
18 "sha256": "55d5b2a544434c59a1f2a1f3b0af27995abd1da0839c4e66a721db0b5e7bd1a0"
19 },
20 "secondary_gate_receipt": {
21 "path": "evidence/fresh19/report.json",
22 "sha256": "35d120b6e69e8b4c7a9f6be989aede2a18fcdb1826d1ae5610086dcd896f6ac8"
23 },
24 "production_comparison_receipt": {
25 "path": "evidence/CORE32_COMPARISON.json",
26 "sha256": "5111b299f77862d63388990b47531d74e30077a17db946b0acd6dacc380727ad"
27 },
28 "actual_axiom_binding": "Every listed declaration is bound to the identical actual post-build transitive axiom records from both completed cold gates.",
29 "registered_lean_modules": [
30 "MachineTheory.PartitionOccupancy",
31 "MachineTheory.OccupancyBinary",
32 "MachineTheory.OccupancyExamples"
33 ],
34 "registered_lean_endpoints": [
35 "Komorebi.MachineTheory.PartitionCorrection.partition_correction_memory",
36 "Komorebi.MachineTheory.PartitionCorrection.signature_eq_iff_occupancy_eq",
37 "Komorebi.MachineTheory.PartitionCorrection.occupancy_realize",
38 "Komorebi.MachineTheory.PartitionCorrection.fromOccupancy_bijective",
39 "Komorebi.MachineTheory.PartitionCorrection.memoryEquiv_remember",
40 "Komorebi.MachineTheory.PartitionCorrection.card_memory",
41 "Komorebi.MachineTheory.PartitionCorrection.fixed_bits_necessary",
42 "Komorebi.MachineTheory.PartitionCorrection.bits_finite_continuation",
43 "Komorebi.MachineTheory.PartitionCorrection.bits_readout_continuation",
44 "Komorebi.MachineTheory.PartitionCorrection.nonempty_cells_iff_surjective",
45 "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_signature_count",
46 "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_no_three_bit_memory"
47 ],
48 "registry_snapshot": {
49 "file": "THEOREM_MAP.json",
50 "sha256": "e0315bcc86c626406a4fd8cfd74edd0a970f205a7ea2d9a554f2d01d99fdfa6b",
51 "use": "Endpoint names and source anchor only; its staged status field is not used as acceptance evidence."
52 },
53 "independent_semantic_review": {
54 "path": "release/independent_review/CORE32_INDEPENDENT_PROOF_AUDIT.md",
55 "sha256": "6ba42fb7cc5880f6f1dfe08764711395c178d6880b4c961ee3c34e98819c7207",
56 "verdict": "No remaining mathematical or source-correspondence gap found for the pinned raw proof revisions.",
57 "scope": "Independent model-based semantic/source review; not a Lean kernel, transitive-axiom, release-gate or independent human peer-review certificate."
58 },
59 "production_modules": [
60 {
61 "file": "MachineTheory/PartitionOccupancy.lean",
62 "sha256": "ed6e2a088abf68b0fb53da4ea7e6f400e026b32e10408123a32295295accb88b",
63 "lines": 222,
64 "authored_declarations": 28,
65 "supporting_theorems": 17
66 },
67 {
68 "file": "MachineTheory/OccupancyBinary.lean",
69 "sha256": "8af6469782ebe0344428f6fa88e34043502e57516933811ddf256054b4f69105",
70 "lines": 133,
71 "authored_declarations": 13,
72 "supporting_theorems": 8
73 },
74 {
75 "file": "MachineTheory/OccupancyExamples.lean",
76 "sha256": "18f2a6e59fc08ae2421d3bc330ac670e2cd9f2b5b0cd3c9c39092e387f5729ab",
77 "lines": 228,
78 "authored_declarations": 45,
79 "supporting_theorems": 26
80 }
81 ],
82 "clauses": [
83 {
84 "id": "partition_events",
85 "clause": "Actual partition evidence algebra",
86 "scope": "source theorem",
87 "source_lines": [
88 [
89 305,
90 305
91 ],
92 [
93 329,
94 329
95 ]
96 ],
97 "statement": "For the raw cell map c : \u03a9 \u2192 I, the admitted events are exactly c\u207b\u00b9(J) for J \u2286 I. All named cells c\u207b\u00b9({i}) are nonempty if and only if c is surjective.",
98 "declarations": [
99 {
100 "name": "Komorebi.MachineTheory.PartitionCorrection.algebra",
101 "kind": "def",
102 "file": "MachineTheory/PartitionOccupancy.lean",
103 "line": 18,
104 "actual_axioms": []
105 },
106 {
107 "name": "Komorebi.MachineTheory.PartitionCorrection.event",
108 "kind": "def",
109 "file": "MachineTheory/PartitionOccupancy.lean",
110 "line": 26,
111 "actual_axioms": []
112 },
113 {
114 "name": "Komorebi.MachineTheory.PartitionCorrection.event_membership_iff",
115 "kind": "theorem",
116 "file": "MachineTheory/PartitionOccupancy.lean",
117 "line": 29,
118 "actual_axioms": []
119 },
120 {
121 "name": "Komorebi.MachineTheory.PartitionCorrection.nonempty_cells_iff_surjective",
122 "kind": "theorem",
123 "file": "MachineTheory/PartitionOccupancy.lean",
124 "line": 212,
125 "actual_axioms": []
126 }
127 ],
128 "correspondence_notes": [
129 "The EvidenceAlgebra carries its own \u03a9 event and intersection-closure proofs. It is not an arbitrary algebra supplied together with the desired conclusion.",
130 "The surjective raw source endpoint preserves the source nonempty-cell convention; the intermediate results also tolerate unused cell names."
131 ]
132 },
133 {
134 "id": "attained_pairs",
135 "clause": "Attained pairs and occupancy",
136 "scope": "source theorem",
137 "source_lines": [
138 [
139 331,
140 333
141 ]
142 ],
143 "statement": "D = range (\u03c9 \u21a6 (c \u03c9,t \u03c9)); the map p : \u03a9 \u2192 D is onto. O(V)=p(V), so d=(i,y) belongs to O(V) exactly when V contains a world with cell i and target y.",
144 "declarations": [
145 {
146 "name": "Komorebi.MachineTheory.PartitionCorrection.Pair",
147 "kind": "abbrev",
148 "file": "MachineTheory/PartitionOccupancy.lean",
149 "line": 33,
150 "actual_axioms": []
151 },
152 {
153 "name": "Komorebi.MachineTheory.PartitionCorrection.pair",
154 "kind": "def",
155 "file": "MachineTheory/PartitionOccupancy.lean",
156 "line": 35,
157 "actual_axioms": []
158 },
159 {
160 "name": "Komorebi.MachineTheory.PartitionCorrection.pair_surjective",
161 "kind": "theorem",
162 "file": "MachineTheory/PartitionOccupancy.lean",
163 "line": 38,
164 "actual_axioms": []
165 },
166 {
167 "name": "Komorebi.MachineTheory.PartitionCorrection.occupancy",
168 "kind": "def",
169 "file": "MachineTheory/PartitionOccupancy.lean",
170 "line": 45,
171 "actual_axioms": []
172 },
173 {
174 "name": "Komorebi.MachineTheory.PartitionCorrection.mem_occupancy_iff",
175 "kind": "theorem",
176 "file": "MachineTheory/PartitionOccupancy.lean",
177 "line": 48,
178 "actual_axioms": []
179 }
180 ],
181 "correspondence_notes": [
182 "Only \u03a9 is required to be finite for cardinality and bit results. No Fintype I, Fintype Y, target-surjectivity, or target-fibre size hypothesis is imposed."
183 ]
184 },
185 {
186 "id": "signature_classification",
187 "clause": "Correction signatures agree exactly when occupancies agree",
188 "scope": "source theorem",
189 "source_lines": [
190 [
191 308,
192 312
193 ],
194 [
195 336,
196 339
197 ]
198 ],
199 "statement": "For all V,W \u2286 \u03a9, \u03a3(V)=\u03a3(W) iff O(V)=O(W). A singleton-cell signature coordinate recovers each occupancy membership; any union-of-cells target image is recovered by transporting its world witness through occupancy.",
200 "declarations": [
201 {
202 "name": "Komorebi.MachineTheory.PartitionCorrection.mem_occupancy_iff_single_cell",
203 "kind": "theorem",
204 "file": "MachineTheory/PartitionOccupancy.lean",
205 "line": 60,
206 "actual_axioms": [
207 "propext"
208 ]
209 },
210 {
211 "name": "Komorebi.MachineTheory.PartitionCorrection.signature_eq_iff_occupancy_eq",
212 "kind": "theorem",
213 "file": "MachineTheory/PartitionOccupancy.lean",
214 "line": 72,
215 "actual_axioms": [
216 "propext",
217 "Quot.sound"
218 ]
219 }
220 ]
221 },
222 {
223 "id": "realization",
224 "clause": "Every subset of attained pairs occurs",
225 "scope": "source theorem",
226 "source_lines": [
227 [
228 339,
229 339
230 ]
231 ],
232 "statement": "For each S \u2286 D, realize(S)=p\u207b\u00b9(S) has occupancy exactly S. Thus occupancy is onto the entire powerset of D.",
233 "declarations": [
234 {
235 "name": "Komorebi.MachineTheory.PartitionCorrection.realize",
236 "kind": "def",
237 "file": "MachineTheory/PartitionOccupancy.lean",
238 "line": 110,
239 "actual_axioms": []
240 },
241 {
242 "name": "Komorebi.MachineTheory.PartitionCorrection.occupancy_realize",
243 "kind": "theorem",
244 "file": "MachineTheory/PartitionOccupancy.lean",
245 "line": 113,
246 "actual_axioms": [
247 "propext",
248 "Classical.choice",
249 "Quot.sound"
250 ]
251 },
252 {
253 "name": "Komorebi.MachineTheory.PartitionCorrection.occupancy_surjective",
254 "kind": "theorem",
255 "file": "MachineTheory/PartitionOccupancy.lean",
256 "line": 117,
257 "actual_axioms": [
258 "propext",
259 "Classical.choice",
260 "Quot.sound"
261 ]
262 }
263 ],
264 "correspondence_notes": [
265 "This is the explicit full-pair-fibre preimage alternative allowed by NEXT_CORE32_SPEC.md. It replaces the prose selection of one representative world from each included cell\u2013target intersection. Surjectivity of p proves p(p\u207b\u00b9(S))=S.",
266 "The realization definition itself selects no representative worlds. This does not assert that the entire encoding development avoids classical choice."
267 ]
268 },
269 {
270 "id": "memory_equivalence",
271 "clause": "Actual equivalence between attained signatures and occupancy subsets",
272 "scope": "source theorem",
273 "source_lines": [
274 [
275 336,
276 339
277 ]
278 ],
279 "statement": "fromOccupancy(S)=remember(realize(S)) is bijective. Its inverse memoryEquiv is an Equiv from attained correction signatures to Set D, and memoryEquiv(remember(V))=O(V).",
280 "declarations": [
281 {
282 "name": "Komorebi.MachineTheory.PartitionCorrection.fromOccupancy",
283 "kind": "def",
284 "file": "MachineTheory/PartitionOccupancy.lean",
285 "line": 121,
286 "actual_axioms": []
287 },
288 {
289 "name": "Komorebi.MachineTheory.PartitionCorrection.fromOccupancy_bijective",
290 "kind": "theorem",
291 "file": "MachineTheory/PartitionOccupancy.lean",
292 "line": 124,
293 "actual_axioms": [
294 "propext",
295 "Classical.choice",
296 "Quot.sound"
297 ]
298 },
299 {
300 "name": "Komorebi.MachineTheory.PartitionCorrection.memoryEquiv",
301 "kind": "def",
302 "file": "MachineTheory/PartitionOccupancy.lean",
303 "line": 142,
304 "actual_axioms": [
305 "propext",
306 "Classical.choice",
307 "Quot.sound"
308 ]
309 },
310 {
311 "name": "Komorebi.MachineTheory.PartitionCorrection.memoryEquiv_fromOccupancy",
312 "kind": "theorem",
313 "file": "MachineTheory/PartitionOccupancy.lean",
314 "line": 146,
315 "actual_axioms": [
316 "propext",
317 "Classical.choice",
318 "Quot.sound"
319 ]
320 },
321 {
322 "name": "Komorebi.MachineTheory.PartitionCorrection.fromOccupancy_occupancy",
323 "kind": "theorem",
324 "file": "MachineTheory/PartitionOccupancy.lean",
325 "line": 150,
326 "actual_axioms": [
327 "propext",
328 "Classical.choice",
329 "Quot.sound"
330 ]
331 },
332 {
333 "name": "Komorebi.MachineTheory.PartitionCorrection.memoryEquiv_remember",
334 "kind": "theorem",
335 "file": "MachineTheory/PartitionOccupancy.lean",
336 "line": 155,
337 "actual_axioms": [
338 "propext",
339 "Classical.choice",
340 "Quot.sound"
341 ]
342 }
343 ],
344 "correspondence_notes": [
345 "Memory is the inherited attained range of the actual correction signature. It is not an arbitrary type of matching cardinality. The equivalence contains both inverse laws."
346 ]
347 },
348 {
349 "id": "signature_count",
350 "clause": "Exactly 2^r attained signatures",
351 "scope": "source theorem",
352 "source_lines": [
353 [
354 336,
355 339
356 ]
357 ],
358 "statement": "With finite \u03a9 and r=card D, card(Memory t)=2^r by the actual memory\u2013powerset equivalence and finite powerset cardinality.",
359 "declarations": [
360 {
361 "name": "Komorebi.MachineTheory.PartitionCorrection.card_memory",
362 "kind": "theorem",
363 "file": "MachineTheory/PartitionOccupancy.lean",
364 "line": 159,
365 "actual_axioms": [
366 "propext",
367 "Classical.choice",
368 "Quot.sound"
369 ]
370 }
371 ]
372 },
373 {
374 "id": "occupancy_operations",
375 "clause": "Exact readout and admitted evidence update on occupancy",
376 "scope": "source theorem",
377 "source_lines": [
378 [
379 305,
380 305
381 ],
382 [
383 315,
384 324
385 ],
386 [
387 339,
388 339
389 ]
390 ],
391 "statement": "Readout is the image of occupancy under target projection. Filtering by c\u207b\u00b9(J) intersects occupancy with the pairs whose cell lies in J. Every actual admitted event has such a representative.",
392 "declarations": [
393 {
394 "name": "Komorebi.MachineTheory.PartitionCorrection.readOccupancy",
395 "kind": "def",
396 "file": "MachineTheory/PartitionOccupancy.lean",
397 "line": 165,
398 "actual_axioms": []
399 },
400 {
401 "name": "Komorebi.MachineTheory.PartitionCorrection.readOccupancy_occupancy",
402 "kind": "theorem",
403 "file": "MachineTheory/PartitionOccupancy.lean",
404 "line": 168,
405 "actual_axioms": [
406 "propext",
407 "Quot.sound"
408 ]
409 },
410 {
411 "name": "Komorebi.MachineTheory.PartitionCorrection.restrictOccupancy",
412 "kind": "def",
413 "file": "MachineTheory/PartitionOccupancy.lean",
414 "line": 175,
415 "actual_axioms": []
416 },
417 {
418 "name": "Komorebi.MachineTheory.PartitionCorrection.occupancy_inter_cells",
419 "kind": "theorem",
420 "file": "MachineTheory/PartitionOccupancy.lean",
421 "line": 178,
422 "actual_axioms": [
423 "propext",
424 "Quot.sound"
425 ]
426 },
427 {
428 "name": "Komorebi.MachineTheory.PartitionCorrection.eventCells",
429 "kind": "def",
430 "file": "MachineTheory/PartitionOccupancy.lean",
431 "line": 197,
432 "actual_axioms": [
433 "Classical.choice"
434 ]
435 },
436 {
437 "name": "Komorebi.MachineTheory.PartitionCorrection.eventCells_preimage",
438 "kind": "theorem",
439 "file": "MachineTheory/PartitionOccupancy.lean",
440 "line": 200,
441 "actual_axioms": [
442 "Classical.choice"
443 ]
444 },
445 {
446 "name": "Komorebi.MachineTheory.PartitionCorrection.occupancy_filter",
447 "kind": "theorem",
448 "file": "MachineTheory/PartitionOccupancy.lean",
449 "line": 203,
450 "actual_axioms": [
451 "propext",
452 "Classical.choice",
453 "Quot.sound"
454 ]
455 }
456 ],
457 "correspondence_notes": [
458 "eventCells uses a chosen cell-subset representative of an actual admitted event, and eventCells_preimage proves its preimage equals that event. Only attained pairs are used, so unused cell names cannot affect a filtered result."
459 ]
460 },
461 {
462 "id": "binary_sufficiency",
463 "clause": "Actual optimal-width binary states and operations",
464 "scope": "source theorem",
465 "source_lines": [
466 [
467 336,
468 339
469 ]
470 ],
471 "statement": "Set D is equivalent to Fin r \u2192 Bool. Composing with memoryEquiv gives an actual binaryMemoryEquiv. encode maps every candidate to r bits; readBits and updateBits satisfy exact raw current-readout and filtering equations; every r-bit state is attained by an encoding.",
472 "declarations": [
473 {
474 "name": "Komorebi.MachineTheory.PartitionCorrection.bitsEquiv",
475 "kind": "def",
476 "file": "MachineTheory/OccupancyBinary.lean",
477 "line": 18,
478 "actual_axioms": [
479 "propext",
480 "Classical.choice",
481 "Quot.sound"
482 ]
483 },
484 {
485 "name": "Komorebi.MachineTheory.PartitionCorrection.binaryMemoryEquiv",
486 "kind": "def",
487 "file": "MachineTheory/OccupancyBinary.lean",
488 "line": 36,
489 "actual_axioms": [
490 "propext",
491 "Classical.choice",
492 "Quot.sound"
493 ]
494 },
495 {
496 "name": "Komorebi.MachineTheory.PartitionCorrection.encode",
497 "kind": "def",
498 "file": "MachineTheory/OccupancyBinary.lean",
499 "line": 40,
500 "actual_axioms": [
501 "propext",
502 "Classical.choice",
503 "Quot.sound"
504 ]
505 },
506 {
507 "name": "Komorebi.MachineTheory.PartitionCorrection.readBits",
508 "kind": "def",
509 "file": "MachineTheory/OccupancyBinary.lean",
510 "line": 43,
511 "actual_axioms": [
512 "propext",
513 "Classical.choice",
514 "Quot.sound"
515 ]
516 },
517 {
518 "name": "Komorebi.MachineTheory.PartitionCorrection.updateBits",
519 "kind": "def",
520 "file": "MachineTheory/OccupancyBinary.lean",
521 "line": 47,
522 "actual_axioms": [
523 "propext",
524 "Classical.choice",
525 "Quot.sound"
526 ]
527 },
528 {
529 "name": "Komorebi.MachineTheory.PartitionCorrection.encode_read",
530 "kind": "theorem",
531 "file": "MachineTheory/OccupancyBinary.lean",
532 "line": 52,
533 "actual_axioms": [
534 "propext",
535 "Classical.choice",
536 "Quot.sound"
537 ]
538 },
539 {
540 "name": "Komorebi.MachineTheory.PartitionCorrection.encode_update",
541 "kind": "theorem",
542 "file": "MachineTheory/OccupancyBinary.lean",
543 "line": 57,
544 "actual_axioms": [
545 "propext",
546 "Classical.choice",
547 "Quot.sound"
548 ]
549 },
550 {
551 "name": "Komorebi.MachineTheory.PartitionCorrection.encode_surjective",
552 "kind": "theorem",
553 "file": "MachineTheory/OccupancyBinary.lean",
554 "line": 63,
555 "actual_axioms": [
556 "propext",
557 "Classical.choice",
558 "Quot.sound"
559 ]
560 }
561 ],
562 "correspondence_notes": [
563 "The finite enumeration and characteristic-vector equivalence are noncomputable Lean definitions. This is an exact mathematical representation theorem, not a benchmark or executable-runtime claim."
564 ]
565 },
566 {
567 "id": "finite_continuations",
568 "clause": "Every finite admitted continuation preserves exact state and readout",
569 "scope": "inherited correction contract instantiated for the new encoding",
570 "source_lines": [
571 [
572 315,
573 324
574 ],
575 [
576 339,
577 339
578 ]
579 ],
580 "statement": "For every finite list of admitted events, running updateBits from encode(V) equals encoding the iterated candidate filter, and readBits returns exactly the resulting target image. The empty event list is included.",
581 "declarations": [
582 {
583 "name": "Komorebi.MachineTheory.PartitionCorrection.bits_finite_continuation",
584 "kind": "theorem",
585 "file": "MachineTheory/OccupancyBinary.lean",
586 "line": 70,
587 "actual_axioms": [
588 "propext",
589 "Classical.choice",
590 "Quot.sound"
591 ]
592 },
593 {
594 "name": "Komorebi.MachineTheory.PartitionCorrection.bits_readout_continuation",
595 "kind": "theorem",
596 "file": "MachineTheory/OccupancyBinary.lean",
597 "line": 80,
598 "actual_axioms": [
599 "propext",
600 "Classical.choice",
601 "Quot.sound"
602 ]
603 }
604 ]
605 },
606 {
607 "id": "binary_necessity",
608 "clause": "Every exact fixed-width b-bit memory needs at least r bits",
609 "scope": "source theorem",
610 "source_lines": [
611 [
612 315,
613 324
614 ],
615 [
616 336,
617 339
618 ]
619 ],
620 "statement": "For arbitrary encoder \u03c1 : Set \u03a9 \u2192 (Fin b \u2192 Bool), readout q, and deterministic step with q(\u03c1(V))=t(V) and step(e,\u03c1(V))=\u03c1(V\u2229e) for all V,e, the map S \u21a6 \u03c1(realize(S)) is injective. Hence 2^r \u2264 2^b and r \u2264 b.",
621 "declarations": [
622 {
623 "name": "Komorebi.MachineTheory.PartitionCorrection.exact_bits_occupancy_injective",
624 "kind": "theorem",
625 "file": "MachineTheory/OccupancyBinary.lean",
626 "line": 88,
627 "actual_axioms": [
628 "propext",
629 "Classical.choice",
630 "Quot.sound"
631 ]
632 },
633 {
634 "name": "Komorebi.MachineTheory.PartitionCorrection.fixed_bits_necessary",
635 "kind": "theorem",
636 "file": "MachineTheory/OccupancyBinary.lean",
637 "line": 100,
638 "actual_axioms": [
639 "propext",
640 "Classical.choice",
641 "Quot.sound"
642 ]
643 }
644 ],
645 "correspondence_notes": [
646 "The injection is proved using inherited any_exact_memory_separates and the new signature/occupancy classification. Minimality is a conclusion, not a supplied certificate.",
647 "The claim is limited to exact deterministic fixed-width binary state on all candidate subsets. It gives no variable-length, average-bit, approximate, randomized, time, or space-complexity lower bound."
648 ]
649 },
650 {
651 "id": "raw_source_endpoint",
652 "clause": "Raw source partition and target endpoint",
653 "scope": "source theorem",
654 "source_lines": [
655 [
656 96,
657 96
658 ],
659 [
660 329,
661 340
662 ]
663 ],
664 "statement": "For finite \u03a9, raw c : \u03a9 \u2192 I, raw t : \u03a9 \u2192 Y, and surjectivity of c, partition_correction_memory packages the count, signature classification, exact r-bit read/update laws, and universal fixed-width lower bound.",
665 "declarations": [
666 {
667 "name": "Komorebi.MachineTheory.PartitionCorrection.partition_correction_memory",
668 "kind": "theorem",
669 "file": "MachineTheory/OccupancyBinary.lean",
670 "line": 118,
671 "actual_axioms": [
672 "propext",
673 "Classical.choice",
674 "Quot.sound"
675 ]
676 }
677 ],
678 "correspondence_notes": [
679 "The source assumes nonempty \u03a9 and nonempty codomains. The Lean result is stronger: it does not require those typeclass hypotheses and also permits \u03a9=\u2205 when the supplied maps and surjectivity are possible. For nonempty \u03a9 the maps already imply nonempty I and Y.",
680 "Actual equivalences and arbitrary finite-continuation endpoints remain explicit separate declarations, rather than being hidden in this conjunctive theorem."
681 ]
682 },
683 {
684 "id": "sensor_counts",
685 "clause": "The source eight-world, four-pair sensor instance",
686 "scope": "source example",
687 "source_lines": [
688 [
689 343,
690 343
691 ]
692 ],
693 "statement": "SensorWorld is Bool \u00d7 Bool \u00d7 Bool, c(b,s,n)=(b,s), t(b,s,n)=b. The cell map is onto, \u03a9 has 8 elements, D is equivalent to Bool \u00d7 Bool and has 4 elements, attained signatures number 16, and an exact 3-bit memory is impossible.",
694 "declarations": [
695 {
696 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.SensorWorld",
697 "kind": "abbrev",
698 "file": "MachineTheory/OccupancyExamples.lean",
699 "line": 14,
700 "actual_axioms": []
701 },
702 {
703 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensorCell",
704 "kind": "def",
705 "file": "MachineTheory/OccupancyExamples.lean",
706 "line": 16,
707 "actual_axioms": []
708 },
709 {
710 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensorTarget",
711 "kind": "def",
712 "file": "MachineTheory/OccupancyExamples.lean",
713 "line": 17,
714 "actual_axioms": []
715 },
716 {
717 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensorCell_surjective",
718 "kind": "theorem",
719 "file": "MachineTheory/OccupancyExamples.lean",
720 "line": 19,
721 "actual_axioms": []
722 },
723 {
724 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensorPairEquiv",
725 "kind": "def",
726 "file": "MachineTheory/OccupancyExamples.lean",
727 "line": 23,
728 "actual_axioms": []
729 },
730 {
731 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_world_count",
732 "kind": "theorem",
733 "file": "MachineTheory/OccupancyExamples.lean",
734 "line": 38,
735 "actual_axioms": [
736 "propext",
737 "Classical.choice",
738 "Quot.sound"
739 ]
740 },
741 {
742 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_pair_count",
743 "kind": "theorem",
744 "file": "MachineTheory/OccupancyExamples.lean",
745 "line": 34,
746 "actual_axioms": [
747 "propext",
748 "Classical.choice",
749 "Quot.sound"
750 ]
751 },
752 {
753 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_signature_count",
754 "kind": "theorem",
755 "file": "MachineTheory/OccupancyExamples.lean",
756 "line": 40,
757 "actual_axioms": [
758 "propext",
759 "Classical.choice",
760 "Quot.sound"
761 ]
762 },
763 {
764 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_no_three_bit_memory",
765 "kind": "theorem",
766 "file": "MachineTheory/OccupancyExamples.lean",
767 "line": 45,
768 "actual_axioms": [
769 "propext",
770 "Classical.choice",
771 "Quot.sound"
772 ]
773 }
774 ]
775 },
776 {
777 "id": "sensor_correction_collision",
778 "clause": "Current targets lose calibration associations",
779 "scope": "source example",
780 "source_lines": [
781 [
782 343,
783 349
784 ]
785 ],
786 "statement": "The source V={(0,0,0),(1,1,0)} and W={(0,1,0),(1,0,0)} have equal present target images. Filtering by s=0 leaves the respective singleton worlds (0,0,0) and (1,0,0), so their correction signatures differ.",
787 "declarations": [
788 {
789 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensorV",
790 "kind": "def",
791 "file": "MachineTheory/OccupancyExamples.lean",
792 "line": 56,
793 "actual_axioms": []
794 },
795 {
796 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensorW",
797 "kind": "def",
798 "file": "MachineTheory/OccupancyExamples.lean",
799 "line": 57,
800 "actual_axioms": []
801 },
802 {
803 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.calibrationCells",
804 "kind": "def",
805 "file": "MachineTheory/OccupancyExamples.lean",
806 "line": 58,
807 "actual_axioms": []
808 },
809 {
810 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_present_targets_equal",
811 "kind": "theorem",
812 "file": "MachineTheory/OccupancyExamples.lean",
813 "line": 60,
814 "actual_axioms": [
815 "propext",
816 "Classical.choice",
817 "Quot.sound"
818 ]
819 },
820 {
821 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_filter_V",
822 "kind": "theorem",
823 "file": "MachineTheory/OccupancyExamples.lean",
824 "line": 63,
825 "actual_axioms": [
826 "propext",
827 "Quot.sound"
828 ]
829 },
830 {
831 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_filter_W",
832 "kind": "theorem",
833 "file": "MachineTheory/OccupancyExamples.lean",
834 "line": 69,
835 "actual_axioms": [
836 "propext",
837 "Quot.sound"
838 ]
839 },
840 {
841 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_signatures_ne",
842 "kind": "theorem",
843 "file": "MachineTheory/OccupancyExamples.lean",
844 "line": 75,
845 "actual_axioms": [
846 "propext",
847 "Classical.choice",
848 "Quot.sound"
849 ]
850 },
851 {
852 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.current_target_set_does_not_determine_correction",
853 "kind": "theorem",
854 "file": "MachineTheory/OccupancyExamples.lean",
855 "line": 86,
856 "actual_axioms": [
857 "propext",
858 "Classical.choice",
859 "Quot.sound"
860 ]
861 }
862 ]
863 },
864 {
865 "id": "empty_and_contradiction",
866 "clause": "Empty candidates, contradictory evidence, and the empty-world extension",
867 "scope": "required boundary controls plus a stronger empty-world extension",
868 "source_lines": [
869 [
870 96,
871 96
872 ],
873 [
874 303,
875 305
876 ]
877 ],
878 "statement": "The empty candidate has empty occupancy. Filtering any V by the admitted empty event gives \u2205, and its exact updated binary readout is \u2205. On \u03a9=Empty there are no attained pairs and exactly one attained signature.",
879 "declarations": [
880 {
881 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.empty_occupancy",
882 "kind": "theorem",
883 "file": "MachineTheory/OccupancyExamples.lean",
884 "line": 93,
885 "actual_axioms": [
886 "propext",
887 "Classical.choice",
888 "Quot.sound"
889 ]
890 },
891 {
892 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.contradictory_filter",
893 "kind": "theorem",
894 "file": "MachineTheory/OccupancyExamples.lean",
895 "line": 97,
896 "actual_axioms": [
897 "propext",
898 "Quot.sound"
899 ]
900 },
901 {
902 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.contradictory_binary_readout",
903 "kind": "theorem",
904 "file": "MachineTheory/OccupancyExamples.lean",
905 "line": 102,
906 "actual_axioms": [
907 "propext",
908 "Classical.choice",
909 "Quot.sound"
910 ]
911 },
912 {
913 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.emptyCell",
914 "kind": "def",
915 "file": "MachineTheory/OccupancyExamples.lean",
916 "line": 108,
917 "actual_axioms": []
918 },
919 {
920 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.emptyTarget",
921 "kind": "def",
922 "file": "MachineTheory/OccupancyExamples.lean",
923 "line": 109,
924 "actual_axioms": []
925 },
926 {
927 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.empty_pair_count",
928 "kind": "theorem",
929 "file": "MachineTheory/OccupancyExamples.lean",
930 "line": 111,
931 "actual_axioms": [
932 "propext",
933 "Classical.choice",
934 "Quot.sound"
935 ]
936 },
937 {
938 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.empty_signature_count",
939 "kind": "theorem",
940 "file": "MachineTheory/OccupancyExamples.lean",
941 "line": 117,
942 "actual_axioms": [
943 "propext",
944 "Classical.choice",
945 "Quot.sound"
946 ]
947 }
948 ],
949 "correspondence_notes": [
950 "\u03a9=\u2205 is an additional consistent case beyond the nonempty-world source convention. It is not used to weaken the nonempty source case."
951 ]
952 },
953 {
954 "id": "evidence_boundary",
955 "clause": "Exactly the admitted cell unions is essential",
956 "scope": "source counterexample and required removed-event boundary control",
957 "source_lines": [
958 [
959 329,
960 329
961 ],
962 [
963 341,
964 341
965 ],
966 [
967 351,
968 353
969 ]
970 ],
971 "statement": "For one nonempty cell with a constant target, D has 1 pair and 2 signatures; two singleton candidates have equal occupancy. A new singleton event splits the cell and distinguishes their signatures. Conversely, with distinct singleton cells those candidates have different occupancies, while retaining only \u2205 and \u03a9 merges their signatures.",
972 "declarations": [
973 {
974 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.oneCell",
975 "kind": "def",
976 "file": "MachineTheory/OccupancyExamples.lean",
977 "line": 122,
978 "actual_axioms": []
979 },
980 {
981 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.constantTarget",
982 "kind": "def",
983 "file": "MachineTheory/OccupancyExamples.lean",
984 "line": 123,
985 "actual_axioms": []
986 },
987 {
988 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.constantPairEquiv",
989 "kind": "def",
990 "file": "MachineTheory/OccupancyExamples.lean",
991 "line": 125,
992 "actual_axioms": []
993 },
994 {
995 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.one_cell_pair_count",
996 "kind": "theorem",
997 "file": "MachineTheory/OccupancyExamples.lean",
998 "line": 135,
999 "actual_axioms": [
1000 "propext",
1001 "Classical.choice",
1002 "Quot.sound"
1003 ]
1004 },
1005 {
1006 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.one_cell_signature_count",
1007 "kind": "theorem",
1008 "file": "MachineTheory/OccupancyExamples.lean",
1009 "line": 139,
1010 "actual_axioms": [
1011 "propext",
1012 "Classical.choice",
1013 "Quot.sound"
1014 ]
1015 },
1016 {
1017 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.constant_singletons_same_occupancy",
1018 "kind": "theorem",
1019 "file": "MachineTheory/OccupancyExamples.lean",
1020 "line": 144,
1021 "actual_axioms": [
1022 "propext",
1023 "Classical.choice",
1024 "Quot.sound"
1025 ]
1026 },
1027 {
1028 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.splitAlgebra",
1029 "kind": "def",
1030 "file": "MachineTheory/OccupancyExamples.lean",
1031 "line": 148,
1032 "actual_axioms": []
1033 },
1034 {
1035 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.splitEvent",
1036 "kind": "def",
1037 "file": "MachineTheory/OccupancyExamples.lean",
1038 "line": 153,
1039 "actual_axioms": []
1040 },
1041 {
1042 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.splitting_cell_changes_signature",
1043 "kind": "theorem",
1044 "file": "MachineTheory/OccupancyExamples.lean",
1045 "line": 155,
1046 "actual_axioms": [
1047 "propext",
1048 "Classical.choice",
1049 "Quot.sound"
1050 ]
1051 },
1052 {
1053 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.singleton_event_not_old_admitted",
1054 "kind": "theorem",
1055 "file": "MachineTheory/OccupancyExamples.lean",
1056 "line": 162,
1057 "actual_axioms": [
1058 "propext"
1059 ]
1060 },
1061 {
1062 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.separateCells",
1063 "kind": "def",
1064 "file": "MachineTheory/OccupancyExamples.lean",
1065 "line": 173,
1066 "actual_axioms": []
1067 },
1068 {
1069 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.separate_singletons_different_occupancy",
1070 "kind": "theorem",
1071 "file": "MachineTheory/OccupancyExamples.lean",
1072 "line": 175,
1073 "actual_axioms": []
1074 },
1075 {
1076 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.missing_cells_merges_signatures",
1077 "kind": "theorem",
1078 "file": "MachineTheory/OccupancyExamples.lean",
1079 "line": 189,
1080 "actual_axioms": [
1081 "propext",
1082 "Classical.choice",
1083 "Quot.sound"
1084 ]
1085 }
1086 ],
1087 "correspondence_notes": [
1088 "These concrete boundary lemmas test both adding a cell-splitting event and omitting the individual-cell events required by the classification proof. They do not reclassify a different evidence family as the original partition contract."
1089 ]
1090 },
1091 {
1092 "id": "target_boundaries",
1093 "clause": "Multiple targets per cell, shared targets across cells, and unattained values",
1094 "scope": "required target/cell boundary controls",
1095 "source_lines": [
1096 [
1097 96,
1098 96
1099 ],
1100 [
1101 331,
1102 333
1103 ]
1104 ],
1105 "statement": "For \u03a9=Bool \u00d7 Bool with cell the first and target the second coordinate, every cell meets both target values and both target values occur in both cells: D has 4 pairs and 16 signatures. For the Nat-valued target with range {0,1}, value 2 is unattained and no attained pair has target coordinate 2.",
1106 "declarations": [
1107 {
1108 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.multiCell",
1109 "kind": "def",
1110 "file": "MachineTheory/OccupancyExamples.lean",
1111 "line": 195,
1112 "actual_axioms": []
1113 },
1114 {
1115 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.multiTarget",
1116 "kind": "def",
1117 "file": "MachineTheory/OccupancyExamples.lean",
1118 "line": 196,
1119 "actual_axioms": []
1120 },
1121 {
1122 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.multiPairEquiv",
1123 "kind": "def",
1124 "file": "MachineTheory/OccupancyExamples.lean",
1125 "line": 198,
1126 "actual_axioms": []
1127 },
1128 {
1129 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.multi_target_pair_count",
1130 "kind": "theorem",
1131 "file": "MachineTheory/OccupancyExamples.lean",
1132 "line": 204,
1133 "actual_axioms": [
1134 "propext",
1135 "Classical.choice",
1136 "Quot.sound"
1137 ]
1138 },
1139 {
1140 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.multi_target_signature_count",
1141 "kind": "theorem",
1142 "file": "MachineTheory/OccupancyExamples.lean",
1143 "line": 208,
1144 "actual_axioms": [
1145 "propext",
1146 "Classical.choice",
1147 "Quot.sound"
1148 ]
1149 },
1150 {
1151 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.natTarget",
1152 "kind": "def",
1153 "file": "MachineTheory/OccupancyExamples.lean",
1154 "line": 213,
1155 "actual_axioms": []
1156 },
1157 {
1158 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.target_two_unattained",
1159 "kind": "theorem",
1160 "file": "MachineTheory/OccupancyExamples.lean",
1161 "line": 215,
1162 "actual_axioms": [
1163 "propext"
1164 ]
1165 },
1166 {
1167 "name": "Komorebi.MachineTheory.PartitionCorrection.Examples.no_unattained_pair",
1168 "kind": "theorem",
1169 "file": "MachineTheory/OccupancyExamples.lean",
1170 "line": 219,
1171 "actual_axioms": [
1172 "propext"
1173 ]
1174 }
1175 ]
1176 }
1177 ],
1178 "scope_limits": [
1179 "This document does not assert source acceptance or a 27/27 correspondence total.",
1180 "No external attribution to [GA], Corollary 5.3, is verified here; the supplied source corollary is the target.",
1181 "Universal exact Lean results and finite sanity computations are distinct evidence classes. No finite enumeration substitutes for the universal theorem.",
1182 "The bit lower bound concerns exact deterministic fixed-width state for every candidate subset, not variable-length or average encoding, approximation, or runtime performance."
1183 ],
1184 "completed_finalization": [
1185 "Recheck all module, source, API, registry, and independent-review pins against the final frozen source snapshot.",
1186 "Bind actual transitive-axiom records for every mapped authored declaration and record actual allowed-axiom results.",
1187 "Bind the two sequential cold gate receipts, independent-snapshot provenance, own-kernel replay receipts, negative-control diagnostics, and production-object comparison.",
1188 "Update draft status only after the coordinator establishes all restart-spec acceptance conditions."
1189 ],
1190 "actual_axioms_by_endpoint": {
1191 "Komorebi.MachineTheory.PartitionCorrection.partition_correction_memory": [
1192 "propext",
1193 "Classical.choice",
1194 "Quot.sound"
1195 ],
1196 "Komorebi.MachineTheory.PartitionCorrection.signature_eq_iff_occupancy_eq": [
1197 "propext",
1198 "Quot.sound"
1199 ],
1200 "Komorebi.MachineTheory.PartitionCorrection.occupancy_realize": [
1201 "propext",
1202 "Classical.choice",
1203 "Quot.sound"
1204 ],
1205 "Komorebi.MachineTheory.PartitionCorrection.fromOccupancy_bijective": [
1206 "propext",
1207 "Classical.choice",
1208 "Quot.sound"
1209 ],
1210 "Komorebi.MachineTheory.PartitionCorrection.memoryEquiv_remember": [
1211 "propext",
1212 "Classical.choice",
1213 "Quot.sound"
1214 ],
1215 "Komorebi.MachineTheory.PartitionCorrection.card_memory": [
1216 "propext",
1217 "Classical.choice",
1218 "Quot.sound"
1219 ],
1220 "Komorebi.MachineTheory.PartitionCorrection.fixed_bits_necessary": [
1221 "propext",
1222 "Classical.choice",
1223 "Quot.sound"
1224 ],
1225 "Komorebi.MachineTheory.PartitionCorrection.bits_finite_continuation": [
1226 "propext",
1227 "Classical.choice",
1228 "Quot.sound"
1229 ],
1230 "Komorebi.MachineTheory.PartitionCorrection.bits_readout_continuation": [
1231 "propext",
1232 "Classical.choice",
1233 "Quot.sound"
1234 ],
1235 "Komorebi.MachineTheory.PartitionCorrection.nonempty_cells_iff_surjective": [],
1236 "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_signature_count": [
1237 "propext",
1238 "Classical.choice",
1239 "Quot.sound"
1240 ],
1241 "Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_no_three_bit_memory": [
1242 "propext",
1243 "Classical.choice",
1244 "Quot.sound"
1245 ]
1246 }
1247 }
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: f2088f0e1186ff9c7e3a8ce644c48deaaff68f90efeecd376f639fe3b5a15e00