extract_not_bare_factorable
plain-language theorem explainer
No real-valued selector on bare two-site recognition ledgers can recover the signed extract of the dual-entry enrichment. Gravity analysts closing the R3 residual cite this as the separation clause: the bare J-cost shadow is strictly coarser than the signed dual-entry state. The proof is a one-line reduction that rewrites the recovery hypothesis through the bare-shadow and extract-zero bridges into the existing blocker non-existence lemma.
Claim. There is no function $\mathrm{select}$ from bare recognition ledgers on $\mathrm{Fin}\,2$ to $\mathbb{R}$ such that, for every real source $d$, $\mathrm{select}$ applied to the bare shadow of the dual-entry enrichment of $d$ equals the signed extract of that enrichment at hinge $0$.
background
Wave B residual R3 treats the bare cost ledger RecognitionLedger as a derived shadow of the foundational dual-entry ledger, which carries integer debit and credit columns with $\phi=\mathrm{debit}-\mathrm{credit}$. The J-cost quotient is even and forgets exactly $\mathrm{sign}(\phi)$. The enrichment is a dual-entry strain state with nonnegative magnitude and a unit-flux orientation cap; a global $\mathbb{Z}/2$ convention pins deficit to debit-leads and matches the Regge sign convention.
RecoversExtractFromBare is the proposed recovery property: a bare-ledger selector returns, for every real $d$, the extract at hinge $0$ of the enriched witness of $d$. Upstream, enrichedWitness_extract_zero identifies that extract with $d$ itself, and enrichedWitness_toBare identifies the bare shadow with the sign-blind bare ledger used by the ratio-substrate blocker. Together these make bare recovery of extract equivalent to bare recovery of the signed source.
proof idea
Term-mode proof by contradiction. Unpack an alleged selector satisfying RecoversExtractFromBare. For each real $d$, rewrite the recovery equation by enrichedWitness_toBare and enrichedWitness_extract_zero, so the selector on the sign-blind bare ledger equals $d$. Package that rewritten hypothesis as a bare-ledger selector recovering the signed source, and discharge by the upstream non-existence lemma no_bare_ledger_selector_recovers_signed_source. No new arithmetic is performed.
why it matters
This is clause (c) of the R3 package: signed-source enrichment is strictly richer than bare RecognitionLedger. Downstream, typedResidual_signed_source_enrichment_schema_closed assembles extract-zero, bare-shadow equality, swap-invariance of the bare shadow, and this non-factorability into the closed typed residual. Module honesty keeps the result off the gap1 bridge and off any binding of recognition_ratio_derived (that is R5). Load-bearing content is F2 plus the three separation facts (a)(b)(c); posting-run adjacency is omitted as garnish. In the broader gravity analysis it certifies that forgetting sign via the even J-cost cannot be inverted by any bare selector, so dual-entry orientation is indispensable for signed residual bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.