Gravity Seven Gaps Recognition Ratio Bridge Jcost Of Ratio Bridge Even In Defici

The even cost of a sign flip

In the Recognition Science framework, a ledger is a discrete record of events, and each event carries a cost, a forced price of recognition. The cost function J is not chosen freely; it is proved to equal (x + 1/x)/2 - 1 for any positive ratio x. This page concerns a bridge structure that connects a ledger to a geometric description, and a specific theorem about what happens to the cost when a geometric deficit changes sign.

The classical fact at the center is the hyperbolic cosine identity. For any real number a, the cost function satisfies J(exp(a)) = cosh(a) - 1. Since cosh is an even function, cosh(a) = cosh(-a), the cost is unchanged when a is replaced by its negative. The theorem jcost_of_ratioBridge_even_in_deficit applies this identity to a bridge that relates a positive comparison ratio x at each hinge to a geometric deficit delta via log x = kappa * delta, in the exact case where the remainder term is zero.

The theorem states: given two such bridges at the same hinge, with the same coupling kappa, and with geometric deficits that are exact opposites (delta_2 = -delta_1), the recognition costs are equal. The proof is a direct application of the cosh identity: the cost of the ratio is cosh(kappa * delta) - 1, and cosh does not see the sign of its argument. This is a THEOREM in the machine-checked library of formal theorems, with no unproved assumptions beyond the bridge structure itself.

This result matters because it separates two observables. The geometric deficit is signed: it can be positive or negative, and flipping it changes the geometry. But the recognition cost, as a function of the ratio, is even: it sees only the magnitude of the distortion, not its direction. The framework's no-go results constrain the ledger deficit, which is nonnegative and even; the bridge keeps the signed information in the logarithm of the ratio. The evenness of the cost is a consistency check, not a contradiction.

The theorem does not claim that the bridge relation itself is derived from first principles. The bridge structure is an explicit admissibility hypothesis, a MODEL tier choice, not a proved consequence. The derivation of the ratio relation from stationarity of the ledger action remains OPEN. The theorem also does not claim anything about the inexact case with a nonzero remainder; the evenness result holds only when the remainder bound is exactly zero.

/-- **THEOREM.** For any bridge and hinge, the J-cost of the comparison
ratio is cosh of its logarithm minus one. Since cosh is even, the ledger
cost is blind to the sign of log x_sigma. -/
theorem jcost_of_ratioBridge_cosh {H : Type*}
    (B : RecognitionRatioBridge H) (σ : H) :
    Cost.Jcost (B.xRatio σ)
      = Real.cosh (Real.log (B.xRatio σ)) - 1 := by
  conv_lhs => rw [← Real.exp_log (B.xRatio_pos σ)]
  exact Cost.Jcost_exp_cosh _

/-- **THEOREM (J-cost parity).** For two exact bridges whose deficits at a
hinge differ by a sign flip while the couplings agree, the J-costs of the
comparison ratios are EQUAL: the per-hinge ledger cost is parity-blind,
exactly as the parity no-gos require, while the signed deficit information
survives in log x_sigma. -/
theorem jcost_of_ratioBridge_even_in_deficit {H : Type*}
    (B₁ B₂ : RecognitionRatioBridge H)
    (h₁ : B₁.remBound = 0) (h₂ : B₂.remBound = 0) (σ : H)
    (hκ : B₂.kappa σ = B₁.kappa σ)
    (hδ : B₂.geometricDeficit σ = - B₁.geometricDeficit σ) :
    Cost.Jcost (B₂.xRatio σ) = Cost.Jcost (B₁.xRatio σ) := by
  rw [jcost_of_exact_ratioBridge B₁ h₁ σ, jcost_of_exact_ratioBridge B₂ h₂ σ,
    hκ, hδ, mul_neg, Real.cosh_neg]

/-- **MODEL (explicit hypothesis, the paper's Def 6.2 recognition-ratio
admissibility clause; NOT yet derived, derivation target is wave 1b).**

A recognition-ratio bridge on a hinge type `H` assigns to each hinge
`sigma` a positive comparison ratio `xRatio sigma`, a coupling
`kappa sigma`, and a SIGNED geometric deficit `geometricDeficit sigma`,
together with a mesh scale `meshScale` and a remainder constant `remBound`,
subject to the odd admissibility relation

  |log (xRatio sigma) - kappa sigma * geometricDeficit sigma|
    <= remBound * meshScale ^ 3.

Scope note: this records the paper's remainder clause AT A FIXED MESH; the
h -> 0 asymptotic family behind the O(h^3) notation is not yet formalized
(open, lane 2). Contrast with the REFUTED
`LedgerToHingeBridge.bridge_assumed` (ledger deficit = geometric deficit):
here the relation is carried by log x, which can take either sign, and the
reconciliation with the sign and parity no-gos is proved below
(`ratioBridge_admits_negative_deficit`,
`ratioBridge_separates_deficit_observables`). -/
structure RecognitionRatioBridge (H : Type*) where
  /-- The positive comparison ratio x_sigma at each hinge. -/
  xRatio : H → ℝ
  /-- Positivity of the comparison ratio. -/
  xRatio_pos : ∀ σ, 0 < xRatio σ
  /-- The hinge coupling kappa_sigma. -/
  kappa : H → ℝ
  /-- The SIGNED geometric deficit delta_sigma at each hinge. -/
  geometricDeficit : H → ℝ
  /-- The mesh scale h. -/
  meshScale : ℝ
  /-- The mesh scale is positive. -/
  meshScale_pos : 0 < meshScale
  /-- The remainder constant of the cubic-mesh clause. -/
  remBound : ℝ
  /-- The remainder constant is nonnegative. -/
  remBound_nonneg : 0 ≤ remBound
  /-- The odd admissibility relation: log x_sigma matches
  kappa_sigma * delta_sigma up to the cubic mesh remainder. -/
  ratio_relation : ∀ σ,
    |Real.log (xRatio σ) - kappa σ * geometricDeficit σ|
      ≤ remBound * meshScale ^ 3

What this page does not claim

The bridge relation is not derived from first principles; it is a modeling assumption. The evenness result does not hold when the remainder bound is nonzero. The theorem does not assert that the geometric deficit itself is even; it remains signed.

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