Encyclopedia Gravity Gravity Seven Gaps Recognition Ratio Bridge Two Hinge Witness Ledger Deficit Eve

ARTICLE 4 claims 3 theorems 1 model

Gravity Seven Gaps Recognition Ratio Bridge Two Hinge Witness Ledger Deficit Eve

A two-hinge model shows why a ledger of recognition costs stays even when geometry flips sign, and why that parity is no contradiction.

Verify this page

The deficit parity witness

In the Recognition Science framework, a ledger is a discrete record of recognition events, each event carrying a nonnegative cost. A deficit is the difference between a ledger's cost and some baseline, and for a ledger it is always nonnegative. The declaration twoHingeWitness_ledger_deficit_even proves a parity fact about a specific two-hinge model: when you reverse the sign of a geometric deficit, the ledger deficit stays exactly the same. The geometric deficit, a signed quantity describing how much a hinge deviates from flat, flips from d to -d, but the ledger deficit, measured through the framework's cost function, is even in that parameter.

Why does the ledger stay even? The proof runs through the framework's cost function J(x) = (x + 1/x)/2 - 1, which the framework derives from five plain conditions. For a positive ratio x, J(x) equals cosh(log x) - 1, and cosh is an even function. The two-hinge witness bridge sets the ratio at one hinge to exp(d) and at the other to exp(-d). Reversing d swaps the two ratios, but cosh(log x) does not change because cosh is symmetric under sign reversal of its argument. So the ledger deficit, which is built from these J-costs, is identical for d and -d. The theorem states this equality for every real d and for both hinges of the model.

This parity result matters because it resolves an apparent tension. An earlier bridge form assumed that the ledger deficit equals a signed geometric hinge deficit, but that form fails: ledger deficits are nonnegative while signed geometric deficits can be negative. The framework's library refuted that old form. The framework instead uses an odd relation on a positive comparison ratio, not an equality of nonnegative deficits. The two-hinge witness shows the two observables are genuinely different: the geometric deficit is signed and odd, the ledger deficit is nonnegative and even. No contradiction remains, because the signed information lives in the ratio, not in the ledger deficit.

In Recognition Science, the theorem is machine-checked in the framework's library of formal theorems, with no unproved assumptions beyond the standard logical axioms. The bridge structure itself is a model, an explicit admissibility hypothesis from the framework, not something the framework derives. What remains open is deriving that ratio relation from stationarity of the ledger action, rather than positing it. The parity theorem is a precise, limited statement: it tells you how one observable behaves under sign flip, and it shows that behavior is consistent with the no-go results. It does not claim that geometry is even, nor that the bridge relation is derived, nor that the model describes actual gravity.

THEOREM twoHingeWitness_ledger_deficit_even · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean
twoHingeWitness_ledger_deficit_even · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean:232 
/-- **THEOREM.** The ledger deficit induced by the witness family is EVEN
under d -> -d, by direct application of the no-go's own family theorem
`ledger_family_deficit_even_of_ratio_parity` (with ratios r d sigma tau =
xRatio sigma / xRatio tau, parity-covariant by
`twoHingeWitnessBridge_xRatio_neg`). -/
theorem twoHingeWitness_ledger_deficit_even (d : ℝ) (σ : Fin 2) :
    RecognitionLedger.deficit
        (ratioBridgeLedger (twoHingeWitnessBridge (-d))) σ
      = RecognitionLedger.deficit
        (ratioBridgeLedger (twoHingeWitnessBridge d)) σ := by
  exact ledger_family_deficit_even_of_ratio_parity
    (fun ε => ratioBridgeLedger (twoHingeWitnessBridge ε))
    (fun ε i j =>
      (twoHingeWitnessBridge ε).xRatio i / (twoHingeWitnessBridge ε).xRatio j)
    (fun ε i j => div_pos ((twoHingeWitnessBridge ε).xRatio_pos i)
      ((twoHingeWitnessBridge ε).xRatio_pos j))
    (fun ε i j => ratioBridgeLedger_cost (twoHingeWitnessBridge ε) i j)
    (fun ε i j => by
      show (twoHingeWitnessBridge (-ε)).xRatio i
            / (twoHingeWitnessBridge (-ε)).xRatio j
          = ((twoHingeWitnessBridge ε).xRatio i
            / (twoHingeWitnessBridge ε).xRatio j)⁻¹
      rw [twoHingeWitnessBridge_xRatio_neg ε i,
        twoHingeWitnessBridge_xRatio_neg ε j, inv_div_inv, inv_div])
    d σ
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_separates_deficit_observables · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean
ratioBridge_separates_deficit_observables · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean:258 
/-- **THEOREM (deficit-observable separation: the reconciliation).** For
every d > 0 the exact, unit-coupled two-hinge witness simultaneously has:

* a SIGNED geometric deficit (value d at hinge 0, strictly negative value
  -d at hinge 1), which the sign no-go forbids for the LEDGER deficit; and
* an induced genuine `RecognitionLedger` whose deficit is NONNEGATIVE at
  every cell (`RecognitionLedger.deficit_nonneg`, the engine behind
  `bridge_forces_nonneg_geometricDeficit`) and EVEN under the sign flip
  d -> -d (`ledger_family_deficit_even_of_ratio_parity`, via
  `twoHingeWitness_ledger_deficit_even`).

The no-gos constrain the ledger deficit; the paper's odd bridge stores the
signed information in log x, hence in the geometric deficit. The two
observables are separated by this witness, so the no-gos and the paper's
bridge are jointly consistent. -/
theorem ratioBridge_separates_deficit_observables (d : ℝ) (hd : 0 < d) :
    (twoHingeWitnessBridge d).remBound = 0 ∧
    (∀ σ, (twoHingeWitnessBridge d).kappa σ = 1) ∧
    (twoHingeWitnessBridge d).geometricDeficit 0 = d ∧
    (twoHingeWitnessBridge d).geometricDeficit 1 < 0 ∧
    (∀ σ, 0 ≤ RecognitionLedger.deficit
        (ratioBridgeLedger (twoHingeWitnessBridge d)) σ) ∧
    (∀ σ, RecognitionLedger.deficit
          (ratioBridgeLedger (twoHingeWitnessBridge (-d))) σ
        = RecognitionLedger.deficit
          (ratioBridgeLedger (twoHingeWitnessBridge d)) σ) := by
  refine ⟨rfl, fun _ => rfl, (twoHingeWitnessBridge_deficit d).1, ?_,
    fun σ => RecognitionLedger.deficit_nonneg _ σ,
    fun σ => twoHingeWitness_ledger_deficit_even d σ⟩
  rw [(twoHingeWitnessBridge_deficit d).2]
  linarith
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 theorem does not claim that the geometric deficit is even; it stays signed. The theorem does not derive the bridge relation from first principles; that derivation remains open. The theorem does not claim the two-hinge model describes actual gravity; it is a witness example.

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