RecoversExtractFromBare
plain-language theorem explainer
Predicate on bare-ledger selectors: a map from two-cell recognition ledgers to reals recovers the signed extract at hinge 0 from every dual-entry witness's bare shadow. Separation theorems cite it to state that no such selector exists. Definitional Prop only; the body is the recovery equation, not a proof.
Claim. A selector $s$ from bare recognition ledgers on a two-cell lattice to $\mathbb{R}$ recovers the signed extract from bare data when, for every real source $d$, $s$ applied to the bare shadow of the dual-entry witness realizing $d$ equals that witness's extract at hinge $0$.
background
Module setting is Wave B residual R3: dual-entry signed-source enrichment. The bare cost ledger is a derived shadow of the foundational recognition ledger, which carries signed debit and credit columns with $\phi = \mathrm{debit} - \mathrm{credit}$. The J-cost quotient is even and forgets exactly $\mathrm{sign}(\phi)$. Enrichment restores column orientation via a dual-entry strain state (integer debit/credit, nonnegative magnitude, unit-flux cap).
A recognition ledger on a finite substrate assigns a symmetric real cost to each cell pair with zero diagonal. The dual-entry witness for a real source $d$ places unit debit/credit on the two cells according to the global $\mathbb{Z}/2$ convention (debit-leads iff $0 \le d$), with magnitude $|d|$. Its bare shadow is the sign-blind J-ledger; extract at hinge 0 is meant to recover the signed source $d$.
Upstream, the no-bare-selector lemma already blocks recovery of a signed source from bare ledgers; this Prop packages the analogous recovery claim for the enriched extract.
proof idea
Definitional Prop, not a theorem. The body is the single universal equation: for every real $d$, the selector on the bare shadow of the dual-entry witness equals the witness extract at hinge 0. No tactics, no lemmas applied at this site.
why it matters
Names the recovery property that R3 must refute. Downstream, the separation theorem (c) proves no bare-ledger selector satisfies this Prop, by direct reduction to the upstream blocker that no bare selector recovers a signed source. The typed residual schema for signed-source enrichment conjoins extract recovery, bare-shadow equality to the sign-blind ledger, swap-invariance of the bare shadow, and the negation of existence of any selector meeting this Prop.
In the Recognition framework this is the load-bearing separation step showing dual-entry orientation is strictly richer than the bare J-ledger: sign($\phi$) is forgotten by the even cost quotient and cannot be reconstructed by any real functional of bare costs alone. It does not touch T5–T8 forcing, RCL, or the alpha band; it closes the R3 enrichment residual in the QG Wave B gap stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.