faceRecord_length
plain-language theorem explainer
On any forced bulk cell configuration the boundary face-record is a length-6 list: one channel per face of the D=3 cube. Holography and Clausius bookkeeping cite this to justify summing record flux over exactly six channels. The proof is pure definitional equality (rfl).
Claim. For every bulk cell configuration $c$, the face-record of $c$ is a finite trace of length exactly $6$.
background
Module RecordMonotonicity is step 3 of the entropy-fork chain: derive weak complementarity on the forced D=3 cell from record accounting rather than from a monolithic holography premise. Boundary heat is the posted record flux summed channel-by-channel over the six faces of the cube.
A CellCfg is a bulk cell configuration. Its faceRecord is the six-channel boundary letter list produced by the cell-injection layer. Trace length is the standard inductive length on finite recognition traces (empty has length 0; each extension adds one).
Downstream bookkeeping equates one-step boundary heat to the change of a record-weight potential. That identity needs both endpoint face-records to have identical length so the flux-versus-weight lemma applies.
proof idea
One-line term proof by rfl. The face-record constructor is definitionally a six-element list (one entry per cube face), so its length reduces to the numeral 6 by computation. No lemmas are invoked.
why it matters
Feeds stepHeatCell_eq_potential, the identity $\delta Q = \Delta\Phi$ that one bulk step posts exactly the change of the record potential. That theorem rewrites both endpoint lengths via this result, then applies recordFlux_eq_weight_sub.
That step is the local generator of the module's ledger theorems: path heat telescopes to $\Phi(\mathrm{end})-\Phi(\mathrm{start})$ (books_balance), erasures export as negative boundary heat (erasure_exports_debit), and zero-heat steps preserve record weight (no_free_erasure). Those are the proved "no free erasure" half of weak complementarity on the forced cell (T8 forces $D=3$, hence six faces).
Without a fixed channel count the flux sum would be ill-typed against the weight potential; this lemma pins the count at the geometric value six.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.