Encyclopedia Foundation Foundation Dimensional Constraints Cost Layer

ARTICLE 5 claims 5 theorems

Foundation Dimensional Constraints Cost Layer

A machine-checked package of theorems about the cost of recognition, used to support dimensional constraints in the framework.

Verify this page

The cost layer

The foundation dimensional constraints cost layer is a compact, public package of theorems about the cost function, the framework's measure of how much a recognition event deviates from a perfect match. It is a machine-checked collection of formal theorems, meaning every statement in it has been verified by a computer. The package exists to expose the cost-theoretic core needed for the dimensional constraints rebuttal, without importing confidential parts of the full development.

The central object is a structure called PublicCostLayer, which asserts that any admissible cost functional agrees with the unique cost function J(x) = (x + 1/x)/2 - 1 on positive real numbers. This is the canonical result that any cost function satisfying five plain conditions must equal this form. In logarithmic coordinates, this cost is simply cosh t - 1, a fact that makes the symmetry of the cost explicit.

The package establishes several key properties of this cost function. The identity ratio, where x = 1, has zero cost. Reciprocal ratios, x and 1/x, have equal cost, reflecting the symmetry of the function. The cost is nonnegative for all positive ratios, and its unique positive zero is exactly x = 1. Near zero, the cost grows without bound, meaning the defect exceeds any prescribed bound as the ratio approaches zero.

In Recognition Science, this cost layer is the foundation for the dimensional constraints argument. The theorem public_cost_layer proves that this structure is available in the current public framework. The cost function's uniqueness and its properties are what allow the framework to derive further structural results, including the eight-tick recognition cycle and the three spatial dimensions. The layer is a public, reusable core that the dimensional constraints rebuttal can cite without exposing the full development.

The practical consequence is that the cost layer provides a clean, verified foundation for the dimensional constraints argument. It packages the cost-theoretic results in a compact namespace, making them easy to reference in the formal development. This is not a new theorem but a public interface to existing results, ensuring the rebuttal rests on solid, machine-checked ground.

THEOREM PublicCostLayer · IndisputableMonolith/Foundation/DimensionalConstraints/CostLayer.lean
PublicCostLayer · IndisputableMonolith/Foundation/DimensionalConstraints/CostLayer.lean:23 
/-- Public cost layer used in the dimensional-constraints rebuttal. -/
structure PublicCostLayer : Prop where
  /-- Any admissible cost functional agrees with `Jcost` on positive reals via
      the canonical primitive-to-uniqueness T5 route. -/
  unique_on_pos :
    ∀ (F : ℝ → ℝ),
      Cost.FunctionalEquation.PrimitiveCostHypotheses F →
      Cost.FunctionalEquation.AczelRegularityKernel (Cost.FunctionalEquation.H F) →
      ∀ {x : ℝ}, 0 < x → F x = Cost.Jcost x
  /-- In logarithmic coordinates, the cost is `cosh t - 1`. -/
  log_closed_form :
    ∀ t : ℝ, Cost.Jlog t = Real.cosh t - 1
  /-- The identity ratio has zero cost. -/
  normalized : Cost.Jcost 1 = 0
  /-- Reciprocal ratios have equal cost. -/
  reciprocal :
    ∀ {x : ℝ}, 0 < x → Cost.Jcost x = Cost.Jcost x⁻¹
  /-- The cost is nonnegative on positive ratios. -/
  nonnegative :
    ∀ {x : ℝ}, 0 < x → 0 ≤ Cost.Jcost x
  /-- The unique positive zero of the cost is `x = 1`. -/
  zero_iff_one :
    ∀ {x : ℝ}, 0 < x → (Cost.Jcost x = 0 ↔ x = 1)
  /-- Near zero, the defect exceeds every prescribed bound. -/
  null_barrier :
    ∀ C : ℝ, ∃ ε > 0, ∀ x : ℝ, 0 < x → x < ε →
      C < Foundation.LawOfExistence.defect x
THEOREM PublicCostLayer · IndisputableMonolith/Foundation/DimensionalConstraints/CostLayer.lean
PublicCostLayer · IndisputableMonolith/Foundation/DimensionalConstraints/CostLayer.lean:23 
/-- Public cost layer used in the dimensional-constraints rebuttal. -/
structure PublicCostLayer : Prop where
  /-- Any admissible cost functional agrees with `Jcost` on positive reals via
      the canonical primitive-to-uniqueness T5 route. -/
  unique_on_pos :
    ∀ (F : ℝ → ℝ),
      Cost.FunctionalEquation.PrimitiveCostHypotheses F →
      Cost.FunctionalEquation.AczelRegularityKernel (Cost.FunctionalEquation.H F) →
      ∀ {x : ℝ}, 0 < x → F x = Cost.Jcost x
  /-- In logarithmic coordinates, the cost is `cosh t - 1`. -/
  log_closed_form :
    ∀ t : ℝ, Cost.Jlog t = Real.cosh t - 1
  /-- The identity ratio has zero cost. -/
  normalized : Cost.Jcost 1 = 0
  /-- Reciprocal ratios have equal cost. -/
  reciprocal :
    ∀ {x : ℝ}, 0 < x → Cost.Jcost x = Cost.Jcost x⁻¹
  /-- The cost is nonnegative on positive ratios. -/
  nonnegative :
    ∀ {x : ℝ}, 0 < x → 0 ≤ Cost.Jcost x
  /-- The unique positive zero of the cost is `x = 1`. -/
  zero_iff_one :
    ∀ {x : ℝ}, 0 < x → (Cost.Jcost x = 0 ↔ x = 1)
  /-- Near zero, the defect exceeds every prescribed bound. -/
  null_barrier :
    ∀ C : ℝ, ∃ ε > 0, ∀ x : ℝ, 0 < x → x < ε →
      C < Foundation.LawOfExistence.defect x
THEOREM PublicCostLayer · IndisputableMonolith/Foundation/DimensionalConstraints/CostLayer.lean
PublicCostLayer · IndisputableMonolith/Foundation/DimensionalConstraints/CostLayer.lean:23 
/-- Public cost layer used in the dimensional-constraints rebuttal. -/
structure PublicCostLayer : Prop where
  /-- Any admissible cost functional agrees with `Jcost` on positive reals via
      the canonical primitive-to-uniqueness T5 route. -/
  unique_on_pos :
    ∀ (F : ℝ → ℝ),
      Cost.FunctionalEquation.PrimitiveCostHypotheses F →
      Cost.FunctionalEquation.AczelRegularityKernel (Cost.FunctionalEquation.H F) →
      ∀ {x : ℝ}, 0 < x → F x = Cost.Jcost x
  /-- In logarithmic coordinates, the cost is `cosh t - 1`. -/
  log_closed_form :
    ∀ t : ℝ, Cost.Jlog t = Real.cosh t - 1
  /-- The identity ratio has zero cost. -/
  normalized : Cost.Jcost 1 = 0
  /-- Reciprocal ratios have equal cost. -/
  reciprocal :
    ∀ {x : ℝ}, 0 < x → Cost.Jcost x = Cost.Jcost x⁻¹
  /-- The cost is nonnegative on positive ratios. -/
  nonnegative :
    ∀ {x : ℝ}, 0 < x → 0 ≤ Cost.Jcost x
  /-- The unique positive zero of the cost is `x = 1`. -/
  zero_iff_one :
    ∀ {x : ℝ}, 0 < x → (Cost.Jcost x = 0 ↔ x = 1)
  /-- Near zero, the defect exceeds every prescribed bound. -/
  null_barrier :
    ∀ C : ℝ, ∃ ε > 0, ∀ x : ℝ, 0 < x → x < ε →
      C < Foundation.LawOfExistence.defect x
THEOREM PublicCostLayer · IndisputableMonolith/Foundation/DimensionalConstraints/CostLayer.lean
PublicCostLayer · IndisputableMonolith/Foundation/DimensionalConstraints/CostLayer.lean:23 
/-- Public cost layer used in the dimensional-constraints rebuttal. -/
structure PublicCostLayer : Prop where
  /-- Any admissible cost functional agrees with `Jcost` on positive reals via
      the canonical primitive-to-uniqueness T5 route. -/
  unique_on_pos :
    ∀ (F : ℝ → ℝ),
      Cost.FunctionalEquation.PrimitiveCostHypotheses F →
      Cost.FunctionalEquation.AczelRegularityKernel (Cost.FunctionalEquation.H F) →
      ∀ {x : ℝ}, 0 < x → F x = Cost.Jcost x
  /-- In logarithmic coordinates, the cost is `cosh t - 1`. -/
  log_closed_form :
    ∀ t : ℝ, Cost.Jlog t = Real.cosh t - 1
  /-- The identity ratio has zero cost. -/
  normalized : Cost.Jcost 1 = 0
  /-- Reciprocal ratios have equal cost. -/
  reciprocal :
    ∀ {x : ℝ}, 0 < x → Cost.Jcost x = Cost.Jcost x⁻¹
  /-- The cost is nonnegative on positive ratios. -/
  nonnegative :
    ∀ {x : ℝ}, 0 < x → 0 ≤ Cost.Jcost x
  /-- The unique positive zero of the cost is `x = 1`. -/
  zero_iff_one :
    ∀ {x : ℝ}, 0 < x → (Cost.Jcost x = 0 ↔ x = 1)
  /-- Near zero, the defect exceeds every prescribed bound. -/
  null_barrier :
    ∀ C : ℝ, ∃ ε > 0, ∀ x : ℝ, 0 < x → x < ε →
      C < Foundation.LawOfExistence.defect x
THEOREM public_cost_layer · IndisputableMonolith/Foundation/DimensionalConstraints/CostLayer.lean
public_cost_layer · IndisputableMonolith/Foundation/DimensionalConstraints/CostLayer.lean:51 
/-- 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

This module does not itself prove the three-dimensionality of space. The cost layer does not introduce new axioms beyond the standard ones. The package does not derive the fine-structure constant or any coupling constant.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND