Encyclopedia Gravity Gravity Seven Gaps Ledger Energy Bridge Cosh Sub One Le Half Sq Mul Cosh

ARTICLE 3 claims 2 theorems 1 model

Gravity Seven Gaps Ledger Energy Bridge Cosh Sub One Le Half Sq Mul Cosh

A simple inequality about hyperbolic functions is the hinge that lets a discrete ledger of recognition costs approximate a geometric energy of curvature.

Verify this page

The cost of a small strain

The hyperbolic cosine function, written cosh, describes shapes like a hanging chain or a catenary. The declaration cosh_sub_one_le_half_sq_mul_cosh proves a bound on how much cosh t exceeds 1 for any real number t: the excess, cosh t − 1, is at most (t²/2) times cosh t. For small t, this says the excess grows no faster than the square of t, with a correction factor that itself grows only mildly. It is a standard analytic fact, and in the Recognition Science framework it becomes the first step in a bridge between two very different descriptions of a deforming space.

The framework models a physical system as a ledger, a discrete record of events, and assigns a cost to each event through a function J. For a small strain, a tiny deformation of a material, the cost J(exp t) equals cosh t − 1. The inequality therefore bounds the ledger's cost of a small strain by a quadratic term, t²/2, times a factor that stays close to 1 for small t. This is not an approximation; it is a proved theorem, valid for every real t, with no error term hidden. The bound is the engine behind a larger result: the ledger's total cost for a collection of small strains matches, up to a quartic error, a sum of squared differences, which is the discrete analog of a curvature energy.

The theorem does not claim that the ledger cost is exactly quadratic. The inequality is one-sided, an upper bound, and the true cost always sits above the quadratic term by a nonnegative remainder. It also does not claim that the bound is tight; the factor cosh t can be larger than 1, so the bound is loose for large t. The declaration is a lemma, not a physical law. It is a piece of the framework's machine-checked library, a formal theorem proved from the axioms of real analysis, and it earns its place only as a step toward the matching theorem that connects the ledger to geometry.

THEOREM cosh_sub_one_le_half_sq_mul_cosh · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
cosh_sub_one_le_half_sq_mul_cosh · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:135 
/-- **THEOREM (two-sided quadratic upper bound).**
cosh t − 1 ≤ (t²/2)·cosh t for ALL t. Combined with
`Cost.cosh_quadratic_lower_bound` (t²/2 ≤ cosh t − 1) this brackets the
ledger cell cost between two quadratic forms. -/
theorem cosh_sub_one_le_half_sq_mul_cosh (t : ℝ) :
    Real.cosh t - 1 ≤ t ^ 2 / 2 * Real.cosh t := by
  have hkey := Cost.cosh_minus_one_eq t
  have hs := abs_sinh_le_abs_mul_cosh (t / 2)
  have h1 : |Real.sinh (t / 2)| ^ 2 ≤ (|t / 2| * Real.cosh (t / 2)) ^ 2 := by
    have := mul_self_le_mul_self (abs_nonneg _) hs
    simpa [pow_two] using this
  have h2 : Real.sinh (t / 2) ^ 2 ≤ (t / 2) ^ 2 * Real.cosh (t / 2) ^ 2 := by
    rw [sq_abs] at h1
    rw [mul_pow, sq_abs] at h1
    exact h1
  have hC : Real.cosh (t / 2) ^ 2 ≤ Real.cosh t := by
    have h2m := Real.cosh_two_mul (t / 2)
    have harg : (2 : ℝ) * (t / 2) = t := by ring
    rw [harg] at h2m
    have hpyth := Real.cosh_sq_sub_sinh_sq (t / 2)
    nlinarith [sq_nonneg (Real.cosh (t / 2) - 1), Real.one_le_cosh (t / 2)]
  have hS_le : Real.sinh (t / 2) ^ 2 ≤ (t / 2) ^ 2 * Real.cosh t :=
    le_trans h2 (mul_le_mul_of_nonneg_left hC (sq_nonneg _))
  nlinarith [hkey, hS_le]
MODEL coboundaryStrainLedger · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
coboundaryStrainLedger · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:239 
/-- **THEOREM (the corrected ledger construction, coboundary scope).**
The J-ratio costs of a coboundary strain field form a genuine
`RecognitionLedger`: cost i j = J(exp(f i − f j)).
* symmetry from J(x) = J(1/x) (`Cost.Jcost_symm`),
* diagonal zero from J(1) = 0,
* nonnegativity from J ≥ 0 on positives,
* RCL subadditivity from the cocycle property
  exp(f i − f j)·exp(f j − f k) = exp(f i − f k) plus J-submultiplicativity
  (`Cost.Jcost_submult` in the proof; equivalently the d'Alembert identity
  `rclGate_Jcost_eq` with J(x/y) ≥ 0).
Scoped to coboundary strains: for general antisymmetric strains the gate
can fail (`general_antisymmetric_strain_can_violate_rcl`). -/
noncomputable def coboundaryStrainLedger {Λ : Type*} [Fintype Λ]
    [DecidableEq Λ] (f : Λ → ℝ) :
    RecognitionLedger.RecognitionLedger Λ where
  cost i j := Cost.Jcost (Real.exp (f i - f j))
  symmetric := by
    intro i j
    show Cost.Jcost (Real.exp (f i - f j)) = Cost.Jcost (Real.exp (f j - f i))
    have h : Real.exp (f j - f i) = (Real.exp (f i - f j))⁻¹ := by
      rw [← Real.exp_neg]
      congr 1
      ring
    rw [h]
    exact Cost.Jcost_symm (Real.exp_pos _)
  diagonal_zero := by
    intro i
    show Cost.Jcost (Real.exp (f i - f i)) = 0
    rw [sub_self, Real.exp_zero, Cost.Jcost_unit0]
  nonneg := fun i j => Cost.Jcost_nonneg (Real.exp_pos _)
  rcl_subadditive := by
    intro i j k
    show Cost.Jcost (Real.exp (f i - f k))
      ≤ RecognitionLedger.rclGate (Cost.Jcost (Real.exp (f i - f j)))
          (Cost.Jcost (Real.exp (f j - f k)))
    have hcomp : Real.exp (f i - f k)
        = Real.exp (f i - f j) * Real.exp (f j - f k) := by
      rw [← Real.exp_add]
      congr 1
      ring
    have hsub := Cost.Jcost_submult (Real.exp_pos (f i - f j))
      (Real.exp_pos (f j - f k))
    rw [hcomp]
    unfold RecognitionLedger.rclGate
    linarith
THEOREM rclGate_Jcost_eq · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean
rclGate_Jcost_eq · IndisputableMonolith/Gravity/SevenGaps/LedgerEnergyBridge.lean:227 
/-- **THEOREM (the panel's key identity).** The RCL gate evaluated on two
J-costs is EXACTLY the J-cost of the product ratio plus the J-cost of the
quotient ratio: R(J(x), J(y)) = J(xy) + J(x/y) for x, y > 0. Since
J(x/y) ≥ 0, the gate inequality J(xy) ≤ R(J(x), J(y)) follows with
identified slack J(x/y). Pure algebra from `Cost.dalembert_identity`. -/
theorem rclGate_Jcost_eq {x y : ℝ} (hx : 0 < x) (hy : 0 < y) :
    RecognitionLedger.rclGate (Cost.Jcost x) (Cost.Jcost y)
      = Cost.Jcost (x * y) + Cost.Jcost (x / y) := by
  have h := Cost.dalembert_identity hx hy
  unfold RecognitionLedger.rclGate
  linarith

What this page does not claim

The theorem does not claim the ledger cost is exactly quadratic; it only provides an upper bound. The theorem does not claim the bound is tight for large t, since cosh t can exceed 1. The theorem does not claim a physical law; it is a formal lemma within 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/Gravity/SevenGaps/LedgerEnergyBridge.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