Mathematics Bipartite Distance Spectrum Approx Contained In Gaussian Like Lattic

The approximation definition

The definition ApproxContainedInGaussianLikeLattice is a precise, formal way to say that a finite set of points in the plane is almost entirely contained in the image of a lattice-like grid. The grid is not required to be a perfect square lattice; it is any rank-two additive structure in the plane whose squared distances are given by an integral positive quadratic form after a uniform scaling. The definition allows a small number of exceptions: for a set of n points and a chosen error bound, all but at most that many points must lie exactly on the grid. This is a deliberately weak notion, chosen so that future work can strengthen it to density-in-a-box, Freiman-isomorphism, or Hausdorff-distance variants without changing the underlying physical statement.

The definition appears in the machine-checked library of formal theorems within the Recognition Science framework. Its role is to state a target, not to prove one. The target is an inverse theorem: if the alphabet of squared cross-distances between two n-point planar sets is small, at most n divided by the square root of the natural logarithm of n, then both sets should be approximately carried by a single Gaussian-like lattice, with error at most n divided by 100. This target is explicitly recorded as not asserted as proved in the library; it is the exact classical lemma needed to turn a physical statement about planar rigidity into a conventional proof.

The definition itself is a formal object with a clear meaning. It takes three inputs: a finite set of points, a Gaussian-like lattice, and a natural number error bound. It asserts the existence of a subset of the original set, containing all but error many points, such that every point in that subset is the image of some integer pair under the lattice's basis map. The lattice structure guarantees that the squared norm of any basis image equals a fixed positive scale times a nonnegative integer quadratic form. This makes the grid genuinely lattice-like: its points sit at positions whose squared distances from the origin are integer multiples of a common scale.

What the definition does not claim is as important as what it claims. It does not assert that any particular set is approximately contained in such a lattice, nor that the inverse theorem holds. It does not assert that the lattice is unique, that the error bound is optimal, or that the approximation is stable under perturbations. The definition merely names a property that a set might have. The property is the conclusion of a larger target, PlanarNormFiberRigidityTarget, which remains open. The library records the definition so that the target can be stated exactly, and so that future work can attempt to prove the inverse theorem against a fixed, unambiguous formal standard.

/-- A finite set is approximately carried by a Gaussian-like lattice if all but
`error` of its points lie in the lattice image.  This is deliberately weak:
future work can replace it by density-in-a-box, Freiman-isomorphism, or Hausdorff
distance variants without changing the physical statement. -/
def ApproxContainedInGaussianLikeLattice
    (A : Finset Point2) (Λ : GaussianLikeLattice) (error : ℕ) : Prop :=
  ∃ A₀ : Finset Point2,
    A₀ ⊆ A ∧
      A.card ≤ A₀.card + error ∧
      ∀ a ∈ A₀, ∃ z : Fin 2 → ℤ, Λ.basis z = a

/-- A rank-two lattice-like carrier in the visible plane, recorded only at the
level needed for the inverse theorem target.  The `basis` map is the proposed
Gaussian-integer coordinate chart; `integral_norm` says visible squared norm is
read from an integral positive binary quadratic form after scaling. -/
structure GaussianLikeLattice where
  basis : (Fin 2 → ℤ) → Point2
  scale : ℝ
  scale_pos : 0 < scale
  qform : (Fin 2 → ℤ) → ℤ
  qform_nonneg : ∀ z, 0 ≤ qform z
  integral_norm :
    ∀ z, normSq (basis z) = scale * (qform z : ℝ)

/-- The inverse theorem target left by the RS physicalization:
small cross-norm alphabet at the Landau-Ramanujan scale forces the visible
points to be approximately carried by a Gaussian-integer-like lattice.

This is not asserted as proved here; it is the exact classical lemma needed to
turn the RS physical statement into a conventional proof. -/
def PlanarNormFiberRigidityTarget : Prop :=
  ∀ᶠ n in atTop,
    ∀ P Q : Finset Point2,
      P.card = n →
      Q.card = n →
      ((crossNormSqAlphabet P Q).card : ℝ) ≤
          (n : ℝ) / Real.sqrt (Real.log n) →
        ∃ Λ : GaussianLikeLattice,
          ApproxContainedInGaussianLikeLattice P Λ (n / 100) ∧
          ApproxContainedInGaussianLikeLattice Q Λ (n / 100)

What this page does not claim

No theorem asserts that any particular set is approximately contained in a Gaussian-like lattice. The inverse theorem PlanarNormFiberRigidityTarget is not proved; it is an open target. The approximation error bound of n divided by 100 is not claimed to be optimal.

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/Mathematics/BipartiteDistanceSpectrum.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: