Lossless backend audit grouping

Coalescing preserves every node id, operation, and complete capsule, in order and with repeats. Consequently, a grouped acceptance proof applies to every node in its source graph plan. These statements concern the planner and its declared contracts, not native kernel execution.

theorem NN.Backend.KernelGroup.canAppend_iff (group : KernelGroup) (kernel : IR.PlannedNodeKernel) : group.canAppend kernel = true ↔ group.op = kernel.op ∧ group.capsule = kernel.capsule

A group may absorb a node only when its operation and complete capsule agree.

theorem NN.Backend.IR.GraphKernelPlan.toCoalescedGroups_expands (plan : GraphKernelPlan) : Array.flatMap (fun (group : KernelGroup) => Array.map (fun (id : ℕ) => (id, group.op, group.capsule)) group.nodeIds) plan.toCoalescedGroups.groups = Array.map (fun (kernel : PlannedNodeKernel) => (kernel.nodeId, kernel.op, kernel.capsule)) plan.kernels

Expanding coalesced audit groups reproduces the original node ids, operations, and full capsules. Array equality preserves order and multiplicity, including repeated node ids.

theorem NN.Backend.IR.GraphKernelPlan.node_mem_coalesced (plan : GraphKernelPlan) (kernel : PlannedNodeKernel) (hkernel : kernel ∈ plan.kernels) : ∃ group ∈ plan.toCoalescedGroups.groups, kernel.nodeId ∈ group.nodeIds ∧ kernel.op = group.op ∧ kernel.capsule = group.capsule

Every original node occurs in a group with exactly its operation and capsule.

theorem NN.Backend.GroupedKernelPlan.acceptable_iff (plan : GroupedKernelPlan) (policy : KernelPolicy) : acceptable policy plan = true ↔ ∀ group ∈ plan.groups, PlannedKernel.acceptable policy group.toPlannedKernel = true

Group acceptance checks every projected operation and complete capsule.

theorem NN.Backend.IR.GraphKernelPlan.node_acceptable (plan : GraphKernelPlan) (policy : KernelPolicy) (haccepted : GroupedKernelPlan.acceptable policy plan.toCoalescedGroups = true) (kernel : PlannedNodeKernel) (hkernel : kernel ∈ plan.kernels) : PlannedKernel.acceptable policy { op := kernel.op, capsule := kernel.capsule } = true

Accepting the coalesced plan guarantees acceptance of each original node's capsule.

theorem NN.Backend.AcceptedGraphKernelPlan.node_acceptable (plan : AcceptedGraphKernelPlan) (kernel : IR.PlannedNodeKernel) (hkernel : kernel ∈ plan.graphPlan.kernels) : PlannedKernel.acceptable plan.policy { op := kernel.op, capsule := kernel.capsule } = true

Every node in an accepted graph plan passes the same complete policy and evidence gate.