Pith. sign in
module module high

IndisputableMonolith.Gravity.SevenGaps.Gap2IncidenceSilenceVerdict

show as:
view Lean formalization →

Scoped no-go at the letter-cost layer of Gap 2: equivariant, total-size-blind letter costs need not be linear by kind in aggregate. A concrete witness (pair cost) satisfies the letter-cost axioms yet fails fixed kind totals. Gravity and QG campaign readers cite it when tracking which named premises of the Gap 2 measure remain unforced. The module packages the witness, named further premises, and a re-export certificate with explicit scope.

claimAmong equivariant letter costs that are blind to total size, aggregate linearity by kind is not forced: there exists a pair cost $C$ such that the fixed-kind-totals property fails. The module records this scoped no-go, the named schedule/measure premises still open above it, and a certificate that the Gap 2 measure derivation is unmoved by the failure.

background

Gap 2 sits in the Seven Gaps gravity campaign: derive the gauge-volume gluing law (inverse-factorial labeled weights and the gauge counting principle) from recognition-ledger structure, or name a scoped obstruction. Upstream arcs reduced the measure to a chain of named premises. Weight is size-blind if cost is kind-only; cost is kind-only if charge is counts-only; charge is counts-only if lattice imbalance and magnitude are. None of those is forced at its own layer.

The prior arc asked whether ledger posting dynamics force the counts-only premise. This module answers one layer down: at the letter-cost layer itself, equivariant total-size-blind costs need not obey aggregate linearity by kind (FixedKindTotals). The full-theory ledger (Phase 0c) tracks which pillar benchmarks are kernel-checked; this no-go is a status-bearing theorem re-export, not a new axiom dump.

Sibling content names the witness (pairCost), records that the kind rule fails twice, and packages schedule/measure premises still required above the letter-cost layer.

proof idea

The module is a theorem package, not a definition dump. Core argument: exhibit an equivariant, total-size-blind letter cost (pair cost) and prove it does not satisfy fixed kind totals, so aggregate linearity by kind is not forced at this layer. Companion lemmas record that the kind rule fails in two independent ways and that the ledger dynamics do not force counts-only. Named schedule and measure premises are collected as further hypotheses still needed above the no-go. A certificate object re-exports the scoped verdict and records that the Gap 2 measure derivation status is unchanged (unmoved) by the letter-cost silence.

why it matters in Recognition Science

Closes a concrete branch of the Gap 2 forcing chain: incidence/silence at the letter-cost layer is a scoped no-go rather than a derivation of counts-only structure. Downstream, Gap2GluingLawStationarity aims to derive the gluing law from recognition-ledger structure or prove a scoped no-go naming missing structure; this module supplies one such named wall (bare letter cost does not force kind totals). Axiom-audit and outside-module probe modules import it to keep the certificate on the ordinary Mathlib basis (propext, Classical.choice, Quot.sound) and to check the verdict from outside the defining module. In the full-theory ledger campaign, the result is a machine-checked status record (0 sorry, 0 new axiom) that prevents silently assuming kind-linearity when building toward gauge counting.

scope and limits

used by (3)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (10)