Encyclopedia Gravity Gravity Seven Gaps Recognition Ratio Bridge Two Hinge Witness Bridge X Ratio Neg

ARTICLE 4 claims 2 theorems 2 models

Gravity Seven Gaps Recognition Ratio Bridge Two Hinge Witness Bridge X Ratio Neg

A machine-checked theorem shows that flipping the sign of a geometric deficit simply inverts a positive ratio, with the recognition cost unchanged.

Verify this page

The sign-flip witness

In the Recognition Science framework, a ledger (a discrete record of recognition events) assigns a nonnegative cost to every pair of events. A separate geometric object, a hinge, carries a signed deficit that can be positive or negative. An old bridge form tried to equate these two, but failed: ledger deficits are nonnegative, while hinge deficits can change sign. The framework's library of machine-checked formal theorems records that failure and then builds a new bridge using a positive comparison ratio at each hinge.

The new bridge posits that the logarithm of this ratio equals a coupling constant times the geometric deficit, up to a small remainder. The declaration twoHingeWitnessBridge_xRatio_neg proves a specific fact about a two-hinge witness family: if you negate the deficit parameter d, the ratio at each hinge becomes its reciprocal. In symbols, for the witness bridge built from -d, the ratio is the multiplicative inverse of the ratio from the bridge built from d. This is a theorem, verified with no unproved assumptions.

This sign-flip behavior matters because the recognition cost function J(x) = (x + 1/x)/2 - 1 is even under x -> 1/x. The theorem jcost_of_ratioBridge_even_in_deficit proves that the cost is unchanged when the deficit sign flips. Meanwhile, the induced ledger deficit, computed from the ratio, stays nonnegative and even under the flip, while the geometric deficit itself remains signed. The bridge therefore separates two observables: the ledger's nonnegative deficit and the hinge's signed deficit. The no-go result that killed the old bridge does not apply to this new form.

In Recognition Science, this witness is a model-tier structure: the bridge relation itself is an admissibility hypothesis, not yet derived from first principles. The theorems about it are proved, but the derivation of the relation from stationarity of the ledger action remains open. The framework claims the sign-flip fact and its cost invariance, not that this bridge is the final physical law.

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
THEOREM twoHingeWitnessBridge_xRatio_neg · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean
twoHingeWitnessBridge_xRatio_neg · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean:219 
/-- **THEOREM.** Ratio parity of the witness family: flipping the sign of d
inverts every comparison ratio. -/
theorem twoHingeWitnessBridge_xRatio_neg (d : ℝ) (σ : Fin 2) :
    (twoHingeWitnessBridge (-d)).xRatio σ
      = ((twoHingeWitnessBridge d).xRatio σ)⁻¹ := by
  show Real.exp (if σ = 0 then -d else -(-d))
      = (Real.exp (if σ = 0 then d else -d))⁻¹
  rw [← Real.exp_neg]
  congr 1
  by_cases h : σ = 0
  · rw [if_pos h, if_pos h]
  · rw [if_neg h, if_neg h]
THEOREM jcost_of_ratioBridge_even_in_deficit · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean
jcost_of_ratioBridge_even_in_deficit · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean:313 
/-- **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 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

This theorem does not claim the bridge relation is derived, only that it is an admissible model. It does not claim the ledger deficit can be negative; the theorem separates ledger and geometric observables. It does not claim the old bridge form is valid; that form is refuted.

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