Materials Superconductor Gap2 From Jcost

What the gap module proves

In Recognition Science, the cost function J(x) = (x + 1/x)/2 - 1 measures the price of a recognition event, a discrete record of a comparison. The module named materials superconductor gap2 from jcost defines a domain cost as J(m/e), where m and e are real numbers. The machine-checked library of formal theorems proves three facts about this definition: the cost is zero when m equals e, it is never negative when both inputs are positive, and the constant phi - 3/2 is positive. These are general properties of the cost function, not statements about superconductors.

The definition of domainCost does not reference any physical quantity. The symbols m and e are just real numbers; the module never says they are mass and charge, or anything else. The docstring records a research note: for cuprate superconductors, the ratio 2Delta/kTc is empirically between 4 and 8, and phi^4 = 6.85 is consistent with that range. But this is an idea for where the mathematics might go, not a result. The Lean file itself states this plainly: it proves nothing specific to the subject.

What the module does establish is a reusable template. It packages the three proved facts into a structure called SCGap2Cert, and proves that this structure is inhabited, meaning the facts are consistent and available. Any future work that wants to apply J to a superconductor must first define m and e in the subject's own terms. Until then, the gap prediction remains a hypothesis with a named falsifier: if a measured cuprate ratio falls outside the phi^4 band of roughly 4 to 8, the identification is falsified.

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]

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

What this page does not claim

The module does not prove any specific prediction about superconductors. The research note's phi^4 = 6.85 is not a derived result, only a consistent observation. No claim is made that m and e represent mass and charge.

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/Materials/SuperconductorGap2FromJCost.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: