IndisputableMonolith.Holography.RecordCostAsymmetry
Defines record cost of a finite map as base-2 log of image cardinality: the independent binary distinctions the map actually performs. That is the image (rank) side of the rank-nullity split the ledger floor charges. Holography workers cite it to separate performed records from fiber microstate cost when naming the area-law coefficient selector. The module packages the definition with zero-cost lemmas, closed-map and domino identities, and the forced one-vs-two multiplicity selector.
claimFor a finite map $f:X\to Y$, record cost is $\log_2|\mathrm{im}\,f|$: the number of independent binary distinctions $f$ performs. Microstate cost is the complementary fiber (nullity) contribution. The ledger floor sums only posted performed distinctions, so only record cost enters the holographic rank/nullity selector between recognition multiplicities one and two.
background
RS holography splits the recognition-pixel area $a_{\mathrm{pix}}=\kappa\cdot H\cdot\ell_P^2$ (the "4" in Bekenstein-Hawking $S=A/4$) into three separately derived pieces: the integer coefficient, the per-event entropy $H=(\phi+2)\log\phi$, and the area scale $\ell_P^2$. Upstream modules already force $H$ and attack the integer on the $D=3$, eight-tick ($2^3$) lattice; $\ell_P^2$ remains blocked by a scale-invariance no-go.
CoefficientBridge and the holography panel treat $\kappa$ as a physical selector to name, not a numeral for decide to pick among labelled integers. EdgeSectorBridge relocates the live candidate away from a naive four-sector entropy reading. RecognitionMultiplicity encodes the selector as a T-1 ledger rank-consistency check, conditional on a modeling choice.
This module supplies the image-side cost that the ledger actually charges: distinctions performed by a finite map, as opposed to unused fiber microstates.
proof idea
Definition-led module, not a single theorem. recordCost is $\mathrm{Nat.log2}$ of image cardinality for an arbitrary finite map; microstateCost is the complementary fiber side. Supporting lemmas: $\log_2$ vanishes on cardinalities $\le 1$; constant maps and more general zero-image cases give record cost zero; closed-map and domino identities relate composite recording; each fiber posts one record under the stated posting rule; record cost equals recognition multiplicity in the one- and two-outcome cases; selector_forced packages the rank-side choice the ledger floor forces. Argument shape is definition plus elementary finite-cardinality and log identities, not a deep existence proof.
why it matters in Recognition Science
Feeds KeystoneFactorThree, whose doc-comment states that the rank/nullity selector from RecordCostAsymmetry leaves one explicit physical premise for a conditional exclusion of the microstate reading of the area-law coefficient (panel-greenlit Live Bet 2). Without a clean split between performed records and fiber cost, the coefficient $\kappa$ collapses back into an ambiguous integer label among 4, 3, 2, 1.
In the broader chain this sits under PixelLocal's attack on the integer factor on the forced $D=3$, eight-tick substrate, and under CoefficientBridge's demand that the selector be named rather than computed. It does not close the full Bekenstein $1/4$ derivation; it isolates the ledger-charged rank side so downstream exclusion structure can bite.
scope and limits
- Does not unconditionally derive Bekenstein-Hawking $S=A/4$ or fix $\kappa=4$.
- Does not determine the area scale $\ell_P^2$ (blocked by scale-invariance no-go).
- Does not re-derive per-event entropy $H$; that lives in RecognitionEventCapacity.
- Does not prove sector-based four-outcome entropy is physical (EdgeSectorBridge rejects that reading).
- Does not discharge RecognitionMultiplicity's modeling hypothesis; selector remains conditional.
- Does not treat infinite or continuous maps; record cost is defined for finite maps only.
used by (1)
depends on (4)
declarations in this module (24)
-
def
recordCost -
def
microstateCost -
theorem
log2_eq_zero_of_le_one -
theorem
record_zero_general -
theorem
record_zero_of_constant -
theorem
recordCost_closed -
theorem
recordCost_domino -
theorem
fiber_posts_one_record -
theorem
records_performed -
theorem
recordCost_eq_multiplicity_one -
theorem
recordCost_eq_multiplicity_two -
theorem
selector_forced -
theorem
bekenstein_selector_from_asymmetry -
theorem
one_le_log2_of_two_le -
theorem
microstate_cost_nonzero_on_constant -
def
target_record_cost_asymmetry -
theorem
target_record_cost_asymmetry_holds -
theorem
recordCostAsymmetryCert -
def
HorizonEntropyIsRecordCost -
def
HorizonEntropyIsMicrostateCost -
theorem
bekenstein_coefficient_of_record_cost -
theorem
kappa_four_thirds_of_microstate_cost -
theorem
record_zero_separates_readings -
theorem
bekenstein_tag_b_cert