Foundation Closed Observable Framework Continuity From Finite Description

The finite-description seam

In mathematics and physics, a continuity condition often appears as a technical convenience: assume the function is smooth, and the proofs go through. The Recognition Science declaration ContinuityFromFiniteDescription takes a different stance. It packages the assumption as a named, auditable obligation, one that must be supplied before a broader reconstruction theorem can fire. The declaration itself is a structure, a formal container, that holds exactly one field: the function J is continuous on the positive real numbers. That is all it asserts.

The name carries the intended story. A ledger, a discrete record of events, should be describable by a finite list of states, with no continuous dials left over. The framework's ClosedObservableFramework structure encodes this as two fields: the state space is countable, and no injective embedding of the real line into it exists. The declaration ContinuityFromFiniteDescription is the extracted continuity obligation from that finite-description seam. It does not show that a countable state space yields continuity; it records the continuity assumption as a separate, checkable hypothesis.

The payoff is architectural. The older RegularityCert bundle lumped continuity, strict convexity, and a calibration condition into one opaque record. The newer split obligations, of which this declaration is one, let each assumption be audited independently. A theorem composition_from_continuity then shows that, given continuity on the positive reals, the composition expression J(xy) + J(x/y) is always finite. That finiteness is a step toward the cost function, the measure of mismatch between two observed ratios, that the framework forces.

What the declaration does not claim matters as much. It does not assert that continuity is a consequence of finite description; the structure is a hypothesis, not a theorem. It does not establish the full functional equation for J, nor the golden ratio, nor any physical constant. Those results live downstream, in other files, and they require the three split obligations together. The declaration is a seam, a place where the framework says: here is the assumption you must supply, and here is what it buys you.

/-- Continuity obligation extracted from the finite-description seam. -/
structure ContinuityFromFiniteDescription (J : ℝ → ℝ) : Prop where
  continuous : ContinuousOn J (Set.Ioi 0)

/-- Continuity obligation extracted from the finite-description seam. -/
structure ContinuityFromFiniteDescription (J : ℝ → ℝ) : Prop where
  continuous : ContinuousOn J (Set.Ioi 0)

/-- **R6 as theorem**: Compositional closure follows from continuity.
If J is continuous on R_{>0}, then J(xy) + J(x/y) is finite. -/
theorem composition_from_continuity
    (J : ℝ → ℝ)
    (hJ_cont : ContinuousOn J (Set.Ioi 0))
    (x y : ℝ) (hx : 0 < x) (hy : 0 < y) :
    ∃ v : ℝ, J (x * y) + J (x / y) = v :=
  ⟨J (x * y) + J (x / y), rfl⟩

What this page does not claim

Continuity is not derived from the countable-state or no-continuous-moduli axioms. The declaration does not establish the functional equation J(x) = (x + 1/x)/2 - 1. No physical constant, such as the golden ratio, follows from this declaration alone.

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