ASSUMPTION_REVIEW_BLOCK06.md
Machine Native Reasoning
ASSUMPTION_REVIEW_BLOCK06.md
1 # Block06 assumption and proof-obligation map
2
3 Source Core4.2, unchanged Reviewed Core0.2, printed p16, source lines565–574.
4
5 | Obligation | Formal object / proof route | Boundary |
6 |---|---|---|
7 | Accessible sender | Attained alpha; Valid | No hidden case argument or default on impossible inputs |
8 | Whole-fibre commonality | Common; valid_iff_common; encoder_exists_iff | Pairwise compatibility is insufficient |
9 | One artifact for all recipients | Audience.Accepts universally quantifies i after fixing c | Separate private messages do not satisfy this contract |
10 | Fixed actual decoder | Audience.run i accepts background i and artifact only | No synthesized replacement decoder |
11 | Output and resources | completed Result with output/work/peakSpace; permission conjunct | Counters are supplied execution semantics, not measured host work |
12 | Finite image | finite case type and attainedFintype | Alphabet may be larger; no efficient search inferred |
13 | Minimum exists | image_size_exists and cover_size_exists, Nat.find | Feasibility is explicit; empty cases handled |
14 | Minima coincide | encoder_within_iff; cardinality_budget_iff; minimum_image_eq_cover | A redundant codebook need not be exactly used |
15 | One witness | minimum_common_artifact | Does not splice separate optimum coordinates |
16 | Alphabet capacity | decoded_alphabet_bound | Decoder installation/storage still charged separately |
17 | Source example | xor_accepts_iff; xor_sender_valid; xor_minimum_codebook | Exact Bool XOR model, not learned language |
18 | Source collision | individually_possible_not_common | Every case soluble does not imply one accessible artifact |
19
20 All statements are complete Lean terms under the declared foundations; actual build and axiom acceptance are recorded by the current final/fresh receipts. These notes are project-authored review, not independent peer review.