module module moderate

`IndisputableMonolith.Holography.RecordMonotonicity`

Defines per-face posted flux and cell heat between boundary records on the D=3 holographic cell, then proves discrete books balance and that erasure cannot be free: any net debit must export. Holography and Clausius-side arguments cite it as the six-channel form of step heat. The development is mostly definitional equalities plus short algebraic identities on signed flip counts.

claimOn the six face channels of a $D=3$ cell, the posted flux between two boundary records is the signed sum of flip bits ($+1$ up, $-1$ down, $0$ unchanged). Cell potential and step heat equal that flux; along a path, heat telescopes. Books balance: net ledger change matches exported flux. Consequently there is no free erasure: a pure debit on the record forces a compensating export.

background

Recognition holography treats the boundary record of a spatial cell as the ledger that must post bulk distinctions. The upstream CellInjection program asks whether flipping an interior bit necessarily changes that record; this module supplies the accounting layer once records are compared.

The central quantity is per-channel posted flux: over the six faces, sum $+1$ for an up flip, $-1$ for a down flip, and $0$ if the face bit is unchanged. That is the six-channel form of the Clausius selector step heat (boundary heat equals posted ledger flux). Record weight is the companion non-signed tally; flux equals a weight difference on the appropriate pairing. Cell potential and step heat are identified with this flux so path heat telescopes.

The local setting is discrete, unit-temperature bookkeeping on face records of fixed length, not continuum thermodynamics. Imports stop at CellInjection and Mathlib; continuum limits and continuum Clausius inequalities are out of scope here.

proof idea

Most declarations are definitions or one-line rewrites: flux as signed face sum, weight as the unsigned companion, and equalities identifying step heat and cell potential with flux. Path heat is the telescoping sum of steps. Books balance is the global conservation identity (net interior change equals exported boundary flux). No-free-erasure and erasure-exports-debit are short corollaries: a pure record debit with no compensating credit forces a nonzero export term. No deep tactic search; the argument is finite signed arithmetic on six channels.

why it matters in Recognition Science

LocalRecognitionHorizonCut imports this module as the posted-record heat leg: exterior projection of a closed cut configuration uses discrete books balance and unit-temperature Clausius as theorems about the horizon record, alongside one-sided seam double-posting. Without flux, potential, and the no-free-erasure corollaries, the entropy-fork program cannot treat boundary heat as forced ledger export.

In the broader Recognition chain this is the holographic bookkeeping companion to complementarity tests (CellInjection): if bulk flips must post, the posted quantity is this flux, and erasure cannot hide debit. It does not itself force $D=3$ or the eight-tick octave; those enter from the forcing chain. It feeds horizon-cut and Clausius-side results rather than mass or $\alpha$ numerics.

scope and limits

Does not prove bulk flips must post; that is CellInjection, not record accounting.
Does not derive continuum Clausius or thermodynamic temperature beyond unit discrete heat.
Does not fix $D=3$, eight-tick structure, or J-cost uniqueness; those are upstream forcing facts.
Does not bound $\alpha$, masses, or Berry thresholds; pure ledger identities only.
Does not treat multi-cell networks or continuum horizons beyond the local cell faces.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Holography.LocalRecognitionHorizonCut module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Holography.CellInjection module_import

declarations in this module (44)

def recordFlux L90
def recordWeight L94
theorem recordFlux_eq_weight_sub L99
theorem recordFlux_self L121
def cellPotential L126
def stepHeatCell L129
theorem faceRecord_length L131
theorem stepHeatCell_eq_potential L134
def pathHeatCell L139
theorem books_balance L148
theorem no_free_erasure L159
theorem erasure_exports_debit L166
def RecordMonotone L173
theorem recordMonotone_of_no_export L179
def gaugeRel L191
theorem gaugeRel_equivalence L196
theorem gauge_step_zero_heat L200
theorem silent_iff_kernel L209
theorem mem_recordKernel_iff L213
theorem gauge_iff_kernel_record L218
theorem gauge_iff_kernel L225
def RecordCompatible L234
def CreatesFreeRecord L240
theorem recordCompatible_iff_no_free_record L245
def runProtocol L255
theorem no_protocol_separates L261
def Separated L274
theorem gauge_never_separated L279
def gaugeSetoid L286
def PhysState L290
def physState L293
def physRecord L296
theorem physRecord_mk L299
theorem weak_complementarity L306
theorem physRecord_mem_image L313
theorem physRecord_surjective_on_records L321
theorem physState_records_card L329
theorem holographic_bound_of_weak_comp L337
def KernelIsGauge L348
theorem weak_complementarity_of_gsl L355
theorem kernelIsGauge_falsifier L364
def target_record_monotonicity L377
theorem target_record_monotonicity_holds L387
theorem recordMonotonicityCert L392