Foundation Foundation

The foundation module

The recognition framework, a system that derives physical structure from the cost of recognizing events, builds its results in a machine-checked library of formal theorems. One early module, called foundation, establishes three general facts about the cost function cost, the price paid when one quantity is compared to another. These facts are deliberately abstract: they hold for any positive numbers, with no physical meaning attached yet.

The first fact is that the cost vanishes when the two quantities are equal. If you compare a number to itself, the cost is zero. The second is that the cost is never negative: comparing any positive number to another positive number gives a result at or above zero. The third is that a certain threshold value, defined as the golden ratio minus three halves, is positive. The golden ratio, approximately 1.618, minus 1.5 leaves about 0.118.

These three facts are proved in the framework's library. The module also bundles them into a single certificate structure, a formal object that packages the three guarantees together. The certificate exists, which means the three facts are consistent and available for later use.

In Recognition Science, the library states these results once, universally quantified, in a shared template file. The foundation module repeats them for its own subject. But the module defines its cost as the function applied to a ratio of two numbers m and e, without defining what m and e represent. The docstring is explicit: this proves nothing specific to the subject, because the quantities are not tied to any physical interpretation.

What the module does establish is a clean starting point. Any later work that defines m and e in physical terms can inherit these three guarantees. The threshold value, for instance, matches a strong coupling constant at the Z boson mass: the framework's value is 0.11803, while the measured Particle Data Group value is 0.1179, a deviation of about one hundredth of a standard deviation. That numerical agreement is a research note in the module, not a proved theorem. The proof that the threshold is positive is what the library checks.

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 that the strong coupling constant equals 0.11803. The module does not define what m and e represent physically. The module does not derive the golden ratio from the cost function.

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