Encyclopedia Gravity Gravity Seven Gaps Recognition Ratio Bridge Ratio Bridge Jcost Quadratic Inexact

ARTICLE 3 claims 2 theorems 1 model

Gravity Seven Gaps Recognition Ratio Bridge Ratio Bridge Jcost Quadratic Inexact

A machine-checked theorem shows how a geometric mismatch between two descriptions of spacetime is measured as a cost, and how that cost behaves when the mismatch is small.

Verify this page

The bridge's energy

In general relativity, a deficit angle is a measure of curvature concentrated at a point or hinge, the kind of singularity that appears in discrete models of spacetime. The framework's recognition account, the idea that reality keeps a discrete record of events, models the energy associated with such a hinge through a bridge relation. This relation compares a geometric deficit, the signed angle, with a positive ratio, and the theorem ratioBridge_jcost_quadratic_inexact proves a precise bound on how the resulting cost behaves for small deficits.

The bridge relation states that the logarithm of the ratio equals a coupling constant times the geometric deficit, plus a remainder that is bounded by a constant times the cube of the mesh scale. When the remainder is zero, the relation is exact. The theorem shows that the J-cost, the framework's energy function, is approximately half the square of the product of the coupling and the deficit. The error is bounded by a quartic term plus a perturbation that depends on the remainder bound and the mesh scale. This is a quadratic approximation with an explicit error estimate, valid when the product of coupling and deficit is small.

The theorem is proved in the framework's machine-checked library of formal theorems, with no admitted axioms. It relies on the fact that the J-cost equals cosh of the logarithm of the ratio minus one, and on a standard bound for the difference between cosh and a quadratic. The result is exact in the sense that the bound is proved for all values within the stated condition, not just asymptotically. It is a statement about the energy of a single hinge, not about the dynamics of the whole system.

What the theorem does not claim is that the bridge relation itself is derived from first principles. The relation is an explicit admissibility hypothesis, a model choice, not a consequence of the framework's axioms. The theorem also does not claim that the quadratic approximation is valid for large deficits; the bound requires the product of coupling and deficit to be at most one in absolute value. Finally, the theorem does not claim that the remainder term vanishes; it only bounds its effect on the cost. The relation between the ratio and the deficit is a modeling assumption, and the theorem is a precise statement about the consequences of that assumption.

THEOREM ratioBridge_jcost_quadratic_inexact · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean
ratioBridge_jcost_quadratic_inexact · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean:446 
/-- **THEOREM (inexact quadratic expansion of the bridge).** For ANY
recognition-ratio bridge (no exactness assumed) with small response
|kappa sigma * delta sigma| <= 1, writing R = remBound * meshScale^3 for
the remainder budget of `ratio_relation`:

  |J(x_sigma) - (kappa sigma * delta sigma)^2 / 2|
    <= (kappa sigma * delta sigma)^4 / 2 + 2 * cosh R * (R + R^2 / 2).

At remBound = 0 the perturbation term vanishes (cosh 0 * 0 = 0) and the
bound reduces to the exact statement `ratioBridge_jcost_quadratic`. This is
the theorem that actually consumes the remainder clause of the structure. -/
theorem ratioBridge_jcost_quadratic_inexact {H : Type*}
    (B : RecognitionRatioBridge H) (σ : H)
    (hsmall : |B.kappa σ * B.geometricDeficit σ| ≤ 1) :
    |Cost.Jcost (B.xRatio σ)
        - (B.kappa σ * B.geometricDeficit σ) ^ 2 / 2|
      ≤ (B.kappa σ * B.geometricDeficit σ) ^ 4 / 2
        + 2 * Real.cosh (B.remBound * B.meshScale ^ 3)
            * (B.remBound * B.meshScale ^ 3
                + (B.remBound * B.meshScale ^ 3) ^ 2 / 2) := by
  have hR0 : 0 ≤ B.remBound * B.meshScale ^ 3 :=
    mul_nonneg B.remBound_nonneg (pow_nonneg (le_of_lt B.meshScale_pos) 3)
  rw [jcost_of_ratioBridge_cosh B σ]
  exact cosh_sub_one_sub_half_sq_abs_le_of_near
    (B.kappa σ * B.geometricDeficit σ) (Real.log (B.xRatio σ))
    (B.remBound * B.meshScale ^ 3) hsmall hR0 (B.ratio_relation σ)
THEOREM jcost_of_ratioBridge_cosh · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean
jcost_of_ratioBridge_cosh · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean:295 
/-- **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 _
MODEL RecognitionRatioBridge · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean
RecognitionRatioBridge · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean:70 
/-- **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 derived from the framework's axioms. The quadratic approximation is valid for large deficits. The remainder term in the bridge relation vanishes.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND