Encyclopedia Gravity Gravity Seven Gaps Hinge Stationarity Core Constrained Equal Split Eq Iff

ARTICLE 3 claims 2 theorems 1 model

Gravity Seven Gaps Hinge Stationarity Core Constrained Equal Split Eq Iff

A machine-checked theorem shows the cheapest way to distribute a fixed total strain across many hinges is to divide it evenly, and it is the only way to do so.

Verify this page

The equal split theorem

The theorem constrained_equal_split_eq_iff concerns a problem of distributing a fixed total amount of strain across a number of hinges, the flexible joints where a discrete surface bends. The setting is a framework called Recognition Science, which models physical structure through a ledger, a discrete record of recognition events, where each event carries a cost, a number that measures how expensive that recognition is. The specific cost function at work here is J(x) = (x + 1/x)/2 - 1, a form that is proved to be forced by five plain conditions in the framework's machine-checked library of formal theorems.

The theorem states a precise fact about a constrained minimization. One can have n hinges and a fixed total budget of strain c to distribute among them. The theorem proves two things. First, the equal split, where every hinge receives c/n, achieves the lowest possible total cost among all distributions that meet the budget. Second, and this is the sharper content, the equal split is the only distribution that achieves that minimum. If any other distribution also reaches the same total cost, it must in fact be the equal split. The proof is a direct consequence of the strict convexity of the cost function: the hyperbolic cosine function, which appears in the cost, has a unique tangent line at each point, and this uniqueness forces the minimizer to be unique.

The theorem does not claim that this equal-split distribution is physically realized in any actual gravitational system. It is a statement about the mathematics of a particular cost function under a constraint. The framework's own documentation is explicit that the coupling term that links the cost to the strain budget is a model, a definitional choice, not a derived consequence of the bare ledger. The theorem takes that coupling as given and proves the optimization fact about it. It also does not claim that the equal split is the correct description of any observed hinge pattern in nature; that would require additional physical assumptions that are not part of this theorem.

What the theorem does establish is a clean structural fact that any theory built on this cost function must respect: under a fixed total strain, the cheapest configuration is the most uniform one, and it is uniquely so. This is a strong constraint on what kinds of non-uniform hinge patterns can be optimal in the framework. It rules out a whole class of candidate solutions that might otherwise seem plausible. The result is a building block, not a final physical prediction, and it shows how the framework's cost function imposes a strong preference for uniformity in constrained settings.

THEOREM constrained_equal_split · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean
constrained_equal_split · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean:391 
/-- **THEOREM (item 5, constrained equal split, lower bound).** Over the
constraint set {t | sum_i t_i = c}, the J-cost sum_i (cosh t_i - 1) is at
least n * (cosh(c/n) - 1): the equal split is optimal. Proved by summing
the tangent-line bound of cosh at c/n; the linear terms cancel against the
budget. NOTE the honest reading: this theorem extracts the equal-split
VALUE from the budget; it does not, and cannot, produce the budget itself
(see `budget_implies_ratio_without_stationarity`). -/
theorem constrained_equal_split (n : ℕ) (hn : 1 ≤ n) (c : ℝ)
    (t : Fin n → ℝ) (hbudget : ∑ i, t i = c) :
    (n : ℝ) * (Real.cosh (c / n) - 1) ≤ ∑ i, (Real.cosh (t i) - 1) := by
  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
  have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
  have hL : ∑ _i : Fin n,
      (Real.cosh (c / n) - Real.sinh (c / n) * (c / n))
      = (n : ℝ) * (Real.cosh (c / n) - Real.sinh (c / n) * (c / n)) := by
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  have hsum : ∑ i : Fin n,
      (Real.cosh (c / n) + Real.sinh (c / n) * (t i - c / n))
      ≤ ∑ i : Fin n, Real.cosh (t i) :=
    Finset.sum_le_sum fun i _ => cosh_tangent_line_le (c / n) (t i)
  have hsplit : ∑ i : Fin n,
      (Real.cosh (c / n) + Real.sinh (c / n) * (t i - c / n))
      = (n : ℝ) * Real.cosh (c / n) := by
    calc ∑ i : Fin n,
        (Real.cosh (c / n) + Real.sinh (c / n) * (t i - c / n))
        = ∑ i : Fin n,
            ((Real.cosh (c / n) - Real.sinh (c / n) * (c / n))
              + Real.sinh (c / n) * t i) :=
          Finset.sum_congr rfl fun i _ => by ring
      _ = (n : ℝ) * (Real.cosh (c / n) - Real.sinh (c / n) * (c / n))
            + Real.sinh (c / n) * c := by
          rw [Finset.sum_add_distrib, hL, ← Finset.mul_sum, hbudget]
      _ = (n : ℝ) * Real.cosh (c / n) := by
          field_simp
          ring
  have hR : ∑ i : Fin n, (Real.cosh (t i) - 1)
      = (∑ i : Fin n, Real.cosh (t i)) - (n : ℝ) := by
    rw [Finset.sum_sub_distrib, Finset.sum_const, Finset.card_univ,
      Fintype.card_fin, nsmul_eq_mul, mul_one]
  rw [hR]
  rw [hsplit] at hsum
  nlinarith [hsum]
THEOREM constrained_equal_split_eq_iff · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean
constrained_equal_split_eq_iff · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean:434 
/-- **THEOREM (item 5, equality characterization).** Under the budget
constraint, the constrained minimum n * (cosh(c/n) - 1) is attained IFF
the configuration is exactly the equal split t_i = c/n. -/
theorem constrained_equal_split_eq_iff (n : ℕ) (hn : 1 ≤ n) (c : ℝ)
    (t : Fin n → ℝ) (hbudget : ∑ i, t i = c) :
    (∑ i, (Real.cosh (t i) - 1) = (n : ℝ) * (Real.cosh (c / n) - 1)) ↔
      t = fun _ => c / n := by
  have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
  have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
  constructor
  · intro heq
    by_contra hnef
    obtain ⟨i₀, hi₀⟩ := Function.ne_iff.mp hnef
    have hlt : ∑ i : Fin n,
        (Real.cosh (c / n) + Real.sinh (c / n) * (t i - c / n))
        < ∑ i : Fin n, Real.cosh (t i) :=
      Finset.sum_lt_sum (fun i _ => cosh_tangent_line_le (c / n) (t i))
        ⟨i₀, Finset.mem_univ i₀,
          cosh_tangent_line_lt (c / n) (t i₀) hi₀⟩
    have hL : ∑ _i : Fin n,
        (Real.cosh (c / n) - Real.sinh (c / n) * (c / n))
        = (n : ℝ) * (Real.cosh (c / n) - Real.sinh (c / n) * (c / n)) := by
      rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin,
        nsmul_eq_mul]
    have hsplit : ∑ i : Fin n,
        (Real.cosh (c / n) + Real.sinh (c / n) * (t i - c / n))
        = (n : ℝ) * Real.cosh (c / n) := by
      calc ∑ i : Fin n,
          (Real.cosh (c / n) + Real.sinh (c / n) * (t i - c / n))
          = ∑ i : Fin n,
              ((Real.cosh (c / n) - Real.sinh (c / n) * (c / n))
                + Real.sinh (c / n) * t i) :=
            Finset.sum_congr rfl fun i _ => by ring
        _ = (n : ℝ) * (Real.cosh (c / n) - Real.sinh (c / n) * (c / n))
              + Real.sinh (c / n) * c := by
            rw [Finset.sum_add_distrib, hL, ← Finset.mul_sum, hbudget]
        _ = (n : ℝ) * Real.cosh (c / n) := by
            field_simp
            ring
    have hR : ∑ i : Fin n, (Real.cosh (t i) - 1)
        = (∑ i : Fin n, Real.cosh (t i)) - (n : ℝ) := by
      rw [Finset.sum_sub_distrib, Finset.sum_const, Finset.card_univ,
        Fintype.card_fin, nsmul_eq_mul, mul_one]
    rw [hsplit] at hlt
    rw [hR] at heq
    nlinarith [hlt, heq]
  · intro ht
    subst ht
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
MODEL sourcedAction · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean
sourcedAction · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean:213 
/-- The sourced action Phi(t) = sum_i (cosh t_i - 1) - (c/n) * sum_i t_i:
the J-cost of the per-tick strains (via J(exp t) = cosh t - 1,
`Cost.Jcost_exp_cosh`) plus an explicit deficit-source coupling of total
strength c = kappa*delta, split evenly across the n ticks. The coupling
term is the MODEL input; see the module header. -/
noncomputable def sourcedAction (n : ℕ) (c : ℝ) (t : Fin n → ℝ) : ℝ :=
  (∑ i, (Real.cosh (t i) - 1)) - c / n * ∑ i, t i

What this page does not claim

The theorem does not claim that the equal-split distribution is physically realized in any actual gravitational system. The theorem does not claim that the coupling term is derived from the bare RecognitionLedger. The theorem does not claim that this cost function is the only possible one for all physical systems.

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/HingeStationarityCore.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