IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerGeneratedHostileProbe
Hostile-probe module for Gap 2 / C14: it builds a deliberately non-local cost that bills every vertex the complex's total SJ and checks that this decoy fails the ledger-generated gate. Contrasts with the canonical recognition cost jCost, which the parent module asks to pass. Anyone auditing the tilt-fork measurement for flag 8 cites the probe verdict and the decoy-failure lemmas. Structure is a battery of named probes (vertex/edge/tet, seed history, C27 caps) ending in a boolean verdict.
claimDefine a hostile cost that charges each vertex the complex's total $SJ$ (non-local billing). The module asserts: (i) this cost is not ledger-generated; (ii) the canonical recognition cost $jCost$ still matches the ledger-generated pattern on vertices and vanishes on edges and tets; (iii) seed-history and C27 shape/hard-stop probes leave flag 8 unmoved, yielding a fixed TRUE/FALSE verdict for the Gap-2 fork.
background
Gap 2 sits in the SevenGaps gravity stack as C14: a pre-registered TRUE/FALSE measurement that decides the tilt fork for flag 8 (gap2_measure_derived). Upstream A1.7 (Gap2LetterCostDichotomy) closed the bulk-cancelling fixed-kind-totals class; residual nonzero history cost can live only in the escape class. The parent module Gap2LedgerGenerated freezes what "ledger-generated" means for the canonical recognition cost $jCost$ and reuses the C15 enumeration harness and SJ spectra.
Ledger-generated means the cost factors through local ledger charges on the complex (vertices, edges, tets) rather than global aggregates. The hostile probe here is the opposite intuition: each vertex is charged the complex's total $SJ$, so the cost is non-local by construction. SJ denotes the recognition-side action/spectrum totals already fixed in the C15 harness; $jCost$ is the standard RS cost built from the unique $J$ of the forcing chain (T5).
proof idea
Not a single theorem: a probe suite imported over Gap2LedgerGenerated. Named checks establish that $jCost$ still matches charge on vertices and is zero on edges and tets, hence remains ledger-generated, while the SJ-total-per-vertex decoy fails that gate. Separate probes cover seed history, C27 shape cap and hard-stop boolean, and that flag 8 is unmoved. The suite collapses to probe_verdict as the recorded TRUE/FALSE outcome for the fork.
why it matters in Recognition Science
Closes the negative side of the C14 LedgerGenerated fork gate: the measurement is not vacuous, because a natural non-local alternative (bill every vertex the total $SJ$) is rejected while $jCost$ stays inside the frozen ledger-generated class. That sharpens the escape-class story left by A1.7 and feeds the pre-registered tilt decision for flag 8 in the SevenGaps gravity program. No downstream Lean dependents are wired yet; the module is an audit/harness layer on Gap2LedgerGenerated rather than a new physics lemma. Landmark contact is indirect: $J$-uniqueness (T5) underwrites $jCost$, and the eight-tick / ledger discipline of the RS stack is what "ledger-generated" is testing.
scope and limits
- Does not prove jCost uniqueness beyond the frozen ledger-generated definition.
- Does not re-derive A1.7 or reopen the bulk-cancelling fixed-kind-totals class.
- Does not claim the hostile SJ-total cost is physically realized; it is a decoy only.
- Does not move flag 8 by itself; only records the pre-registered probe verdict.
- Does not address Gaps other than Gap 2 / C14 in the SevenGaps list.
depends on (1)
declarations in this module (12)
-
theorem
probe_jCost_vertex_matches_charge -
theorem
probe_jCost_edge_zero -
theorem
probe_jCost_tet_zero -
theorem
probe_jCost_ledgerGenerated -
theorem
probe_decoy_fails -
def
sjTotalVertexCost -
theorem
probe_sjTotal_not_ledgerGenerated -
theorem
probe_seed_history -
theorem
probe_C27_shape_cap2 -
theorem
probe_C27_hard_stop_bool -
theorem
probe_flag_unmoved -
theorem
probe_verdict