Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Seven physical row roles and exact T depletion

Abstract

Shared physical prefix proofs on seven distinct row roles.

The occurrence carrier is the disjoint sum of parent labels and literal dependent row indices. An embedding of Fin(7) selects the seven distinct prefix roles. The M5 consumer uses their inclusion in Fin(10); the general original-source consumer uses their inclusion in the natural row indices, restricted by its actual 2m-row physical partition.

PrefixArithmetic belongs to M5SourceArithmetic and contains exactly the source arithmetic through y, without a0 or an a0<=z premise. Its original arithmetic_geometry, canonical_mask_height, gate_limits and wj_geometry proofs are shared directly. M5 Arithmetic extends this record with its actual a0 and the original a0 bounds for the M5 tail only.

This module owns row masks and their disjoint sums, legal prefix extension by SMALL batches and individual LARGE labels, the W_J construction, its bank identity, the T extension, and transport of strip legality along an occurrence map. The used set and retained masks are literal finite sets. Both the existing M5 consumer and the general LOWER consumer call these same proofs. These are shared accepted prefix arguments, with no additional mathematical credit claimed for their relocation.

The common T interface requires an actually constructed retained subset and payment mask satisfying its gate. Each consumer supplies that selection by its own proof. The generic LOWER construction retains the entire b row, pays no u label, and proves its exact future complement. The M5-only U/V0 extension still uses a0<=z, and its terminal complement still uses ten rows. Neither conclusion follows from this shared seven-row module.

References