Gravity Seven Gaps Exact Shell Gauge Uv To Equiv Triple Injective

The triple injectivity

In discrete geometry, a common way to study a space is to enumerate its building blocks up to a certain size. A bounded complex is such an object: it carries a size cap, a natural number B, and the same abstract complex appears as an element of BoundedComplex B for every B above its complexity. This creates a hazard: if you sum over all caps, you count the same complex many times.

The Recognition Science framework's machine-checked library of formal theorems addresses this with a construction called the exact class. An exact complex carries no cap fields; it is determined by its signature, the triple (v, e, t) of its vertex, edge, and tetrahedron counts. The library proves that a bounded complex maps to an exact complex by forgetting the cap, and that this map is a definitional equality: the cap-relaxation map of the bounded class collapses. The declaration toEquivTriple_injective establishes that this map is injective, meaning no two distinct bounded complexes collapse to the same exact complex. Combined with the theorem shell_index_unique, which states that a complex's signature determines exactly one shell index, this proves that no configuration is counted in two shells.

What this does not claim is equally precise. The injectivity result is a combinatorial fact about the enumeration of finite complexes; it says nothing about the physical continuum limit. The complexity cutoff is not mesh refinement, and the module explicitly states that the physical continuum limit remains an open target. The regulator exp(-ρ·n²) used in the path sum is a mathematical regulator inserted by hand, not derived physics, and its removal in the ρ → 0⁺ limit is a named open problem. The action or phase entering the unitary weight is a parameter, an arbitrary function on equivalence classes, not a derived physical action.

In plain terms, the declaration guarantees that the framework's bookkeeping is sound: when it sums over complexity shells, it does not double-count. That is a necessary condition for any further physical claim, but it is not itself a physical claim. The framework's honesty protocol requires stating that the regulator is not derived, the action is not derived, and the continuum limit is not reached. The injectivity result is the foundation on which those honest limits are recorded, not a step beyond them.

/-- **THEOREM (cap-dependence collapses).**  Relaxing the cap of a bounded
complex does not change its exact image: the map to the cap-free class
identifies all capped copies of the same configuration (definitional
equality). -/
theorem toExact_relax {B B' : ℕ} (h : B ≤ B') (K : BoundedComplex B) :
    toExact (PathSumMeasure.relax h K) = toExact K := rfl

/-- **THEOREM (no double counting).**  An exact complex can sit in the
shell at level `n` (i.e. its signature can be a `ShellSig n`) ONLY for
`n = exactComplexity K`: each configuration has exactly one shell.
Combined with the fact that `GlobalEquivalent` lives on a fixed signature,
no abstract complex is counted in two shells. -/
theorem shell_index_unique {v e t : ℕ} (K : ExactComplex v e t) {n : ℕ}
    (s : ShellSig n) (hv : sigV s = v) (he : sigE s = e) (ht : sigT s = t) :
    n = exactComplexity K := by
  unfold exactComplexity
  rw [← hv, ← he, ← ht]
  exact s.2.symm

What this page does not claim

The regulator exp(-ρ·n²) is not derived physics, but a mathematical regulator inserted by hand. The action or phase entering the unitary weight is not a derived physical action, but a parameter. The physical continuum limit, where the complexity cutoff becomes mesh refinement, is not established.

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/ExactShellGaugeUV.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: