RecoversSignedSourceFromBareLedger
plain-language theorem explainer
A predicate on real-valued maps from bare two-cell recognition ledgers: the map recovers the signed unit-coupled source if it returns every real d when fed the sign-blind bare ledger of d. Anyone citing the bare-ledger blocker uses this as the exact recovery property being ruled out. The body is a one-line universal equality, not a proof.
Claim. A map $\mathrm{select}$ from bare two-cell recognition ledgers to $\mathbb{R}$ recovers the signed source from the bare ledger if, for every real $d$, $\mathrm{select}$ applied to the sign-blind bare ledger of $d$ equals $d$.
background
In the P2.1 terminal package, the claim is that the recognition-ratio bridge does not follow from a bare recognition ledger alone. The missing premise is a signed deficit-source constitutive coupling: a source strength linear in a hinge deficit, coupled into the total J-cost strain action.
A bare two-cell ledger records only the unsigned J-cost data on a two-site complex. The sign-blind bare ledger of a real source strength $d$ is the ledger induced by that strength after discarding orientation, so opposite signs produce the same ledger. Geometric deficit here is the usual hinge deficit $2\pi - \sum\theta$ (dihedral/Schläfli), but the blocker only needs that the ledger forgets the sign of the source.
The module therefore separates constitutive source data from ledger observables: recovery of the signed source would have to be a pure function of the bare ledger.
proof idea
Definitional Prop, not a theorem. The body is the single universal statement that the candidate selector, evaluated on the sign-blind bare ledger of every real $d$, returns $d$. No tactics or lemmas are invoked; sibling lemmas about sign-blind ledgers and cost extensionality are used only by the downstream non-existence theorem.
why it matters
This is the exact recovery property negated by the bare-ledger blocker: no selector from bare two-cell ledgers recovers the signed unit-coupled source, because the ledgers at sources $+1$ and $-1$ coincide while the required outputs differ. That theorem feeds the proposition-valued P2.1 certificate collecting coboundary telescoping, circularity of imposed strain budgets, the bare-ledger blocker, and the positive stationarity derivation once the named constitutive coupling is supplied.
In the Recognition gravity chain this pins why signed deficit-source orientation is extra constitutive data, not information already in the bare J-ledger, so the recognition-ratio bridge is not smuggled in as a ledger identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.