IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerSiteBlindness
Minimal two-vertex, one-edge graph where the recognition ledger is blind to site permutations that a path-sum measure must see. Supplies explicit witnesses that agree on ledger cost yet disagree on measure weight, and proves there is no site-symmetric measure on this substrate. Cited by the Gap-2 gauge-counting inevitability census as structural evidence that richer ledger structure forces ν = 1/|Aut|.
claimOn the directed graph with vertices $\{0,1\}$ and single edge $0\to 1$, the recognition-ledger cost is invariant under site permutations, while any normalized positive path-sum measure cannot be. Explicit ledger-agreeing, measure-disagreeing witnesses exist; the automorphism group is trivial ($|\mathrm{Aut}|=1$) and site-symmetry cardinality equals $2!$.
background
Recognition gravity books gravitational action as the continuum limit of total ledger cost on a discrete recognition substrate (the Recognition Ledger module: structural theorem, zero sorry). Gap 2 in the seven-gaps program asks whether that ledger, together with posting-layer structure, already forces the physical class mass to be the gauge-counting weight $\nu=1/|\mathrm{Aut}|$.
The companion MeasureSubstrateBlocker module proves a no-go: relabeling invariance, positivity, and normalization alone do not select a path-sum measure, while ExactShellGaugePreflight records that gauge-counting mass equals $1/|\mathrm{Aut}|$ under a model uniform-gauge-density premise. The present module isolates the smallest concrete graph on which ledger bookkeeping is blind to site symmetry that any measure must resolve.
Objects introduced here include the two-point one-edge graph, its automorphism cardinality, off-diagonal ledger cost on $\mathrm{Fin},2$, site-symmetry cardinality, a uniform ledger, and paired witnesses that match on ledger values yet differ as measures.
proof idea
The module is a short constructive argument chain, not a single theorem. It defines the two-vertex one-edge substrate and computes $|\mathrm{Aut}|=1$ by a subsingleton instance on edge automorphisms. Site-symmetry on $\mathrm{Fin},2$ is identified with the full permutation group (every perm is a site symmetry), so the site-symmetry cardinality is $2!$. Off-diagonal ledger cost and a uniform ledger are evaluated explicitly. From those calculations one obtains: (i) no measure can be site-symmetric on this substrate, and (ii) concrete witnesses that agree on the ledger yet disagree as measures. Downstream modules import these facts as named lemmas rather than re-deriving the $\mathrm{Fin},2$ combinatorics.
why it matters in Recognition Science
Feeds IndisputableMonolith.Gravity.SevenGaps.GaugeCountingInevitableReasons, the necessary-reasons census for Gap 2. That parent assumes the Gap-2 measure target (richer RecognitionLedger / posting-layer structure forces MeasureSubstrateBlocker.GaugeCountingPrinciple, equivalently $\nu=1/|\mathrm{Aut}|$) and lists every fact that would make the target unavoidable, each marked proved, OPEN, MODEL, or refuted.
Ledger site-blindness is the structural reason the ledger alone cannot pin the measure: cost is insensitive to site permutations that change path-sum weights. The two-point one-edge witnesses make that blindness fully explicit and finite, so the census can cite a proved obstruction rather than a slogan. In the broader Recognition gravity stack this sits under the ledger-as-action programme and the path-sum measure no-go, tightening why gauge counting must be imposed (or derived from richer structure) rather than read off raw ledger cost.
scope and limits
- Does not prove the full Gap-2 theorem that ledger structure forces ν = 1/|Aut| in general.
- Does not construct or select a continuum path-sum measure on arbitrary graphs.
- Does not claim the two-edge or larger substrates; only the Fin 2 one-edge witness.
- Does not discharge MODEL premises recorded in MeasureSubstrateBlocker (uniform gauge density).
- Does not address dynamical gravity field equations or continuum limits of the action.
used by (1)
depends on (2)
declarations in this module (20)
-
abbrev
twoPointOneEdge -
instance
instSubsingletonAutOneEdge -
theorem
autCard_twoPointOneEdge -
theorem
mu_twoPointOneEdge -
def
siteSymCard -
theorem
cost_offDiag_fin2 -
theorem
every_perm_is_siteSym -
theorem
siteSymCard_fin2 -
theorem
no_siteSymmetry_measure -
theorem
witnesses_agree_on_ledger_disagree_on_measure -
def
uniformLedger -
theorem
uniformLedger_offDiag -
theorem
encoding_unconstrained -
theorem
value_route_is_encoding_choice -
def
uniformLedger3 -
theorem
uniform3_siteSym -
def
dcost -
def
distinctLedger -
theorem
swap01_not_siteSym_distinct -
theorem
siteSymmetry_is_chosen_by_the_encoding