Recognition Certification

Certificates of recognition

A certificate, in the Recognition Science framework, is a structured promise about a measurement. The framework models recognition as a ledger, a discrete record of events, and a certificate is the part of the ledger that vouches for a value. It names an interval, a lower and upper bound, and asserts that the true value lies inside that interval. The interval has a width, the difference between its endpoints, and the whole certificate is valid only when the lower bound is strictly positive, a condition the framework proves follows from validity itself.

The certificate carries two kinds of intervals. One is a residue interval per species, a range for the measured remainder after recognition. The other is a gap interval per integer charge, a range for the expected gap value. The certificate is valid when every residue interval sits inside its corresponding gap interval, and when the gap function itself lands inside the gap interval. From this schema, the framework proves a central inequality: if two measurements share the same integer charge, their residues differ by at most twice the gap tolerance. This is the anchor identity in inequality form, and it is what makes certificates useful: they bound how far apart two recognitions of the same charge can be.

The framework also defines a zero-width certificate, where every interval collapses to a single point. In that case the anchor identity becomes an exact equality, not an inequality: the residue equals the gap function exactly. This is the limiting case, the certificate that promises perfect agreement. The framework proves that this zero-width certificate is itself valid, so the exact equality is not an assumption but a derived consequence of the certificate schema.

In Recognition Science, the framework proves these bounds from the certificate structure alone, with no extra assumptions about the measurements. The practical meaning is that a certificate gives a quantitative handle on reproducibility: same charge, bounded difference. The framework's library, a machine-checked collection of formal theorems, records these proofs so that the bounds are not heuristic but derived. The value of the module is that it turns an intuitive notion, that measurements of the same thing should agree, into a precise inequality with a formal proof.

The framework's contribution here is modest but foundational. It does not say what the residue values are, nor what the gap function is. It says only that if you have a valid certificate, then certain bounds follow. That separation, between the certificate's data and the consequences of its validity, is what makes the module reusable. Any future theory that supplies a certificate automatically inherits these bounds.

/-- Equal‑Z degeneracy (inequality form) from a certificate. -/
lemma equalZ_residue_of_cert {Species : Type} {Z : Species → Int} {Fgap : Int → ℝ}
    {C : AnchorCert Species} (hC : Valid Z Fgap C)
  (res : Species → ℝ) (hres : ∀ i, memI (C.Ires i) (res i))
  {i j : Species} (hZ : Z i = Z j) :
  |res i - res j| ≤ 2 * C.eps (Z i) := by
  have hI_i : (Igap C (Z i)).lo ≤ (C.Ires i).lo ∧ (C.Ires i).hi ≤ (Igap C (Z i)).hi :=
    hC.Ires_in_Igap i
  have hI_j : (Igap C (Z j)).lo ≤ (C.Ires j).lo ∧ (C.Ires j).hi ≤ (Igap C (Z j)).hi :=
    hC.Ires_in_Igap j
  have hres_i : memI (Igap C (Z i)) (res i) := by
    have hr0 := hres i
    exact ⟨le_trans hI_i.1 hr0.1, le_trans hr0.2 hI_i.2⟩
  have hres_j : memI (Igap C (Z i)) (res j) := by
    have hr0 := hres j
    have hlo_j : (Igap C (Z i)).lo ≤ (C.Ires j).lo := by simpa [hZ] using hI_j.1
    have hhi_j : (C.Ires j).hi ≤ (Igap C (Z i)).hi := by simpa [hZ] using hI_j.2
    exact ⟨le_trans hlo_j hr0.1, le_trans hr0.2 hhi_j⟩
  have hbound :=
    abs_sub_le_width_of_memI (I := Igap C (Z i)) (x := res i) (y := res j) hres_i hres_j
  have hw :
      width (Igap C (Z i)) = 2 * C.eps (Z i) := by
    simp [Igap, width]
    ring
  simpa [hw, two_mul] using hbound

lemma zeroWidthCert_valid {Species : Type} (Z : Species → Int) (Fgap : Int → ℝ) :
    Valid Z Fgap (zeroWidthCert Z Fgap) := by
  refine {
    M0_pos := by simp [zeroWidthCert]
  , Fgap_in := by
      intro i
      dsimp [zeroWidthCert, Igap, memI]
      constructor <;> linarith
  , Ires_in_Igap := by
      intro i
      dsimp [zeroWidthCert, Igap]
      constructor <;> linarith
  }

/-- Exact anchor identity from a zero-width certificate. -/
lemma anchorIdentity_of_zeroWidthCert {Species : Type} (Z : Species → Int) (Fgap : Int → ℝ)
    (res : Species → ℝ) (hres : ∀ i, memI ((zeroWidthCert Z Fgap).Ires i) (res i)) :
  ∀ i : Species, res i = Fgap (Z i) := by
  intro i
  have h := hres i
  dsimp [zeroWidthCert, memI] at h
  exact le_antisymm h.2 h.1

What this page does not claim

No claim that certificates determine the actual values of residues or gap functions. No claim that the framework's certificates apply to any specific physical measurement outside the framework. No claim that the zero-width certificate is achievable in practice, only that it is formally valid.

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/Recognition/Certification.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: