Foundation Recognition Lattice3

A lattice of costs

A lattice is a discrete grid of points. The foundation recognition lattice3 is a one-dimensional grid whose points are the powers of the golden ratio: ..., phi^-2, phi^-1, 1, phi, phi^2, ... . Each rung is a ratio of two quantities, and the framework measures the distance between rungs with a cost function J. This cost is not chosen freely; a proved theorem forces it to be J(x) = (x + 1/x)/2 - 1. At the rung where the ratio is 1, the cost is zero. Moving one step to phi costs J(phi), which is about 0.118.

The formal content is deliberately modest. It proves three general facts about this cost: the cost is zero when the ratio is 1, the cost is never negative for positive ratios, and the threshold phi - 3/2 is positive. These facts hold for any positive real numbers m and e, because the cost depends only on their ratio. A certificate structure packages these three facts together, and it is proved that such a certificate exists. Nothing is proved specific to a physical subject, because the quantities m and e are not defined in any domain's own terms.

In Recognition Science, the lattice is a model of discrete recognition events. The framework models a ledger, a discrete record of events, where each rung is a possible state of a ratio. The ground state sits at ratio 1, where the cost is zero. The first excited rung sits at phi, with a small positive cost. The threshold phi - 3/2 is a canonical number, about 0.118, that marks a boundary in the cost structure. The lattice structure is internally consistent: the cost behaves as a distance should, and the threshold is a well-defined positive number.

The value of this structure is not in the facts themselves, which are simple, but in what they enable. The lattice provides a concrete setting where the forced cost function can be applied to ratios. It is a template for how a domain-specific definition would work: one must define what m and e mean in that domain. The pattern is shown and is reusable. The framework's library, a machine-checked collection of formal theorems, records this pattern so that later work can build on it without re-proving the basics.

What this means in practice is that the lattice is a scaffold, not a finished building. It gives a precise language for talking about ratios and their costs, and it proves the minimal facts that any such structure must satisfy. A reader who wants to apply this to a real system must supply the missing piece: a definition of m and e in that system's own terms. Until then, the lattice remains a formal object with a clean structure and an open question about its physical interpretation.

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

What this page does not claim

This module proves nothing specific to any physical subject because m and e are undefined. The lattice is not claimed to be the physical structure of space or time. The cost function J is not derived in this module; it is imported from a prior theorem.

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