Gravity Seven Gaps Measure Invariance No Go Aut Card Two Point Complex

The two-point witness

The declaration autCard_twoPointComplex establishes a small but decisive counting fact: for a configuration consisting of two vertices and no edges, the number of relabelings that preserve the configuration, its automorphism group, has cardinality exactly 2. The proof works by exhibiting an explicit equivalence between the automorphism group of this two-vertex complex and the permutation group on two elements, then counting the latter. This is a theorem in the machine-checked library of formal theorems, proved with no gaps and no special axioms.

Why this counting matters: the framework's path-sum measure assigns each configuration a weight based on its symmetry, specifically the reciprocal of the size of its automorphism group. For the two-vertex complex, that weight is 1/2. The declaration is a witness that this weight is genuinely less than 1, separating it from a rival candidate that assigns every configuration the uniform weight 1. The two-vertex complex is the smallest case where the symmetry-factor measure and the uniform measure disagree.

In Recognition Science, the ledger, a discrete record of recognition events, needs a way to weight the possible configurations it can hold. The natural guess is that relabeling invariance, the requirement that the weight not change when vertices are renamed, plus positivity and normalization, forces the symmetry-factor measure. The framework's library proves this guess false. Three different weight functions satisfy all the named axioms, and in fact a countably infinite family does. The two-vertex complex provides the concrete separation: the symmetry-factor measure gives it weight 1/2, the uniform measure gives it weight 1, and both satisfy every invariance axiom.

What the declaration does not claim is just as important. It does not prove that the symmetry-factor measure is the right one; it refutes the claim that invariance alone determines it. It does not derive the measure from deeper substrate axioms; that derivation remains an open target. And it does not address the continuum limit, where the discrete ledger would become a continuous theory. The no-go result is scoped to the axioms actually named: a richer axiom set, including a gluing or factorization condition, could in principle restore uniqueness, and that possibility is exactly the open frontier.

/-- **THEOREM.**  `|Aut(twoPoint)| = 2` exactly (the identity and the
vertex swap). -/
theorem autCard_twoPointComplex (B : ℕ) (hB : 2 ≤ B) :
    Nat.card (Aut (twoPointComplex B hB)) = 2 := by
  rw [Nat.card_congr (twoPointAutEquiv B hB), Nat.card_eq_fintype_card,
    Fintype.card_prod, Fintype.card_prod,
    Fintype.card_equiv (Equiv.refl (Fin 2)),
    Fintype.card_equiv (Equiv.refl (Fin 0)),
    Fintype.card_fin 2, Fintype.card_fin 0]
  norm_num [Nat.factorial]

/-- **THEOREM.**  The symmetry-factor measure of the two-point witness is
exactly `1/2`. -/
theorem mu_twoPointComplex (B : ℕ) (hB : 2 ≤ B) :
    mu (twoPointComplex B hB) = 1 / 2 := by
  unfold mu
  rw [autCard_twoPointComplex B hB]
  norm_num

/-- **THEOREM.**  The uniform weight 1 satisfies every named invariance
axiom. -/
theorem uniformMeasure_satisfies (B : ℕ) :
    InvarianceAxioms B (uniformMeasure B) :=
  ⟨fun _ _ _ => rfl, fun _ => one_pos, fun _ => le_refl 1, rfl⟩

/-- **THEOREM.**  `1/|Aut|` satisfies every named invariance axiom. -/
theorem muMeasure_satisfies (B : ℕ) : InvarianceAxioms B (muMeasure B) :=
  ⟨fun _ _ h => mu_congr h, fun K => mu_pos K, fun K => mu_le_one K,
    mu_emptyComplex B⟩

/-- **HEADLINE (strengthened form).**  The named invariance axioms admit a
countably INFINITE injective family of measures `1/|Aut|^(n+1)`: the
underdetermination is not a two-point accident. -/
theorem invariance_admits_infinite_measure_family (B : ℕ) (hB : 2 ≤ B) :
    (∀ n : ℕ, InvarianceAxioms B (muPowMeasure B n)) ∧
      Function.Injective (muPowMeasure B) :=
  ⟨muPowMeasure_satisfies B, muPowMeasure_injective B hB⟩

/-- **HEADLINE (KILL + WITNESS).**  The named invariance axioms do NOT
determine the path-sum measure: the symmetry-factor measure `1/|Aut|`
and the uniform weight 1 BOTH satisfy every named axiom, yet they are
unequal, with the pointwise strict inequality exhibited at the concrete
two-point witness (where `|Aut| = 2`).  This is the kernel refutation of
the killed "mu-from-invariance" determination claim; the substrate
derivation of a unique measure remains OPEN. -/
theorem mu_not_determined_by_invariance (B : ℕ) (hB : 2 ≤ B) :
    InvarianceAxioms B (muMeasure B) ∧
    InvarianceAxioms B (uniformMeasure B) ∧
    muMeasure B ≠ uniformMeasure B ∧
    muMeasure B (twoPointComplex B hB) <
      uniformMeasure B (twoPointComplex B hB) :=
  ⟨muMeasure_satisfies B, uniformMeasure_satisfies B,
    muMeasure_ne_uniformMeasure B hB,
    muMeasure_lt_uniform_at_witness B hB⟩

What this page does not claim

The symmetry-factor measure is not proved to be the unique measure satisfying the named axioms. The measure is not derived from deeper recognition-ledger substrate axioms. The result does not address the continuum limit of the path-sum measure.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/SevenGaps/MeasureInvarianceNoGo.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: