Foundation Primitive Recognition Calculus Prcchain Bridge Jcost Log Eq Clog One

The log-coordinate cost

The cost function J(x) = (x + 1/x)/2 - 1 measures the price of a recognition event in the framework's ledger, a discrete record of such events. The declaration jcost_log_eq_clog_one states that when you measure this cost not in the original units but in logarithmic coordinates, the formula becomes J(e^t) = cosh(t) - 1. This is the hyperbolic cosine, the curve a hanging chain makes, shifted down by one so that the cost is zero when the input is one, meaning no recognition event has occurred.

The significance is that this is the unique member of a family of cost functions with a particular symmetry property. The framework proves that any cost function satisfying five plain conditions must equal this J, and the log-coordinate form shows that this unique function has a second derivative of exactly 1 at the origin. This is the calibration condition: the cost's curvature at the unit is fixed, not chosen. The theorem is proved in a machine-checked library of formal theorems, meaning the derivation is verified step by step by a computer.

In the broader framework, this calibrated cost feeds a chain of further results. The first physical output of that chain is the golden ratio φ, which the framework derives as the unique self-similar scaling. The theorem also establishes that φ, along with the numbers 8 and 3 that appear later in the chain, all live in a countable field, a mathematical structure strictly smaller than the full continuum of real numbers. This means the framework's foundational chain runs on a countable carrier; it never needs the uncountable continuum at any of its rungs.

What the declaration does not claim is just as important. It does not claim that the cost function's form is an empirical fact; that is a theorem about a mathematical structure, not a measurement. It does not claim that the golden ratio, the number 8, or the number 3 are derived from the cost function alone; those are separate theorems in the chain. And it does not claim that the countable field is the only possible carrier for the framework; it establishes that this particular chain runs on it, not that no other construction could.

/-- `Cost.Jcost` in log coordinates is the `c = 1` member of the δ-forced cost
family: `Jcost(eᵗ) = cosh(1·t) − 1`. -/
theorem jcost_log_eq_clog_one (t : ℝ) :
    Cost.Jcost (Real.exp t) = Real.cosh (1 * t) - 1 := by
  simp only [Cost.Jcost, one_mul, Real.cosh_eq, Real.exp_neg]

/-- **Item 3, sharpened: every chain output lands in the countable field.** The
calibrated δ cost feeds the chain, and each of the chain's named outputs, the base
ratio φ (T6), the eight-tick cadence 8 = 2³ (T7), and the spatial dimension 3
(T8), is an element of the countable RS field. The forcing chain runs end to end on
a countable carrier; the continuum is never the home of any rung. -/
theorem rs_chain_all_rungs_in_field :
    deriv (deriv (fun t => Cost.Jcost (Real.exp t))) 0 = 1
      ∧ Real.goldenRatio ∈ MinimalField.rsField
      ∧ (8 : ℝ) ∈ MinimalField.rsField
      ∧ (3 : ℝ) ∈ MinimalField.rsField
      ∧ (MinimalField.rsField : Set ℝ).Countable :=
  ⟨jcost_logCurvature_one, phi_in_minimal_field,
    MinimalField.rsField_eight_tick, MinimalField.rsField_dimension,
    MinimalField.rsField_countable⟩

What this page does not claim

The cost function's form is an empirical measurement. The golden ratio, 8, or 3 are derived from the cost function alone. The countable field is the only possible carrier for the framework.

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/PrimitiveRecognitionCalculus/PRCChainBridge.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: