Gravity Gravity Tidal Deform3 Cert

The certificate's scope

Tidal deformability measures how much a compact object, such as a neutron star, stretches in response to a companion's gravitational pull. In standard astrophysics, the dimensionless tidal deformability Λ of a neutron star is a number typically in the hundreds; a typical measured range is Λ ∼ 500–1000. The Recognition Science framework's declaration named TidalDeform3Cert does not compute that number. Instead, it packages three purely mathematical facts about a cost function, and the name is a research note, not a result.

The cost function is domainCost, defined as J(m/e), where J is the framework's forced cost function and m and e are positive real numbers. The three facts are: (1) when m equals e, the cost is zero; (2) for any positive m and e, the cost is nonnegative; (3) the constant φ − 3/2 is positive, where φ is the golden ratio. Each fact is proved in the machine-checked library of formal theorems, and the certificate simply bundles them into a structure with a proof of existence.

In Recognition Science, the framework models the cost of recognition events. The certificate's three facts are general properties of that cost, not results about gravity. The declaration's docstring says explicitly that it proves nothing specific to its subject, because the domain cost is defined without reference to tidal deformability. The research note records an intended comparison: Λ ∼ φ^13 ≈ 521, which is consistent with the observed range, but that comparison is not part of the certificate.

What the certificate does establish is that the cost function is well-behaved in a minimal sense: it has a zero at equality, is nonnegative, and has a positive threshold. These properties hold for any positive inputs, so they apply to any domain where m and e are defined. The certificate does not define m or e in terms of neutron-star mass and radius, so it cannot say anything about actual tidal deformability.

The practical upshot is a clean separation: the machine-checked part is trustworthy but generic, and the physical application remains a research idea. A reader should not mistake the certificate for a derivation of Λ from first principles. The framework's own library states that what would make this a theorem about its subject is a definition of m and e in that subject's own terms.

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

theorem cert_inhabited : Nonempty TidalDeform3Cert := ⟨cert⟩

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

The certificate does not compute a numerical value for tidal deformability. The certificate does not define m or e in terms of neutron-star mass and radius. The certificate does not prove the research note's comparison Λ ∼ φ^13 ≈ 521.

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