recognitionRatioBridgeStatus
plain-language theorem explainer
Canonical documentation record for the recognition-ratio bridge module: four boolean status flags, all set true. It marks that the paper's odd log-ratio admissibility is encoded as a model hypothesis, that a kernel-checked negative geometric-deficit witness exists, that bare-ledger derivation remains open, and that the old even bridge form is refuted. Cited only by the rfl-forced flags theorem; no mathematical content beyond bookkeeping.
Claim. The recognition-ratio bridge status record is the structure instance with all four documentation flags true: the paper's odd ratio relation is encoded; a negative geometric-deficit witness is present; derivation from stationarity is still open; and the old even bridge form is marked refuted.
background
This module (Seven Gaps, Phase 0a) encodes the physics paper's substrate-to-geometry bridge as an odd relation on a positive comparison ratio $x_\sigma$ at each hinge: $\log x_\sigma = \kappa_\sigma \delta_\sigma + R$ with $|R| \le \mathrm{remBound},\mathrm{meshScale}^3$. That clause is an admissibility hypothesis on $\log x$, not an equality of nonnegative deficits.
The older bridge form (ledger deficit equals signed geometric hinge deficit) was refuted: ledger deficits are nonnegative and J-ratio deficits are even in the deformation, while signed Regge response is odd. The ratio bridge reconciles this by keeping signed information in $\log x$ and inducing a genuine recognition ledger whose deficit stays nonnegative and even.
RecognitionRatioBridgeStatus is only a documentation structure of four booleans classifying MODEL vs THEOREM vs OPEN residual vs refutation. The mathematics lives in the named theorems above it, not in these flags.
proof idea
Pure structure instance: four field assignments to true. No tactics, no lemmas, no computation. Downstream recognitionRatioBridgeStatus_flags then discharges the four equalities by rfl.
why it matters
Bookkeeping endpoint for Phase 0a of the Seven Gaps gravity program. It records, in one place, that (i) the paper's Def 6.2 odd recognition-ratio clause is present as an explicit model hypothesis, (ii) the strong escape from the sign no-go (ratioBridge_admits_negative_deficit and related witnesses) is theorem-tier, (iii) full derivation from bare ledger stationarity remains an open residual (partially closed elsewhere by stationarity bridge closure, with deficit-source coupling still model), and (iv) the old even form is marked refuted by the LedgerBridgeNoGo line.
Only consumer is recognitionRatioBridgeStatus_flags, an rfl-forced conjunction used as a machine-readable status summary. No forcing-chain (T0–T8) step is advanced here; the record merely tracks how far the odd bridge has been reconciled with the ledger no-gos inside the gravity domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.