Machine Native Reasoning

Download original file

Read the formatted document

1 # Source-to-Lean map — cumulative Block 19
2 
3 All 27 selected source statements have explicit endpoint targets. Admission is effective only after the complete current-source and independently extracted-source gates and their comparison pass. This source map alone is not a verification receipt. The unchanged source index fixes the statement identities.
4 
5 ## 1.1 — A record determines a target exactly on its fibres
6 Source `r:factor`, original printed page 1, lines [98, 106]. Status: `KERNEL_CHECKED_BLOCK01`.
7 
8 - `Komorebi.MachineTheory.decoder_exists_iff`
9 - `Komorebi.MachineTheory.no_decoder_of_collision`
10 
11 ## 1.2 — Evidence-initialized behavioral state
12 Source `r:behavior`, original printed page 2, lines [146, 157]. Status: `KERNEL_CHECKED_BLOCK01`.
13 
14 - `Komorebi.MachineTheory.evidence_initialized_predictor_iff`
15 - `Komorebi.MachineTheory.Predictor.record_sufficient`
16 - `Komorebi.MachineTheory.Predictor.minimal_initialized_card`
17 - `Komorebi.MachineTheory.canonical_initialized_card`
18 
19 ## 2.1 — Exact accounting of the discarded excursion
20 Source `r:packet`, original printed page 4, lines [183, 192]. Status: `KERNEL_CHECKED_BLOCK01`.
21 
22 - `Komorebi.MachineTheory.split_encoding_comp`
23 - `Komorebi.MachineTheory.hidden_return_identity`
24 - `Komorebi.MachineTheory.compressed_comp_iff_no_return`
25 - `Komorebi.MachineTheory.split_projector_idempotent`
26 - `Komorebi.MachineTheory.compression_projector_idempotent`
27 
28 ## 2.3 — Forward transport of a reusable method
29 Source `r:transport`, original printed page 5, lines [204, 218]. Status: `KERNEL_CHECKED_BLOCK01`.
30 
31 - `Komorebi.MachineTheory.forward_transport`
32 - `Komorebi.MachineTheory.forward_output`
33 - `Komorebi.MachineTheory.invariant_forward_transport`
34 - `Komorebi.MachineTheory.invariant_forward_output`
35 
36 ## 2.4 — A common observable quotient
37 Source `r:common`, original printed page 5, lines [233, 250]. Status: `KERNEL_CHECKED_BLOCK17`.
38 
39 - `Komorebi.MachineTheory.CommonQuotient.source_core24`
40 - `Komorebi.MachineTheory.CommonQuotient.source_core24_reference`
41 - `Komorebi.MachineTheory.CommonQuotient.agreement_iff_invisible`
42 - `Komorebi.MachineTheory.CommonQuotient.agreement_iff_commonModel`
43 - `Komorebi.MachineTheory.CommonQuotient.switching_output`
44 - `Komorebi.MachineTheory.CommonQuotient.stage_finrank_eq`
45 
46 ## 2.5 — When complete packets are genuine probability components
47 Source `r:positive-packets`, original printed page 6, lines [267, 279]. Status: `KERNEL_CHECKED_BLOCK18`.
48 
49 - `Komorebi.MachineTheory.PositivePackets.source_core25`
50 - `Komorebi.MachineTheory.PositivePackets.sum_positive_weights_one`
51 - `Komorebi.MachineTheory.PositivePackets.Coordinate.source_core25_coordinate`
52 - `Komorebi.MachineTheory.PositivePackets.Coordinate.classification_iff`
53 - `Komorebi.MachineTheory.PositivePackets.Transport.source_coordinate_change`
54 
55 ## 3.1 — Minimal exact memory for a correction contract
56 Source `r:memory`, original printed page 8, lines [314, 325]. Status: `KERNEL_CHECKED_BLOCK01`.
57 
58 - `Komorebi.MachineTheory.EvidenceAlgebra.signature_congruence`
59 - `Komorebi.MachineTheory.EvidenceAlgebra.memory_readout_continuation`
60 - `Komorebi.MachineTheory.EvidenceAlgebra.memory_universal_property`
61 - `Komorebi.MachineTheory.EvidenceAlgebra.memory_minimal_card`
62 - `Komorebi.MachineTheory.EvidenceAlgebra.signature_empty`
63 
64 ## 3.2 — The size of partition correction memory
65 Source `r:occupancy`, original printed page 9, lines [335, 340]. Status: `KERNEL_CHECKED_BLOCK19`.
66 
67 - `Komorebi.MachineTheory.PartitionCorrection.partition_correction_memory`
68 - `Komorebi.MachineTheory.PartitionCorrection.signature_eq_iff_occupancy_eq`
69 - `Komorebi.MachineTheory.PartitionCorrection.occupancy_realize`
70 - `Komorebi.MachineTheory.PartitionCorrection.fromOccupancy_bijective`
71 - `Komorebi.MachineTheory.PartitionCorrection.memoryEquiv_remember`
72 - `Komorebi.MachineTheory.PartitionCorrection.card_memory`
73 - `Komorebi.MachineTheory.PartitionCorrection.fixed_bits_necessary`
74 - `Komorebi.MachineTheory.PartitionCorrection.bits_finite_continuation`
75 - `Komorebi.MachineTheory.PartitionCorrection.bits_readout_continuation`
76 - `Komorebi.MachineTheory.PartitionCorrection.nonempty_cells_iff_surjective`
77 - `Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_signature_count`
78 - `Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_no_three_bit_memory`
79 
80 ## 3.4 — When a report preserves every Bayesian correction
81 Source `r:bayes`, original printed page 9, lines [364, 385]. Status: `KERNEL_CHECKED_BLOCK02`.
82 
83 - `Komorebi.MachineTheory.Bayes.ReportingModel.all_iff_full_support_prior`
84 - `Komorebi.MachineTheory.Bayes.ReportingModel.all_iff_exists_full_support`
85 - `Komorebi.MachineTheory.Bayes.ReportingModel.all_iff_reconstruction`
86 - `Komorebi.MachineTheory.Bayes.ReportingModel.reconstructs_of_full_support`
87 - `Komorebi.MachineTheory.Bayes.ReportingModel.preservesAll_of_reconstructs`
88 
89 ## 3.5 — Least refinement closed under prediction and correction
90 Source `r:joint-refinement`, original printed page 11, lines [405, 422]. Status: `KERNEL_CHECKED_BLOCK02`.
91 
92 - `Komorebi.MachineTheory.BayesianLumping.likelihood_constant_on_fibres`
93 - `Komorebi.MachineTheory.BayesianLumping.fixed_positive_coarse_iff`
94 - `Komorebi.MachineTheory.Refinement.step_rel_iff`
95 - `Komorebi.MachineTheory.Refinement.bounded_stabilization`
96 - `Komorebi.MachineTheory.Refinement.stopIndex_bound`
97 - `Komorebi.MachineTheory.Refinement.stable_iff_prediction`
98 - `Komorebi.MachineTheory.Refinement.admissible_iff`
99 - `Komorebi.MachineTheory.Refinement.least_prediction_correction_refinement`
100 
101 ## 3.6 — One quotient for reports, posteriors, and feedback
102 Source `r:instrument`, original printed page 12, lines [445, 466]. Status: `KERNEL_CHECKED_BLOCK01`.
103 
104 - `Komorebi.MachineTheory.Instrument.quotient_exists_iff`
105 - `Komorebi.MachineTheory.Instrument.quotient_unique`
106 - `Komorebi.MachineTheory.Instrument.instrument_iff_reports_and_posteriors`
107 - `Komorebi.MachineTheory.Instrument.quotient_feedback_law`
108 - `Komorebi.MachineTheory.Instrument.totalHistoryMass_eq`
109 - `Komorebi.MachineTheory.Instrument.positive_history_posterior_dist`
110 - `Komorebi.MachineTheory.Instrument.stopped_feedback`
111 - `Komorebi.MachineTheory.Instrument.stoppedAndSurvivingMass_eq`
112 
113 ## 3.8 — A whole-history bound with an explicit conditioning cost
114 Source `r:history-bound`, original printed page 13, lines [483, 503]. Status: `KERNEL_CHECKED_BLOCK04`.
115 
116 - `Komorebi.MachineTheory.ApproximateHistory.whole_history_bound`
117 - `Komorebi.MachineTheory.ApproximateHistory.observed_history_bound`
118 - `Komorebi.MachineTheory.ApproximateHistory.conditional_final_bound`
119 - `Komorebi.MachineTheory.ApproximateHistory.history_event_positive`
120 - `Komorebi.MachineTheory.Variation.condition_bound`
121 
122 ## 4.1 — A decision bound for one actual approximation chain
123 Source `r:risk`, original printed page 15, lines [533, 550]. Status: `KERNEL_CHECKED_BLOCK05`.
124 
125 - `Komorebi.MachineTheory.ResponseDecision.decision_error_global`
126 - `Komorebi.MachineTheory.ResponseDecision.metric_minimizers_exist`
127 - `Komorebi.MachineTheory.ResponseDecision.regret_to_minimum`
128 - `Komorebi.MachineTheory.ResponseDecision.unique_minimizer_transfer`
129 - `Komorebi.MachineTheory.ResponseDecision.risk_threshold`
130 
131 ## 4.2 — A common artifact for fixed recipients
132 Source `r:recipient`, original printed page 16, lines [565, 574]. Status: `KERNEL_CHECKED_BLOCK06`.
133 
134 - `Komorebi.MachineTheory.Recipient.encoder_exists_iff`
135 - `Komorebi.MachineTheory.Recipient.cardinality_budget_iff`
136 - `Komorebi.MachineTheory.Recipient.minimum_image_eq_cover`
137 - `Komorebi.MachineTheory.Recipient.minimum_common_artifact`
138 - `Komorebi.MachineTheory.RecipientExecution.Audience.common_artifact_iff`
139 
140 ## 5.1 — Exact joint feasibility for explicit controllers
141 Source `r:inquiry`, original printed page 17, lines [611, 618]. Status: `KERNEL_CHECKED_BLOCK07`.
142 
143 - `Komorebi.MachineTheory.HardInquiry.Model.exact_frontier`
144 - `Komorebi.MachineTheory.HardInquiry.Model.joint_budget_iff`
145 - `Komorebi.MachineTheory.HardInquiry.Model.solve_witness`
146 - `Komorebi.MachineTheory.HardInquiry.Model.backup_dominates`
147 - `Komorebi.MachineTheory.HardInquiry.Model.compute_eq_solve`
148 - `Komorebi.MachineTheory.HardInquiry.Model.execution_sound`
149 - `Komorebi.MachineTheory.HardInquiry.Model.worst_coordinate_attained`
150 - `Komorebi.MachineTheory.HardInquiry.Model.profile_records`
151 - `Komorebi.MachineTheory.HardInquiry.AudienceBridge.recipient_inquiry`
152 - `Komorebi.MachineTheory.HardExamples.four_frontier_all`
153 - `Komorebi.MachineTheory.HardExamples.four_no_mixed_budget`
154 - `Komorebi.MachineTheory.HardControls.sensor_recipient_execution`
155 
156 ## 5.3 — A candidate attaining both lower bounds is optimal
157 Source `r:lowerbound`, original printed page 18, lines [635, 642]. Status: `KERNEL_CHECKED_BLOCK08`.
158 
159 - `Komorebi.MachineTheory.BinaryDiagnosis.binary_lower_bounds`
160 - `Komorebi.MachineTheory.BinaryDiagnosis.records_exact`
161 - `Komorebi.MachineTheory.BinaryDiagnosis.actual_run_lower_bound`
162 - `Komorebi.MachineTheory.BinaryDiagnosis.checked_candidate_closes_frontier`
163 - `Komorebi.MachineTheory.BinaryDiagnosis.admitted_frontier`
164 - `Komorebi.MachineTheory.BinaryDiagnosis.admitted_budget`
165 
166 ## 5.4 — The same compressed belief supports the same inquiry
167 Source `r:belief-planning`, original printed page 20, lines [664, 675]. Status: `KERNEL_CHECKED_BLOCK03`.
168 
169 - `Komorebi.MachineTheory.Planning.optimal_value_characterization`
170 - `Komorebi.MachineTheory.Planning.ExactMap.value_eq`
171 - `Komorebi.MachineTheory.Planning.ExactMap.firstValue_eq`
172 - `Komorebi.MachineTheory.Planning.ExactMap.optimalFirst_iff`
173 - `Komorebi.MachineTheory.Planning.ExactMap.feasible_iff`
174 - `Komorebi.MachineTheory.Planning.ExactMap.evaluate_eq`
175 - `Komorebi.MachineTheory.Planning.ExactMap.common_minimizing_tree`
176 - `Komorebi.MachineTheory.BeliefPlanning.compressed_belief_planning`
177 - `Komorebi.MachineTheory.BeliefPlanning.common_optimal_inquiry`
178 - `Komorebi.MachineTheory.BeliefPlanning.constructed_quotient_planning`
179 - `Komorebi.MachineTheory.Planning.ExactMap.optimalStop_iff`
180 
181 ## 5.6 — Uniform model error controls a changed policy
182 Source `r:policy-error`, original printed page 22, lines [712, 730]. Status: `KERNEL_CHECKED_BLOCK04`.
183 
184 - `Komorebi.MachineTheory.ApproximateDecision.same_policy_error`
185 - `Komorebi.MachineTheory.ApproximateDecision.uniform_policy_regret`
186 - `Komorebi.MachineTheory.ApproximateDecision.minimizing_policies_exist`
187 - `Komorebi.MachineTheory.ApproximateDecision.history_policy_error`
188 - `Komorebi.MachineTheory.ApproximateDecision.history_selected_policy_regret`
189 
190 ## 6.1 — What finite counterexamples establish
191 Source `r:cegis`, original printed page 23, lines [742, 747]. Status: `KERNEL_CHECKED_BLOCK09`.
192 
193 - `Komorebi.MachineTheory.Synthesis.counterexample_guided_synthesis`
194 - `Komorebi.MachineTheory.Synthesis.accepted_first`
195 - `Komorebi.MachineTheory.Synthesis.exhaustion_iff`
196 - `Komorebi.MachineTheory.Synthesis.truthful_call_bound`
197 - `Komorebi.MachineTheory.Synthesis.truthful_outcome`
198 - `Komorebi.MachineTheory.Synthesis.no_unbounded_truthful_calls`
199 - `Komorebi.MachineTheory.Synthesis.resume_bounded`
200 - `Komorebi.MachineTheory.Synthesis.bounded_completion_sound`
201 
202 ## 6.2 — Ordered semantic compression preserves the teacher trace
203 Source `r:ordered`, original printed page 23, lines [759, 766]. Status: `KERNEL_CHECKED_BLOCK09`.
204 
205 - `Komorebi.MachineTheory.Synthesis.ordered_compression`
206 - `Komorebi.MachineTheory.Synthesis.representative_search_complete`
207 - `Komorebi.MachineTheory.Synthesis.teacher_work_preserved`
208 - `Komorebi.MachineTheory.Synthesis.prepare_value`
209 
210 ## 6.4 — A sound prefix exclusion
211 Source `r:prefix`, original printed page 24, lines [781, 788]. Status: `KERNEL_CHECKED_BLOCK10`.
212 
213 - `Komorebi.MachineTheory.PrefixScan.integer_completion_iff`
214 - `Komorebi.MachineTheory.OrderedCompiler.prefix_exclusion`
215 - `Komorebi.MachineTheory.OrderedCompiler.source_prefix_certificate`
216 - `Komorebi.MachineTheory.OrderedCompiler.admitted_search_sound_complete`
217 - `Komorebi.MachineTheory.OrderedCompiler.admitted_failure_iff_empty_frontier`
218 
219 ## 7.1 — Selective reuse with complete dependencies
220 Source `r:dependencies`, original printed page 26, lines [809, 814]. Status: `KERNEL_CHECKED_BLOCK11`.
221 
222 - `Komorebi.MachineTheory.Dependency.System.selective_reuse`
223 - `Komorebi.MachineTheory.Dependency.System.restoration`
224 - `Komorebi.MachineTheory.Dependency.System.admitted_reuse_and_restoration`
225 - `Komorebi.MachineTheory.Dependency.closure_iff_reach`
226 
227 ## 7.3 — Which gains survive every admitted price?
228 Source `r:prices`, original printed page 27, lines [835, 840]. Status: `KERNEL_CHECKED_BLOCK12`.
229 
230 - `Komorebi.MachineTheory.ResourcePrices.all_nonnegative_prices_iff`
231 - `Komorebi.MachineTheory.ResourcePrices.finite_price_minimum`
232 - `Komorebi.MachineTheory.ResourcePrices.listed_hull_minimizer`
233 - `Komorebi.MachineTheory.ResourcePrices.saving_net`
234 - `Komorebi.MachineTheory.PriceExamples.priced_scan`
235 - `Komorebi.MachineTheory.PriceExamples.robust_reuse_threshold`
236 - `Komorebi.MachineTheory.PriceRevision.restored_negative_real_saving`
237 
238 ## 7.4 — A conditional error budget for a lineage
239 Source `r:lineage`, original printed page 28, lines [848, 858]. Status: `KERNEL_CHECKED_BLOCK13`.
240 
241 - `Komorebi.MachineTheory.Lineage.conditional_marginal_bound`
242 - `Komorebi.MachineTheory.Lineage.finite_lineage_bound`
243 - `Komorebi.MachineTheory.Lineage.lineage_bound`
244 - `Komorebi.MachineTheory.Lineage.lineage_ennreal_bound`
245 - `Komorebi.MachineTheory.Lineage.selected_lineage_bound`
246 - `Komorebi.MachineTheory.Lineage.stopped_selected_lineage_bound`
247 - `Komorebi.MachineTheory.Lineage.divergent_real_total_not_union_bound`
248 
249 ## 8.1 — Target-relative joint reconstruction
250 Source `r:reconstruction`, original printed page 29, lines [873, 878]. Status: `KERNEL_CHECKED_BLOCK14`.
251 
252 - `Komorebi.MachineTheory.JointReconstruction.finite_joint_reconstruction`
253 - `Komorebi.MachineTheory.JointReconstruction.exists_decoder_iff_ker_le`
254 - `Komorebi.MachineTheory.JointReconstruction.exists_decoder_extending_imageDecoder`
255 - `Komorebi.MachineTheory.JointReconstruction.full_state_iff_injective`
256 - `Komorebi.MachineTheory.JointReconstruction.ker_stackRecords`
257 - `Komorebi.MachineTheory.JointReconstruction.stacked_decoder_iff`
258 
259 ## 8.2 — A quotient that preserves legal operations
260 Source `r:governance`, original printed page 29, lines [888, 898]. Status: `KERNEL_CHECKED_BLOCK15`.
261 
262 - `Komorebi.MachineTheory.LegalQuotient.finite_source_legal_quotient`
263 - `Komorebi.MachineTheory.LegalQuotient.exists_quotient_iff`
264 - `Komorebi.MachineTheory.LegalQuotient.representativeQuotient_factors`
265 - `Komorebi.MachineTheory.LegalQuotient.quotient_unique`
266 - `Komorebi.MachineTheory.LegalQuotient.ofEnabled_reconstruct`
267 - `Komorebi.MachineTheory.LegalQuotient.finite_legal_quotient_sequences`
268 - `Komorebi.MachineTheory.LegalQuotient.Factors.execute_map`
269 - `Komorebi.MachineTheory.LegalQuotient.Factors.labels_eq`
270 - `Komorebi.MachineTheory.LegalQuotient.Factors.lift_execution`
271 
272 ## 8.3 — Safe continuation that retains an ending strategy
273 Source `r:ending`, original printed page 30, lines [918, 927]. Status: `KERNEL_CHECKED_BLOCK16_RECOVERY`.
274 
275 - `Komorebi.MachineTheory.SafeEnding.ending_stabilizes`
276 - `Komorebi.MachineTheory.SafeEnding.running_stabilizes`
277 - `Komorebi.MachineTheory.SafeEnding.endRank_zero_iff`
278 - `Komorebi.MachineTheory.SafeEnding.rank_action`
279 - `Komorebi.MachineTheory.SafeEnding.ending_region_iff`
280 - `Komorebi.MachineTheory.SafeEnding.safe_continuation_iff`
281 - `Komorebi.MachineTheory.SafeEnding.source_core83`
282 - `Komorebi.MachineTheory.SafeEnding.command_rank_bound`
283 - `Komorebi.MachineTheory.SafeEnding.command_rank_arrival`
284 - `Komorebi.MachineTheory.SafeEnding.running_has_infinite_path`
285 - `Komorebi.MachineTheory.SafeEnding.ending_prefix_extends`
286 

Back to source controls