Foundation Dimensional Constraints Cost Layer Public Cost Layer

The public cost core

The declaration public_cost_layer is a packaged collection of formal theorems about a cost function. In the Recognition Science framework, a cost is a number assigned to a ratio between two quantities, measuring how far the ratio is from equality. This particular package is a compact, paper-specific namespace: it exposes just the statements needed for a rebuttal paper about dimensional constraints, without importing confidential parts of the full development.

The core content is a structure called PublicCostLayer, which is a proposition that bundles together several properties of the cost function. The central theorem states that any admissible cost functional agrees with the canonical form J(x) = (x + 1/x)/2 - 1 on positive real numbers, via the standard primitive-to-uniqueness route. In logarithmic coordinates, this cost takes the simpler form cosh t - 1. The package also establishes basic properties: the identity ratio has zero cost, reciprocal ratios have equal cost, the cost is nonnegative, the unique positive zero is at x = 1, and near zero the defect exceeds every prescribed bound.

In Recognition Science, this cost function is not chosen freely but forced by five plain conditions: reciprocal symmetry, zero cost at unity, a forced composition law, calibration, and continuity. The theorem that any admissible cost must equal J is proved in the framework's machine-checked library of formal theorems. The public_cost_layer declaration packages this result in a form suitable for the dimensional-constraints rebuttal paper.

What the declaration does not claim is equally important. It does not claim that the cost function is the only possible one without the five conditions; it only states the uniqueness result given those conditions. It does not claim anything about the physical interpretation of the cost, only its mathematical form. It does not claim that the dimensional constraints themselves are proved here; that is the subject of other files in the development.

/-- The public cost layer is available in the current public framework. -/
theorem public_cost_layer : PublicCostLayer := by
  refine
    { unique_on_pos := ?_
      log_closed_form := Cost.Jlog_as_cosh
      normalized := Cost.Jcost_unit0
      reciprocal := ?_
      nonnegative := ?_
      zero_iff_one := ?_
      null_barrier := Foundation.LawOfExistence.nothing_cannot_exist }
  · intro F hF hKernel x hx
    exact Cost.FunctionalEquation.primitive_to_uniqueness_of_kernel F hF hKernel x hx
  · intro x hx
    exact Cost.Jcost_symm hx
  · intro x hx
    exact Cost.Jcost_nonneg hx
  · intro x hx
    exact Cost.Jcost_eq_zero_iff x hx

/-- The public cost layer is available in the current public framework. -/
theorem public_cost_layer : PublicCostLayer := by
  refine
    { unique_on_pos := ?_
      log_closed_form := Cost.Jlog_as_cosh
      normalized := Cost.Jcost_unit0
      reciprocal := ?_
      nonnegative := ?_
      zero_iff_one := ?_
      null_barrier := Foundation.LawOfExistence.nothing_cannot_exist }
  · intro F hF hKernel x hx
    exact Cost.FunctionalEquation.primitive_to_uniqueness_of_kernel F hF hKernel x hx
  · intro x hx
    exact Cost.Jcost_symm hx
  · intro x hx
    exact Cost.Jcost_nonneg hx
  · intro x hx
    exact Cost.Jcost_eq_zero_iff x hx

/-- The public cost layer is available in the current public framework. -/
theorem public_cost_layer : PublicCostLayer := by
  refine
    { unique_on_pos := ?_
      log_closed_form := Cost.Jlog_as_cosh
      normalized := Cost.Jcost_unit0
      reciprocal := ?_
      nonnegative := ?_
      zero_iff_one := ?_
      null_barrier := Foundation.LawOfExistence.nothing_cannot_exist }
  · intro F hF hKernel x hx
    exact Cost.FunctionalEquation.primitive_to_uniqueness_of_kernel F hF hKernel x hx
  · intro x hx
    exact Cost.Jcost_symm hx
  · intro x hx
    exact Cost.Jcost_nonneg hx
  · intro x hx
    exact Cost.Jcost_eq_zero_iff x hx

What this page does not claim

The public cost layer does not prove the dimensional constraints themselves. It does not claim the cost function is unique without the five stated conditions. It does not provide a physical interpretation of 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/DimensionalConstraints/CostLayer.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: