recognitionRatioBridgeStatus_flags
plain-language theorem explainer
Four boolean status flags on the recognition-ratio bridge are all true: the paper's odd log-ratio relation is encoded, a negative geometric-deficit witness exists, derivation from stationarity is still open, and the old even bridge form is recorded as refuted. Anyone auditing Seven Gaps Phase 0a completeness would cite this. The proof is four reflexivity checks against the status definition; pure documentation, not new mathematics.
Claim. The canonical status record for the recognition-ratio bridge satisfies: the paper's odd relation on $\log x_\sigma$ is encoded; a witness admitting negative geometric deficit exists; derivation of the bridge from stationarity remains open; and the old even ledger-to-hinge form is marked refuted.
background
Seven Gaps Phase 0a replaces a refuted substrate-to-geometry bridge with the paper's odd form. The old form equated ledger deficit to signed geometric hinge deficit; ledger deficits are nonnegative and even in the deformation parameter, while signed Regge response is odd, so that equality is impossible.
The physics paper instead posits an admissibility clause on a positive comparison ratio $x_\sigma$ at each hinge:
$\log x_\sigma = \kappa_\sigma,\delta_\sigma + r$ with $|r| \le R,h^3$. That structure is the model-tier hypothesis RecognitionRatioBridge (paper Def 6.2 clause), not yet derived from stationarity.
The status record packages four documentation booleans for this module: whether the paper relation is encoded, whether a negative-deficit witness is present, whether stationarity derivation is still open, and whether the old even form is recorded as refuted. Upstream, the record is the definition that hard-codes all four fields to true.
proof idea
Term-mode proof: a 4-tuple of rfl. Each conjunct is definitional equality against the corresponding field of recognitionRatioBridgeStatus, which sets all four booleans to true. No lemmas, no tactics, no computation beyond reflexivity.
why it matters
Closes the documentation layer of Seven Gaps Phase 0a. The module already proves kernel-checked reconciliations with the no-gos: every exact unit-coupled bridge admits opposite-sign geometric deficits on two hinges; every bridge induces a genuine recognition ledger whose cost is J-cost of the ratio quotient; on the witness family the induced ledger deficit stays nonnegative and even under $d\mapsto -d$, while geometric deficit stays signed. Two observables, no contradiction.
This flag theorem does not add mathematics. It freezes the audit surface so a reader (or CI) can see at a glance that the paper relation is present, the negative-deficit witness is present, stationarity derivation is explicitly still open, and the old even form is marked refuted. No downstream theorems depend on it. Framework role is bookkeeping inside the gravity/Seven Gaps stack, adjacent to the ledger no-go and the odd-form bridge, not on the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.