ledger_forces_separation
plain-language theorem explainer
Ledger closed-flux conservation implies existence of a balanced-parity encoding such that no decoder recovers the hidden bit from any index set smaller than n/2. Complexity researchers modeling dual computation-recognition scales under ledger assumptions would cite this for hypothetical separations. The short tactic proof supplies the BalancedParityHidden encoder and reduces the decoder assumption to a contradiction via the omega_n_queries lower bound.
Claim. Let $L$ be a ledger with closed flux conservation, i.e., $L.closed_flux(γ)=0$ for every flux $γ$. Then there exists an encoding $e:Bool→(Fin n→Bool)$ such that for every bit $b$ and every index set $M$ with $|M|<n/2$, no decoder $d$ satisfies $d(e(b)|_M)=b$.
background
This theorem lives inside the ComputationBridge scaffold module, which explores hypothetical ledger-based complexity separations and is explicitly excluded from the verified certificate chain. The central upstream objects are the hidden-mask encoder (bit $b$ masked by random $R$ via conditional negation) and the omega_n_queries theorem (any universal decoder on a proper subset must fail). The restrict operation simply projects a full word onto the queried coordinates. The ledger hypothesis is drawn from LedgerUnits with the balanced property supplied by LedgerForcing, enforcing double-entry conservation.
proof idea
The tactic proof introduces the ledger and flux hypothesis, then instantiates BalancedParityHidden.enc as the witness encoding. For arbitrary $b$ and $M$ with $|M|<n/2$, it assumes a decoder exists, applies classical logic, and reduces the assumption to a negated universal statement. The key step invokes omega_n_queries on the restricted encoding via simpa, yielding the required contradiction.
why it matters
The result supplies one concrete mechanism for the module's stated key insight: ledger double-entry structure forces information hiding that separates computation from observation. It directly supports the hypothetical SAT-separation and P-vs-NP claims listed in the module documentation, though the same documentation warns against treating the construction as proven mathematics. The declaration sits outside the T0-T8 forcing chain and does not feed any verified downstream theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.