ledgerEnergyBridgeStatus_flags
plain-language theorem explainer
Status certificate for the corrected ledger-to-geometry bridge: five theorems are marked proved (J-cost expansion, coboundary ledger instance, antisymmetric RCL-gate failure, quadratic matching, shear visibility), Isaacson identification is marked model, and Hessian-symbol plus tensor-multichannel comparisons remain open. Auditors of Seven Gaps Lane 1b cite this as the single boolean summary. The proof is eight reflexivity checks against the canonical status record.
Claim. The canonical ledger-energy bridge status record asserts: the $J$-cost expansion theorem holds; the coboundary ledger instance theorem holds; the general antisymmetric RCL-gate failure theorem holds; the quadratic matching theorem holds; the shear visibility theorem holds; the Isaacson identification is a model; the Hessian-symbol comparison is open; and the tensor multichannel comparison is open.
background
Seven Gaps Lane 1b replaces an unsatisfiable signed bridge (ledger deficit equal to signed geometric hinge deficit) with a bridge to nonnegative curvature-quadratic geometric energy of Isaacson type, $\sum_h A_h \delta_h^2$. The geometric side is pure hinge data; the ledger side is pure substrate potential and $J$-cost. Matching links the two only after both are defined independently.
The construction is scoped to coboundary strains $s_{ij}=f_i-f_j$: those ratios obey the cocycle law and RCL subadditivity via the d'Alembert identity on $J$. General antisymmetric strains can violate the RCL gate, so the status record also tracks that negative result.
ledgerEnergyBridgeStatus is the module's canonical boolean scorecard. Proved items are set true for theorems; model and open items are likewise flagged explicitly so the honest limit (instance shape-compatibility, not yet independent Regge geometry) is machine-readable.
proof idea
Pure term-mode reflexivity. The goal is an eight-fold conjunction of field equalities against the definitional values in the status record; each conjunct is discharged by rfl, packaged as an 8-tuple constructor. No lemmas are invoked beyond definitional unfolding of the record.
why it matters
Gives a single, rfl-forced audit point for Lane 1b of the gravity Seven Gaps program: what is theorem, what is model, and what remains open. Downstream consumers (none yet wired in the graph) can pattern-match on these flags rather than re-inspecting each proof. The open Hessian-symbol and tensor-multichannel flags mark the honest limit stated in the module: the canonical instance certifies shape-compatibility of ledger total cost with quadratic curvature energy when hinge data is read off the ledger potential, not a match to independently derived Regge geometry. That separation keeps the forcing chain (RCL, $J$-uniqueness, coboundary scoping) clean while advertising the remaining geometric identification work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.