Pith. sign in
module module moderate

IndisputableMonolith.Gravity.SevenGaps.Gap6LookalikeReceipt

show as:
view Lean formalization →

Receipt module for Gap 6 lookalike-falsification in the QG seven-gaps campaign. It banks certificates that 3D CDT tetrahedra, 3D Lorentzian Wick continuation, 4D kinematical hinge data, and related sign/combinatorial witnesses are not action-level 4D Einstein-Hilbert recovery. Gravity auditors cite it to separate scoped increments from the full-theory closer. Structure is a ledger of named non-equality and not-action-level certificates assembled from imported Wick and hinge modules.

claimA machine-checked receipt that several Gap-6 lookalikes fail to be 4D action-level gravity: a 3-simplex has 4 vertices (not the 5 of a 4-simplex carrier); 3D Lorentzian/CDT Wick continuation is not the 4D Regge/EH action; 4D kinematical hinge and $C_{m4}$ sign data remain below action level. Each item is a named certificate, not a full dynamical closure.

background

The seven-gaps campaign tracks scoped QG increments without flipping full-strength QGScopeAudit flags. Gap 6 concerns false positives: constructions that resemble discrete gravity (causal tetrahedra, Wick-rotated hinges, glued pentachora) but do not yet recover the continuum Einstein-Hilbert quadratic action in 4D.

Upstream, CausalSimplexWick builds the first certified Lorentzian layer for $D=3$ CDT-style tetrahedron classes and kinematical Wick rotation; all prior discrete-gravity results in the program were Euclidean. ThreePentCausalConsistency and GluedPentsHingeWitness supply admissible causal edge lengths and path-link (not cycle) witnesses on minimal interior-hinge complexes. SRSConvergesEH4D is the ledger-facing export that may later inhabit weak-field quadratic action recovery; this receipt deliberately does not claim that inhabitation.

The module doc line is combinatorial: 3D CDT tetrahedra use 4 vertices; the 4D carrier uses 5. That cardinality mismatch anchors the first non-lookalike certificates.

proof idea

Not a single theorem proof. The module assembles a family of banked certificates and Prop-level receipts imported from Wick hinge data, 4-1 and 3-2 hinge lanes, causal simplex Wick, glued-pents witnesses, three-pent causal consistency, action-cert family assembly, and the campaign/full-theory ledgers.

Typical pattern: combinatorial card inequalities (3-simplex vertex/edge counts unequal to 4D carrier), then named certificates that 3D Lorentzian continuation, 4D kinematical continuation, hinge data, and $C_{m4}$ sign data are not action-level 4D. Each certificate is a scoped non-claim relative to S_RS_converges_EH_4d-class closers, not a derivation of continuum gravity.

why it matters in Recognition Science

Feeds Gap6LookalikeReceiptAudit, the axiom audit for Wave C4 R0 gap6 lookalike-falsify receipt (headline theorems restricted to [propext, Classical.choice, Quot.sound]). In the Recognition gravity stack this protects the full-theory ledger: campaign increments (3D Lorentzian layer, hinge witnesses, Wick cert families) must not be misread as T8-adjacent $D=3$ spatial forcing or as completed 4D EH recovery.

Parent campaign context is the seven-gaps ledger and Phase 0c full-theory ledger: flags flip only on kernel-checked, critic-passed targets. Gap 6's job is negative: prove lookalikes are lookalikes so later positive closers (edge_tt_decomposition, S_RS_converges_EH_4d) remain the sole action-level claims. Without this receipt, kinematical Wick or glued-pent path links could be over-cited as Regge action.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.

declarations in this module (28)