Information Moore Law Rs Moore Law Cert

The certificate and its limits

Moore's Law is the observation that the number of transistors on an integrated circuit tends to double every one and a half to two years. The Recognition Science library contains a declaration called MooreLawCert, a machine-checked certificate that bundles three proved facts about a certain cost function. The cost function is recognition cost: the price reality pays, in this framework, for recording a recognition event, measured here as a ratio between two quantities m and e.

The three proved facts are general properties of that cost function, not facts about transistors. First, when the two quantities are equal, the cost is zero. Second, for positive quantities, the cost is never negative. Third, the number phi minus 3/2 is positive, where phi is the golden ratio, about 1.618. The certificate simply packages these three facts together and proves that such a package exists. The name suggests a connection to Moore's Law, but the certificate itself says nothing about transistor counts, doubling times, or any empirical electronics data.

The library's own documentation is explicit on this point. The paragraph about transistor growth doubling every phi-years is a research note recording where the idea was meant to go, not a result. The certificate proves nothing specific to Moore's Law because its cost function is defined as J(m/e) without any reference to transistors. What would make this a theorem about Moore's Law is a definition of m and e in terms of actual chip data, and no such definition appears in the library.

In plain terms, MooreLawCert is a proof of three mathematical facts about a cost function, wrapped in a name that points toward an intended application. The application itself remains open. The certificate is a placeholder, not a derivation of Moore's Law.

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

MooreLawCert does not prove or predict any transistor growth rate. The certificate does not establish that the golden ratio governs Moore's Law. No empirical data about integrated circuits is used or cited in the certificate.

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/Information/Moore_Law_RS.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: