Encyclopedia Gravity Gravity Seven Gaps Recognition Ratio Bridge Cosh Sub One Sub Half Sq Abs Le Of N

ARTICLE 3 claims 3 theorems

Gravity Seven Gaps Recognition Ratio Bridge Cosh Sub One Sub Half Sq Abs Le Of N

A machine-checked bound shows how a cost function stays close to a simple square law when its input is near a known value, and where the approximation breaks down.

Verify this page

The near-match bound

The central object is the cost, a measure of how expensive a recognition event is. The framework's cost function is J(x) = (x + 1/x)/2 - 1, which for positive x equals cosh(log x) - 1. A natural question is how J behaves when its input is close to a reference value. The declaration cosh_sub_one_sub_half_sq_abs_le_of_near answers this: if a value t is within a small distance R of a reference a, and |a| ≤ 1, then the absolute difference between J(exp t) and a²/2 is bounded by a⁴/2 plus a term that grows with R and cosh R.

In plainer terms, the theorem says that when the deviation from the reference is small, the cost is approximately the square of that deviation divided by two. The quartic term a⁴/2 is the first correction, and the term involving R controls how much the approximation degrades as the input moves away. This is a local quadratic approximation with an explicit error bound, not an asymptotic statement. The bound is proved in the machine-checked library of formal theorems, with no unproved assumptions admitted.

The declaration is a lemma used to prove a larger result about gravity. In the Seven Gaps project, a bridge relation links a recognition ratio to a geometric deficit. The theorem ratioBridge_jcost_quadratic uses this lemma to show that, for an exact bridge with zero remainder, the cost equals (κδ)²/2 up to a quartic error, where κ is a coupling and δ is the deficit. The inexact version adds a perturbation term that depends on the remainder bound and the mesh scale cubed.

What the declaration does not claim is as important as what it proves. It does not establish that the approximation holds for all inputs, only for those near the reference with |a| ≤ 1. It does not prove that the bridge relation itself is derived from first principles; that derivation remains open. And it does not claim that the geometric deficit is nonnegative. In fact, a separate theorem shows that the geometric deficit can be negative while the ledger deficit, a different observable, stays nonnegative. The bound is a tool, not a physical law.

THEOREM cosh_sub_one_sub_half_sq_abs_le_of_near · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean
cosh_sub_one_sub_half_sq_abs_le_of_near · IndisputableMonolith/Gravity/SevenGaps/RecognitionRatioBridge.lean:396 
/-- **THEOREM (inexact quadratic expansion, generic form).** If
|t - a| <= R with 0 <= R and |a| <= 1, then

  |cosh t - 1 - a^2/2| <= a^4/2 + 2 * cosh R * (R + R^2/2).

The first term is the exact quartic remainder; the second is the explicit
perturbation cost of the inexactness. -/
theorem cosh_sub_one_sub_half_sq_abs_le_of_near (a t R : ℝ)
    (hsmall : |a| ≤ 1) (hR0 : 0 ≤ R) (hnear : |t - a| ≤ R) :
    |Real.cosh t - 1 - a ^ 2 / 2|
      ≤ a ^ 4 / 2 + 2 * Real.cosh R * (R + R ^ 2 / 2) := by
  have hexact : |Real.cosh a - 1 - a ^ 2 / 2| ≤ a ^ 4 / 2 := by
    have h := Jcost_exp_sub_half_sq_abs_le a hsmall
    rwa [Cost.Jcost_exp_cosh] at h
  have hpert := abs_cosh_add_sub_cosh_le a (t - a)
  rw [show a + (t - a) = t from by ring] at hpert
  have hcosha : Real.cosh a ≤ 2 := by
    have hmono : Real.cosh a ≤ Real.cosh 1 := by
      rw [Real.cosh_le_cosh]
      simpa using hsmall
    linarith [cosh_one_lt_two]
  have hcoshr : Real.cosh (t - a) ≤ Real.cosh R := by
    rw [Real.cosh_le_cosh, abs_of_nonneg hR0]
    exact hnear
  have hr2 : (t - a) ^ 2 ≤ R ^ 2 := by
    nlinarith [hnear, abs_nonneg (t - a), sq_abs (t - a)]
  have hnn : (0 : ℝ) ≤ |t - a| + (t - a) ^ 2 / 2 :=
    add_nonneg (abs_nonneg _) (by positivity)
  have hchain : Real.cosh a * Real.cosh (t - a) * (|t - a| + (t - a) ^ 2 / 2)
      ≤ 2 * Real.cosh R * (R + R ^ 2 / 2) := by
    have h1 : Real.cosh a * Real.cosh (t - a) ≤ 2 * Real.cosh R :=
      mul_le_mul hcosha hcoshr (le_of_lt (Real.cosh_pos _)) (by norm_num)
    have h2 : |t - a| + (t - a) ^ 2 / 2 ≤ R + R ^ 2 / 2 := by
      linarith [hnear, hr2]
    have h3 : (0 : ℝ) ≤ 2 * Real.cosh R :=
      mul_nonneg (by norm_num) (le_of_lt (Real.cosh_pos R))
    calc Real.cosh a * Real.cosh (t - a) * (|t - a| + (t - a) ^ 2 / 2)
        ≤ 2 * Real.cosh R * (|t - a| + (t - a) ^ 2 / 2) :=
          mul_le_mul_of_nonneg_right h1 hnn
      _ ≤ 2 * Real.cosh R * (R + R ^ 2 / 2) :=
          mul_le_mul_of_nonneg_left h2 h3
  have htri : |Real.cosh t - 1 - a ^ 2 / 2|
      ≤ |Real.cosh t - Real.cosh a| + |Real.cosh a - 1 - a ^ 2 / 2| := by
    have hsplit : Real.cosh t - 1 - a ^ 2 / 2
        = (Real.cosh t - Real.cosh a) + (Real.cosh a - 1 - a ^ 2 / 2) := by
      ring
    rw [hsplit]
    exact abs_add_le _ _
  linarith [htri, hpert, hexact, hchain]
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
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

What this page does not claim

The approximation does not hold for all inputs, only for those near the reference with |a| ≤ 1. The bridge relation itself is not derived from first principles; that derivation remains open. The geometric deficit is not claimed to be nonnegative; it can be negative while the ledger deficit stays nonnegative.

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