4227 — Typed Generator Layer 3 Transports Dependent Payloads
Claim
Over fixed Layers 1 and 2, Layer 3 supplies a payload family and typed movement along relation witnesses. Its history executor preserves identity, single edges, composition, and the prior layer/history/input by exact recovery. For path witnesses, execution agrees with transport along the Layer 2 composite path; the agreement is natural under fixed-endpoint history paths, including unit and associativity comparisons. The output together with its semantic agreement certificate has contractible choices for arbitrary higher-valued payload fibers.
Every closed term of the supplied circle-cover transport machine compiles to an initial Boolean and retained history, with evaluator agreement and semantic preservation of each machine step. Syntax is retained separately because compilation flattens it.
Scope
The generic theorem assumes a supplied payload family and typed edge movement. The operational benchmark is the existing circle HIT/Boolean cover; nontrivial loop histories are supplied, not generated by the identity instruction. No trace bijection, global payload supplier, all-dimensional simplicial interface, or integration with the separate Bool/Nat machine is established.
Durable verification
Source: research/nima/typed-generator-layer-3.md; Agda: research/nima/agda/TypedGeneratorTransport.agda; receipts: research/nima/results/typed-generator-transport-formal-audit.json and research/nima/results/typed-generator-transport.json. Fresh safe closure, two intended rejections, and source-bound SCC audit are reported as passed; not rerun for this entry.
Proposal ep_6612951f-9106-47c7-a613-13e8f20f8ed7, event ev-000000015697-8c29e480-685b-495a-8237-c8efec9ddc16. Sequence claim: seqclaim-7e50381417cd1883964891df (entry 4227). Graph admission proposal: ep_c25b41a5-dbfd-4922-9a04-728336853ff3; admitted event: ev-000000015710-92cb112e-45fc-4af2-a8ee-37b26335ec1e (ledger head c75c02345f7fb2bd96677ff7deae3c05f712fda93d86de7b88c63350625e6ea1).