Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.DynamicStructureBracketAudit

show as:
view Lean formalization →

Audit layer for the Wave C2 dynamic structure-function bracket on two sites. It sits on the R0+R1 closure that rejects the frozen-Hamiltonian decoy and records the correct configuration partials when the structure function varies. Gravity residual-DAG maintainers cite it to confirm the typed residuals stay discharged. The module is organizational: it imports and re-exposes the bracket development rather than proving new identities.

claimModule-level audit of the two-site dynamic structure-function bracket: the naive substitution of a configuration-dependent $g$ into a frozen Hamiltonian slot $H_W$ fails because $\partial_q$ picks up an uncompensated $\partial g/\partial q$ term; the audited development records the corrected partials that cancel that residual.

background

Recognition Science gravity work tracks typed residuals in a residual DAG for quantum-gravity Wave C2 (Gap 5). The parent development DynamicStructureBracket closes the first two residuals R0 and R1 on a two-site structure-function bracket.

R0 is the decoy: plugging a varying structure factor $g(x)$ into a frozen Hamiltonian weight $H_W$ while reusing frozen configuration partials leaves an uncompensated $\partial g/\partial q$ in the configuration derivative. R1 is the matching corrected identity once those partials are recomputed with $g$ dynamic.

This audit module imports that bracket development and packages the residual status for the SevenGaps gravity stack. No new geometric primitives are introduced here; the setting is the same two-site discrete phase-space bracket used upstream.

proof idea

Definition and audit packaging module, not a standalone proof script. It imports DynamicStructureBracket and surfaces the R0 decoy failure together with the R1 corrected dynamic partials. Argument structure lives entirely in the imported module: exhibit the extra $\partial g/\partial q$ term under frozen partials, then discharge the residual with the dynamic configuration derivatives.

why it matters in Recognition Science

Keeps the SevenGaps gravity residual ledger honest for Wave C2 Gap 5. Downstream consumers of the dynamic bracket need a stable audit surface that records R0 as rejected and R1 as closed; this module is that surface. It does not itself feed named parent theorems in the current graph (used_by is empty), but it anchors the R0+R1 slice of the residual DAG draft so later residuals can assume the two-site dynamic bracket without reopening the decoy. Within the broader RS gravity program it is bookkeeping for structure-function dependence, not a new forcing-chain step (T0–T8) or mass-ladder identity.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.