# Source-to-Lean map — cumulative Block 19

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.

## 1.1 — A record determines a target exactly on its fibres
Source `r:factor`, original printed page 1, lines [98, 106]. Status: `KERNEL_CHECKED_BLOCK01`.

- `Komorebi.MachineTheory.decoder_exists_iff`
- `Komorebi.MachineTheory.no_decoder_of_collision`

## 1.2 — Evidence-initialized behavioral state
Source `r:behavior`, original printed page 2, lines [146, 157]. Status: `KERNEL_CHECKED_BLOCK01`.

- `Komorebi.MachineTheory.evidence_initialized_predictor_iff`
- `Komorebi.MachineTheory.Predictor.record_sufficient`
- `Komorebi.MachineTheory.Predictor.minimal_initialized_card`
- `Komorebi.MachineTheory.canonical_initialized_card`

## 2.1 — Exact accounting of the discarded excursion
Source `r:packet`, original printed page 4, lines [183, 192]. Status: `KERNEL_CHECKED_BLOCK01`.

- `Komorebi.MachineTheory.split_encoding_comp`
- `Komorebi.MachineTheory.hidden_return_identity`
- `Komorebi.MachineTheory.compressed_comp_iff_no_return`
- `Komorebi.MachineTheory.split_projector_idempotent`
- `Komorebi.MachineTheory.compression_projector_idempotent`

## 2.3 — Forward transport of a reusable method
Source `r:transport`, original printed page 5, lines [204, 218]. Status: `KERNEL_CHECKED_BLOCK01`.

- `Komorebi.MachineTheory.forward_transport`
- `Komorebi.MachineTheory.forward_output`
- `Komorebi.MachineTheory.invariant_forward_transport`
- `Komorebi.MachineTheory.invariant_forward_output`

## 2.4 — A common observable quotient
Source `r:common`, original printed page 5, lines [233, 250]. Status: `KERNEL_CHECKED_BLOCK17`.

- `Komorebi.MachineTheory.CommonQuotient.source_core24`
- `Komorebi.MachineTheory.CommonQuotient.source_core24_reference`
- `Komorebi.MachineTheory.CommonQuotient.agreement_iff_invisible`
- `Komorebi.MachineTheory.CommonQuotient.agreement_iff_commonModel`
- `Komorebi.MachineTheory.CommonQuotient.switching_output`
- `Komorebi.MachineTheory.CommonQuotient.stage_finrank_eq`

## 2.5 — When complete packets are genuine probability components
Source `r:positive-packets`, original printed page 6, lines [267, 279]. Status: `KERNEL_CHECKED_BLOCK18`.

- `Komorebi.MachineTheory.PositivePackets.source_core25`
- `Komorebi.MachineTheory.PositivePackets.sum_positive_weights_one`
- `Komorebi.MachineTheory.PositivePackets.Coordinate.source_core25_coordinate`
- `Komorebi.MachineTheory.PositivePackets.Coordinate.classification_iff`
- `Komorebi.MachineTheory.PositivePackets.Transport.source_coordinate_change`

## 3.1 — Minimal exact memory for a correction contract
Source `r:memory`, original printed page 8, lines [314, 325]. Status: `KERNEL_CHECKED_BLOCK01`.

- `Komorebi.MachineTheory.EvidenceAlgebra.signature_congruence`
- `Komorebi.MachineTheory.EvidenceAlgebra.memory_readout_continuation`
- `Komorebi.MachineTheory.EvidenceAlgebra.memory_universal_property`
- `Komorebi.MachineTheory.EvidenceAlgebra.memory_minimal_card`
- `Komorebi.MachineTheory.EvidenceAlgebra.signature_empty`

## 3.2 — The size of partition correction memory
Source `r:occupancy`, original printed page 9, lines [335, 340]. Status: `KERNEL_CHECKED_BLOCK19`.

- `Komorebi.MachineTheory.PartitionCorrection.partition_correction_memory`
- `Komorebi.MachineTheory.PartitionCorrection.signature_eq_iff_occupancy_eq`
- `Komorebi.MachineTheory.PartitionCorrection.occupancy_realize`
- `Komorebi.MachineTheory.PartitionCorrection.fromOccupancy_bijective`
- `Komorebi.MachineTheory.PartitionCorrection.memoryEquiv_remember`
- `Komorebi.MachineTheory.PartitionCorrection.card_memory`
- `Komorebi.MachineTheory.PartitionCorrection.fixed_bits_necessary`
- `Komorebi.MachineTheory.PartitionCorrection.bits_finite_continuation`
- `Komorebi.MachineTheory.PartitionCorrection.bits_readout_continuation`
- `Komorebi.MachineTheory.PartitionCorrection.nonempty_cells_iff_surjective`
- `Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_signature_count`
- `Komorebi.MachineTheory.PartitionCorrection.Examples.sensor_no_three_bit_memory`

## 3.4 — When a report preserves every Bayesian correction
Source `r:bayes`, original printed page 9, lines [364, 385]. Status: `KERNEL_CHECKED_BLOCK02`.

- `Komorebi.MachineTheory.Bayes.ReportingModel.all_iff_full_support_prior`
- `Komorebi.MachineTheory.Bayes.ReportingModel.all_iff_exists_full_support`
- `Komorebi.MachineTheory.Bayes.ReportingModel.all_iff_reconstruction`
- `Komorebi.MachineTheory.Bayes.ReportingModel.reconstructs_of_full_support`
- `Komorebi.MachineTheory.Bayes.ReportingModel.preservesAll_of_reconstructs`

## 3.5 — Least refinement closed under prediction and correction
Source `r:joint-refinement`, original printed page 11, lines [405, 422]. Status: `KERNEL_CHECKED_BLOCK02`.

- `Komorebi.MachineTheory.BayesianLumping.likelihood_constant_on_fibres`
- `Komorebi.MachineTheory.BayesianLumping.fixed_positive_coarse_iff`
- `Komorebi.MachineTheory.Refinement.step_rel_iff`
- `Komorebi.MachineTheory.Refinement.bounded_stabilization`
- `Komorebi.MachineTheory.Refinement.stopIndex_bound`
- `Komorebi.MachineTheory.Refinement.stable_iff_prediction`
- `Komorebi.MachineTheory.Refinement.admissible_iff`
- `Komorebi.MachineTheory.Refinement.least_prediction_correction_refinement`

## 3.6 — One quotient for reports, posteriors, and feedback
Source `r:instrument`, original printed page 12, lines [445, 466]. Status: `KERNEL_CHECKED_BLOCK01`.

- `Komorebi.MachineTheory.Instrument.quotient_exists_iff`
- `Komorebi.MachineTheory.Instrument.quotient_unique`
- `Komorebi.MachineTheory.Instrument.instrument_iff_reports_and_posteriors`
- `Komorebi.MachineTheory.Instrument.quotient_feedback_law`
- `Komorebi.MachineTheory.Instrument.totalHistoryMass_eq`
- `Komorebi.MachineTheory.Instrument.positive_history_posterior_dist`
- `Komorebi.MachineTheory.Instrument.stopped_feedback`
- `Komorebi.MachineTheory.Instrument.stoppedAndSurvivingMass_eq`

## 3.8 — A whole-history bound with an explicit conditioning cost
Source `r:history-bound`, original printed page 13, lines [483, 503]. Status: `KERNEL_CHECKED_BLOCK04`.

- `Komorebi.MachineTheory.ApproximateHistory.whole_history_bound`
- `Komorebi.MachineTheory.ApproximateHistory.observed_history_bound`
- `Komorebi.MachineTheory.ApproximateHistory.conditional_final_bound`
- `Komorebi.MachineTheory.ApproximateHistory.history_event_positive`
- `Komorebi.MachineTheory.Variation.condition_bound`

## 4.1 — A decision bound for one actual approximation chain
Source `r:risk`, original printed page 15, lines [533, 550]. Status: `KERNEL_CHECKED_BLOCK05`.

- `Komorebi.MachineTheory.ResponseDecision.decision_error_global`
- `Komorebi.MachineTheory.ResponseDecision.metric_minimizers_exist`
- `Komorebi.MachineTheory.ResponseDecision.regret_to_minimum`
- `Komorebi.MachineTheory.ResponseDecision.unique_minimizer_transfer`
- `Komorebi.MachineTheory.ResponseDecision.risk_threshold`

## 4.2 — A common artifact for fixed recipients
Source `r:recipient`, original printed page 16, lines [565, 574]. Status: `KERNEL_CHECKED_BLOCK06`.

- `Komorebi.MachineTheory.Recipient.encoder_exists_iff`
- `Komorebi.MachineTheory.Recipient.cardinality_budget_iff`
- `Komorebi.MachineTheory.Recipient.minimum_image_eq_cover`
- `Komorebi.MachineTheory.Recipient.minimum_common_artifact`
- `Komorebi.MachineTheory.RecipientExecution.Audience.common_artifact_iff`

## 5.1 — Exact joint feasibility for explicit controllers
Source `r:inquiry`, original printed page 17, lines [611, 618]. Status: `KERNEL_CHECKED_BLOCK07`.

- `Komorebi.MachineTheory.HardInquiry.Model.exact_frontier`
- `Komorebi.MachineTheory.HardInquiry.Model.joint_budget_iff`
- `Komorebi.MachineTheory.HardInquiry.Model.solve_witness`
- `Komorebi.MachineTheory.HardInquiry.Model.backup_dominates`
- `Komorebi.MachineTheory.HardInquiry.Model.compute_eq_solve`
- `Komorebi.MachineTheory.HardInquiry.Model.execution_sound`
- `Komorebi.MachineTheory.HardInquiry.Model.worst_coordinate_attained`
- `Komorebi.MachineTheory.HardInquiry.Model.profile_records`
- `Komorebi.MachineTheory.HardInquiry.AudienceBridge.recipient_inquiry`
- `Komorebi.MachineTheory.HardExamples.four_frontier_all`
- `Komorebi.MachineTheory.HardExamples.four_no_mixed_budget`
- `Komorebi.MachineTheory.HardControls.sensor_recipient_execution`

## 5.3 — A candidate attaining both lower bounds is optimal
Source `r:lowerbound`, original printed page 18, lines [635, 642]. Status: `KERNEL_CHECKED_BLOCK08`.

- `Komorebi.MachineTheory.BinaryDiagnosis.binary_lower_bounds`
- `Komorebi.MachineTheory.BinaryDiagnosis.records_exact`
- `Komorebi.MachineTheory.BinaryDiagnosis.actual_run_lower_bound`
- `Komorebi.MachineTheory.BinaryDiagnosis.checked_candidate_closes_frontier`
- `Komorebi.MachineTheory.BinaryDiagnosis.admitted_frontier`
- `Komorebi.MachineTheory.BinaryDiagnosis.admitted_budget`

## 5.4 — The same compressed belief supports the same inquiry
Source `r:belief-planning`, original printed page 20, lines [664, 675]. Status: `KERNEL_CHECKED_BLOCK03`.

- `Komorebi.MachineTheory.Planning.optimal_value_characterization`
- `Komorebi.MachineTheory.Planning.ExactMap.value_eq`
- `Komorebi.MachineTheory.Planning.ExactMap.firstValue_eq`
- `Komorebi.MachineTheory.Planning.ExactMap.optimalFirst_iff`
- `Komorebi.MachineTheory.Planning.ExactMap.feasible_iff`
- `Komorebi.MachineTheory.Planning.ExactMap.evaluate_eq`
- `Komorebi.MachineTheory.Planning.ExactMap.common_minimizing_tree`
- `Komorebi.MachineTheory.BeliefPlanning.compressed_belief_planning`
- `Komorebi.MachineTheory.BeliefPlanning.common_optimal_inquiry`
- `Komorebi.MachineTheory.BeliefPlanning.constructed_quotient_planning`
- `Komorebi.MachineTheory.Planning.ExactMap.optimalStop_iff`

## 5.6 — Uniform model error controls a changed policy
Source `r:policy-error`, original printed page 22, lines [712, 730]. Status: `KERNEL_CHECKED_BLOCK04`.

- `Komorebi.MachineTheory.ApproximateDecision.same_policy_error`
- `Komorebi.MachineTheory.ApproximateDecision.uniform_policy_regret`
- `Komorebi.MachineTheory.ApproximateDecision.minimizing_policies_exist`
- `Komorebi.MachineTheory.ApproximateDecision.history_policy_error`
- `Komorebi.MachineTheory.ApproximateDecision.history_selected_policy_regret`

## 6.1 — What finite counterexamples establish
Source `r:cegis`, original printed page 23, lines [742, 747]. Status: `KERNEL_CHECKED_BLOCK09`.

- `Komorebi.MachineTheory.Synthesis.counterexample_guided_synthesis`
- `Komorebi.MachineTheory.Synthesis.accepted_first`
- `Komorebi.MachineTheory.Synthesis.exhaustion_iff`
- `Komorebi.MachineTheory.Synthesis.truthful_call_bound`
- `Komorebi.MachineTheory.Synthesis.truthful_outcome`
- `Komorebi.MachineTheory.Synthesis.no_unbounded_truthful_calls`
- `Komorebi.MachineTheory.Synthesis.resume_bounded`
- `Komorebi.MachineTheory.Synthesis.bounded_completion_sound`

## 6.2 — Ordered semantic compression preserves the teacher trace
Source `r:ordered`, original printed page 23, lines [759, 766]. Status: `KERNEL_CHECKED_BLOCK09`.

- `Komorebi.MachineTheory.Synthesis.ordered_compression`
- `Komorebi.MachineTheory.Synthesis.representative_search_complete`
- `Komorebi.MachineTheory.Synthesis.teacher_work_preserved`
- `Komorebi.MachineTheory.Synthesis.prepare_value`

## 6.4 — A sound prefix exclusion
Source `r:prefix`, original printed page 24, lines [781, 788]. Status: `KERNEL_CHECKED_BLOCK10`.

- `Komorebi.MachineTheory.PrefixScan.integer_completion_iff`
- `Komorebi.MachineTheory.OrderedCompiler.prefix_exclusion`
- `Komorebi.MachineTheory.OrderedCompiler.source_prefix_certificate`
- `Komorebi.MachineTheory.OrderedCompiler.admitted_search_sound_complete`
- `Komorebi.MachineTheory.OrderedCompiler.admitted_failure_iff_empty_frontier`

## 7.1 — Selective reuse with complete dependencies
Source `r:dependencies`, original printed page 26, lines [809, 814]. Status: `KERNEL_CHECKED_BLOCK11`.

- `Komorebi.MachineTheory.Dependency.System.selective_reuse`
- `Komorebi.MachineTheory.Dependency.System.restoration`
- `Komorebi.MachineTheory.Dependency.System.admitted_reuse_and_restoration`
- `Komorebi.MachineTheory.Dependency.closure_iff_reach`

## 7.3 — Which gains survive every admitted price?
Source `r:prices`, original printed page 27, lines [835, 840]. Status: `KERNEL_CHECKED_BLOCK12`.

- `Komorebi.MachineTheory.ResourcePrices.all_nonnegative_prices_iff`
- `Komorebi.MachineTheory.ResourcePrices.finite_price_minimum`
- `Komorebi.MachineTheory.ResourcePrices.listed_hull_minimizer`
- `Komorebi.MachineTheory.ResourcePrices.saving_net`
- `Komorebi.MachineTheory.PriceExamples.priced_scan`
- `Komorebi.MachineTheory.PriceExamples.robust_reuse_threshold`
- `Komorebi.MachineTheory.PriceRevision.restored_negative_real_saving`

## 7.4 — A conditional error budget for a lineage
Source `r:lineage`, original printed page 28, lines [848, 858]. Status: `KERNEL_CHECKED_BLOCK13`.

- `Komorebi.MachineTheory.Lineage.conditional_marginal_bound`
- `Komorebi.MachineTheory.Lineage.finite_lineage_bound`
- `Komorebi.MachineTheory.Lineage.lineage_bound`
- `Komorebi.MachineTheory.Lineage.lineage_ennreal_bound`
- `Komorebi.MachineTheory.Lineage.selected_lineage_bound`
- `Komorebi.MachineTheory.Lineage.stopped_selected_lineage_bound`
- `Komorebi.MachineTheory.Lineage.divergent_real_total_not_union_bound`

## 8.1 — Target-relative joint reconstruction
Source `r:reconstruction`, original printed page 29, lines [873, 878]. Status: `KERNEL_CHECKED_BLOCK14`.

- `Komorebi.MachineTheory.JointReconstruction.finite_joint_reconstruction`
- `Komorebi.MachineTheory.JointReconstruction.exists_decoder_iff_ker_le`
- `Komorebi.MachineTheory.JointReconstruction.exists_decoder_extending_imageDecoder`
- `Komorebi.MachineTheory.JointReconstruction.full_state_iff_injective`
- `Komorebi.MachineTheory.JointReconstruction.ker_stackRecords`
- `Komorebi.MachineTheory.JointReconstruction.stacked_decoder_iff`

## 8.2 — A quotient that preserves legal operations
Source `r:governance`, original printed page 29, lines [888, 898]. Status: `KERNEL_CHECKED_BLOCK15`.

- `Komorebi.MachineTheory.LegalQuotient.finite_source_legal_quotient`
- `Komorebi.MachineTheory.LegalQuotient.exists_quotient_iff`
- `Komorebi.MachineTheory.LegalQuotient.representativeQuotient_factors`
- `Komorebi.MachineTheory.LegalQuotient.quotient_unique`
- `Komorebi.MachineTheory.LegalQuotient.ofEnabled_reconstruct`
- `Komorebi.MachineTheory.LegalQuotient.finite_legal_quotient_sequences`
- `Komorebi.MachineTheory.LegalQuotient.Factors.execute_map`
- `Komorebi.MachineTheory.LegalQuotient.Factors.labels_eq`
- `Komorebi.MachineTheory.LegalQuotient.Factors.lift_execution`

## 8.3 — Safe continuation that retains an ending strategy
Source `r:ending`, original printed page 30, lines [918, 927]. Status: `KERNEL_CHECKED_BLOCK16_RECOVERY`.

- `Komorebi.MachineTheory.SafeEnding.ending_stabilizes`
- `Komorebi.MachineTheory.SafeEnding.running_stabilizes`
- `Komorebi.MachineTheory.SafeEnding.endRank_zero_iff`
- `Komorebi.MachineTheory.SafeEnding.rank_action`
- `Komorebi.MachineTheory.SafeEnding.ending_region_iff`
- `Komorebi.MachineTheory.SafeEnding.safe_continuation_iff`
- `Komorebi.MachineTheory.SafeEnding.source_core83`
- `Komorebi.MachineTheory.SafeEnding.command_rank_bound`
- `Komorebi.MachineTheory.SafeEnding.command_rank_arrival`
- `Komorebi.MachineTheory.SafeEnding.running_has_infinite_path`
- `Komorebi.MachineTheory.SafeEnding.ending_prefix_extends`