Encyclopedia Gravity Gravity Seven Gaps Recognition Ratio Bridge

ARTICLE 4 claims 3 theorems 1 model

Gravity Seven Gaps Recognition Ratio Bridge

A bridge in a machine-checked library that connects a ledger of recognition events to geometric curvature, and settles a sign disagreement between two ways of measuring a deficit.

Verify this page

The recognition-ratio bridge

The recognition-ratio bridge is a formal structure in the Recognition Science framework's machine-checked library. It encodes a specific relation between two kinds of quantities at a hinge, a point where discrete pieces of a geometric surface meet. The relation says the logarithm of a positive comparison ratio, x, is approximately equal to a coupling constant, kappa, times a geometric deficit, delta, with a small remainder that shrinks like the cube of the mesh scale. In plain terms, it is a proposed law connecting a discrete record of events, a ledger, to the curvature of a continuous shape.

The main achievement is reconciling this bridge with earlier negative results. A previous form of the bridge, which equated a ledger deficit directly to a signed geometric deficit, was refuted: ledger deficits are nonnegative, while geometric deficits can be signed. The new bridge avoids this contradiction by using a ratio, not a direct equality. The module proves that for any real number d, there exists an exact bridge on two hinges with geometric deficits d and -d. This shows the bridge can accommodate negative geometric deficits without violating the nonnegativity of the ledger deficit, because the two quantities are different observables.

The library proves that the cost function, J(x) = (x + 1/x)/2 - 1, applied to the ratio, equals cosh(log x) - 1. This means the cost depends only on the even part of the relation and is unchanged if the sign of the geometric deficit is flipped. The module also proves a quadratic approximation: for small deficits, the cost is approximately (kappa * delta)^2 / 2, with a quartic error term. This holds exactly when the remainder bound is zero, and with an additional explicit perturbation term otherwise.

In Recognition Science, this bridge is a MODEL tier structure, an explicit admissibility hypothesis from a physics paper, not yet derived from deeper principles. The named theorems about its properties are THEOREM tier, proved with no axioms beyond the standard three. The derivation of the ratio relation from stationarity of the ledger action remains OPEN. The module also records that the asymptotic family as mesh scale goes to zero is OPEN, with the remainder clause stated at one fixed mesh only.

THEOREM ratioBridge_admits_negative_deficit · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean
ratioBridge_admits_negative_deficit · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean:175 
/-- **THEOREM (escape from the sign no-go, strong universal form).** For
EVERY d there is an EXACT (remBound = 0), UNIT-COUPLED (kappa = 1)
recognition-ratio bridge on two hinges whose geometric deficit takes the
prescribed values d at hinge 0 and -d at hinge 1. For d > 0 the deficit at
hinge 1 is strictly negative, which
`bridge_forces_nonneg_geometricDeficit` proves impossible for the old
deficit-equality form: the odd log-ratio form escapes the sign obstruction
with no free field absorbing the content. -/
theorem ratioBridge_admits_negative_deficit (d : ℝ) :
    ∃ B : RecognitionRatioBridge (Fin 2),
      B.remBound = 0 ∧ (∀ σ, B.kappa σ = 1) ∧
      B.geometricDeficit 0 = d ∧ B.geometricDeficit 1 = -d :=
  ⟨twoHingeWitnessBridge d, rfl, fun _ => rfl,
    (twoHingeWitnessBridge_deficit d).1, (twoHingeWitnessBridge_deficit d).2⟩
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 _
THEOREM ratioBridge_jcost_quadratic · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean
ratioBridge_jcost_quadratic · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean:334 
/-- **THEOREM (exact quadratic expansion).** For an exact bridge with small
response |kappa sigma * delta sigma| <= 1:

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

Same numeric lemma `Jcost_exp_sub_half_sq_abs_le` as the quadratic-energy
matching of `LedgerEnergyBridge`. -/
theorem ratioBridge_jcost_quadratic {H : Type*}
    (B : RecognitionRatioBridge H) (hB : B.remBound = 0) (σ : H)
    (hsmall : |B.kappa σ * B.geometricDeficit σ| ≤ 1) :
    |Cost.Jcost (B.xRatio σ)
        - (B.kappa σ * B.geometricDeficit σ) ^ 2 / 2|
      ≤ (B.kappa σ * B.geometricDeficit σ) ^ 4 / 2 := by
  rw [xRatio_eq_exp_of_exact B hB σ]
  exact Jcost_exp_sub_half_sq_abs_le _ hsmall
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 is not derived from more fundamental principles; it is an explicit hypothesis. The module does not prove that the ledger deficit can be negative. The asymptotic behavior of the bridge as mesh scale goes to zero is not established.

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