Foundation Rs Falsifiability Master Thm3 Rsfalsifiability3 Cert

A certificate of three facts

A certificate is a formal bundle of facts. The declaration RSFalsifiability3Cert packages three statements about a function called cost, a measure of the price of a recognition event. The first fact: when the two inputs to the cost are equal and nonzero, the cost is zero. The second: for any two positive inputs, the cost is never negative. The third: a specific constant, the golden ratio minus three halves, is greater than zero.

These three facts are proved in the machine-checked library of formal theorems. The proofs are short and general. The first follows from dividing a number by itself. The second follows from a known property of the cost function on positive numbers. The third follows from the golden ratio being greater than 1.5, which is itself a proved fact.

The certificate bundles these three proved facts into a single object. It exists: the library constructs it explicitly. This means the bundle is inhabited, not merely describable.

What the certificate does not do is make any claim about a particular subject. The cost function it uses is defined as Jcost (m / e), where m and e are just real numbers. Nothing in the definition says what m or e mean. They could be masses, energies, or anything else. The research note attached to the module records where the idea was meant to go, but the note is not a result. To make this a theorem about a subject, someone would need to define m and e in that subject's own terms.

The certificate also does not establish the falsifiability of the whole framework. The library's docstring mentions falsification bands for several constants, but those bands are not part of the certificate. The certificate proves only the three general facts, nothing more.

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 RSFalsifiability3Cert := ⟨cert⟩

What this page does not claim

The certificate does not assign any physical meaning to the inputs m and e. The certificate does not prove the framework is falsifiable. The certificate does not establish any prediction about a measured constant.

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/Foundation/RS_FalsifiabilityMasterThm3.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: