Encyclopedia Gravity Gravity Seven Gaps Hinge Stationarity Core Sourced Ratio Is Admissible
ARTICLE 4 claims 3 theorems 1 model
Gravity Seven Gaps Hinge Stationarity Core Sourced Ratio Is Admissible
A machine-checked proof shows how a specific strain ratio can be derived from minimizing a cost, and exactly where the model's input enters.
The sourced ratio
The declaration sourced_ratio_isAdmissible is a theorem in the Recognition Science library. It establishes that a particular construction, called the sourced ratio family, satisfies a formal admissibility predicate. In plain terms, the theorem proves that a ratio of recognition strains can be derived from a principle of minimizing a cost function, provided one explicitly adds a coupling term to that cost. The theorem is proved in the machine-checked library of formal theorems, with zero unproved axioms.
The construction begins with a cost function called recognition cost, a measure of the expense of a recognition event. The framework's core cost function is J(x) = (x + 1/x)/2 - 1. The sourced action adds a linear term to the sum of these costs: Phi(t) = sum_i (cosh t_i - 1) - (kappa*delta/n) * sum_i t_i. The theorem proves that this action has a unique global minimizer at t_i = arsinh(kappa*delta/n). This means that, for a given deficit delta and coupling strength kappa, the strain ratios that minimize the cost are all equal to that specific value.
The theorem then shows that this minimizer produces a ratio whose logarithm approximates kappa*delta with a cubic error term. The explicit bound is |n * arsinh(c/n) - c| <= |c|^3 / (6 n^2). This is the sourced stationary ratio. The admissibility predicate requires this approximation to hold uniformly for all mesh scales h below a threshold h0, with constants that do not depend on h. The theorem closes this requirement end-to-end, providing an explicit constant C_R = |kappa|^3 * C_K^3 * h0^3 / (6 n^2).
The theorem also records what it does not do. The coupling term -(kappa*delta/n) * sum_i t_i is a constitutive model choice, not a derived consequence of the bare recognition ledger. The docstring is explicit: this term is NOT derived from the bare RecognitionLedger, and no such derivation is claimed. The theorem's proof also requires a hypothesis bounding the deficit, and it passes through the curvature condition as a hypothesis rather than deriving it.
In Recognition Science, this result is part of a larger program to derive gravitational structure from recognition costs. The theorem provides a rigorous, kernel-checked foundation for one specific mechanism, while honestly flagging where a model input enters. It is a precise statement about a mathematical construction, not a claim about the physical universe.
THEOREM sourced_unique_minimizer · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean
/-- **THEOREM (item 3, sourced unique minimizer).** For every n (no
n >= 1 hypothesis is needed; at n = 0 both conjuncts are trivially true
on the empty tick set) and every total source strength c, the sourced
action
Phi(t) = sum_i (cosh t_i - 1) - (c/n) * sum_i t_i over t : Fin n → ℝ has
the unique global minimizer t_i = arsinh(c/n) for all i. The stationarity
condition sinh t_i = c/n is genuinely FORCED here (contrast with the
circular raw 1b route, `budget_implies_ratio_without_stationarity`), but
only because the deficit-source coupling was supplied as a MODEL input. -/
theorem sourced_unique_minimizer (n : ℕ) (c : ℝ) (t : Fin n → ℝ) :
sourcedAction n c (sourcedMinimizer n c) ≤ sourcedAction n c t ∧
(sourcedAction n c t = sourcedAction n c (sourcedMinimizer n c) →
t = sourcedMinimizer n c) :=
⟨sourced_minimizer_le n c t, sourced_minimizer_unique n c t⟩
THEOREM sourced_ratio_cubic_error · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean
/-- **THEOREM (item 4, cubic error of the sourced ratio, constant 1/6).**
|n * arsinh(c/n) - c| <= |c|^3 / (6 n^2) for n >= 1. This is the honest
form of the bridge expansion: the sourced stationary log ratio
n * arsinh(c/n) equals the deficit source c = kappa*delta up to an
explicitly bounded cubic error. -/
theorem sourced_ratio_cubic_error (n : ℕ) (hn : 1 ≤ n) (c : ℝ) :
|(n : ℝ) * Real.arsinh (c / n) - c|
≤ |c| ^ 3 / (6 * (n : ℝ) ^ 2) := by
have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0
have hkey : (n : ℝ) * Real.arsinh (c / n) - c
= (n : ℝ) * (Real.arsinh (c / n) - c / n) := by
field_simp
rw [hkey, abs_mul, abs_of_pos hn0]
have hcn : |c / (n : ℝ)| ^ 3 = |c| ^ 3 / (n : ℝ) ^ 3 := by
rw [abs_div, abs_of_pos hn0, div_pow]
calc (n : ℝ) * |Real.arsinh (c / n) - c / n|
≤ (n : ℝ) * (|c / (n : ℝ)| ^ 3 / 6) :=
mul_le_mul_of_nonneg_left (abs_arsinh_sub_self_le (c / n)) hn0.le
_ = |c| ^ 3 / (6 * (n : ℝ) ^ 2) := by
rw [hcn]
field_simp
THEOREM sourced_ratio_isAdmissible · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean
/-- **THEOREM (item 6, end-to-end admissibility of the sourced ratio).**
Under the curvature bound |delta(h)| <= C_K h^2 on (0, h0), the
sourced-stationary construction yields an admissible family with the
EXPLICIT uniform constant C_R = |kappa|^3 * C_K^3 * h0^3 / (6 n^2),
computed from the cubic error bound `sourced_ratio_cubic_error`:
|log x(h) - kappa*delta(h)| = |n*arsinh(kappa*delta(h)/n) - kappa*delta(h)|
<= |kappa*delta(h)|^3/(6n^2) <= (|kappa| C_K h^2)^3/(6n^2)
<= (|kappa|^3 C_K^3 h0^3/(6n^2)) * h^3 for h in (0, h0).
Two honest disclosures. (a) The curvature conjunct |delta(h)| <= C_K h^2
of the conclusion is a PASSTHROUGH of the hypothesis `hδ`, restated inside
the predicate only so the admissibility record is self-contained; the new
content of this theorem is entirely the bridge conjunct. (b) There is no
0 < h0 hypothesis: for h0 <= 0 the interval (0, h0) is empty and the
predicate is vacuously true, so adding positivity would not strengthen
the conclusion; the statement carries content exactly when 0 < h0. -/
theorem sourced_ratio_isAdmissible (n : ℕ) (hn : 1 ≤ n)
(h₀ kappa C_K : ℝ) (δ : ℝ → ℝ)
(hδ : ∀ h ∈ Set.Ioo (0 : ℝ) h₀, |δ h| ≤ C_K * h ^ 2) :
(sourcedRatioFamily n kappa δ).IsAdmissible h₀ kappa C_K
(|kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 / (6 * (n : ℝ) ^ 2)) := by
intro h hh
obtain ⟨hh1, hh2⟩ := hh
have hδh := hδ h ⟨hh1, hh2⟩
refine ⟨hδh, ?_⟩
have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
have hCK : 0 ≤ C_K := by
have hsq : (0 : ℝ) < h ^ 2 := by positivity
nlinarith [abs_nonneg (δ h), hδh, hsq]
have hh3 : h ^ 3 ≤ h₀ ^ 3 := pow_le_pow_left₀ hh1.le hh2.le 3
show |Real.log (Real.exp ((n : ℝ) * Real.arsinh (kappa * δ h / n)))
- kappa * δ h| ≤ _
rw [Real.log_exp]
have hnum : |kappa * δ h| ^ 3
≤ |kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 * h ^ 3 := by
have h1 : |kappa * δ h| ^ 3 = |kappa| ^ 3 * |δ h| ^ 3 := by
rw [abs_mul, mul_pow]
have h2 : |δ h| ^ 3 ≤ (C_K * h ^ 2) ^ 3 :=
pow_le_pow_left₀ (abs_nonneg _) hδh 3
have h3 : (C_K * h ^ 2) ^ 3 = C_K ^ 3 * (h ^ 3 * h ^ 3) := by ring
have h4 : C_K ^ 3 * (h ^ 3 * h ^ 3) ≤ C_K ^ 3 * (h₀ ^ 3 * h ^ 3) := by
refine mul_le_mul_of_nonneg_left ?_ (by positivity)
exact mul_le_mul_of_nonneg_right hh3 (by positivity)
calc |kappa * δ h| ^ 3 = |kappa| ^ 3 * |δ h| ^ 3 := h1
_ ≤ |kappa| ^ 3 * (C_K ^ 3 * (h₀ ^ 3 * h ^ 3)) := by
refine mul_le_mul_of_nonneg_left ?_ (by positivity)
calc |δ h| ^ 3 ≤ (C_K * h ^ 2) ^ 3 := h2
_ = C_K ^ 3 * (h ^ 3 * h ^ 3) := h3
_ ≤ C_K ^ 3 * (h₀ ^ 3 * h ^ 3) := h4
_ = |kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 * h ^ 3 := by ring
calc |(n : ℝ) * Real.arsinh (kappa * δ h / n) - kappa * δ h|
≤ |kappa * δ h| ^ 3 / (6 * (n : ℝ) ^ 2) :=
sourced_ratio_cubic_error n hn (kappa * δ h)
_ ≤ (|kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 * h ^ 3) / (6 * (n : ℝ) ^ 2) := by
have hden : (0 : ℝ) ≤ (6 * (n : ℝ) ^ 2)⁻¹ := by positivity
rw [div_eq_mul_inv, div_eq_mul_inv]
exact mul_le_mul_of_nonneg_right hnum hden
_ = |kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 / (6 * (n : ℝ) ^ 2) * h ^ 3 := by
ring
MODEL sourcedAction · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean
/-- 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 sourced ratio is derived from the bare recognition ledger without any additional model input. The theorem proves that the physical universe obeys this ratio. The curvature condition is derived from recognition principles; it is passed through as a hypothesis.
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:
- What is the physical interpretation of the deficit delta in the recognition ledger?
- How does the sourced ratio connect to the broader derivation of gravitational structure?
- What experimental or observational evidence could falsify the model choice of the coupling term?
- Does the admissibility predicate generalize to other cost functions beyond J?
- What is the status of deriving the curvature condition from recognition principles alone?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM sourced_unique_minimizer · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean
/-- **THEOREM (item 3, sourced unique minimizer).** For every n (no n >= 1 hypothesis is needed; at n = 0 both conjuncts are trivially true on the empty tick set) and every total source strength c, the sourced action Phi(t) = sum_i (cosh t_i - 1) - (c/n) * sum_i t_i over t : Fin n → ℝ has the unique global minimizer t_i = arsinh(c/n) for all i. The stationarity condition sinh t_i = c/n is genuinely FORCED here (contrast with the circular raw 1b route, `budget_implies_ratio_without_stationarity`), but only because the deficit-source coupling was supplied as a MODEL input. -/ theorem sourced_unique_minimizer (n : ℕ) (c : ℝ) (t : Fin n → ℝ) : sourcedAction n c (sourcedMinimizer n c) ≤ sourcedAction n c t ∧ (sourcedAction n c t = sourcedAction n c (sourcedMinimizer n c) → t = sourcedMinimizer n c) := ⟨sourced_minimizer_le n c t, sourced_minimizer_unique n c t⟩The sourced action has a unique global minimizer at t_i = arsinh(kappa*delta/n). sourced_unique_minimizer · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.leanTHEOREM sourced_ratio_cubic_error · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean
/-- **THEOREM (item 4, cubic error of the sourced ratio, constant 1/6).** |n * arsinh(c/n) - c| <= |c|^3 / (6 n^2) for n >= 1. This is the honest form of the bridge expansion: the sourced stationary log ratio n * arsinh(c/n) equals the deficit source c = kappa*delta up to an explicitly bounded cubic error. -/ theorem sourced_ratio_cubic_error (n : ℕ) (hn : 1 ≤ n) (c : ℝ) : |(n : ℝ) * Real.arsinh (c / n) - c| ≤ |c| ^ 3 / (6 * (n : ℝ) ^ 2) := by have hn0 : (0 : ℝ) < n := by exact_mod_cast hn have hne : (n : ℝ) ≠ 0 := ne_of_gt hn0 have hkey : (n : ℝ) * Real.arsinh (c / n) - c = (n : ℝ) * (Real.arsinh (c / n) - c / n) := by field_simp rw [hkey, abs_mul, abs_of_pos hn0] have hcn : |c / (n : ℝ)| ^ 3 = |c| ^ 3 / (n : ℝ) ^ 3 := by rw [abs_div, abs_of_pos hn0, div_pow] calc (n : ℝ) * |Real.arsinh (c / n) - c / n| ≤ (n : ℝ) * (|c / (n : ℝ)| ^ 3 / 6) := mul_le_mul_of_nonneg_left (abs_arsinh_sub_self_le (c / n)) hn0.le _ = |c| ^ 3 / (6 * (n : ℝ) ^ 2) := by rw [hcn] field_simpThe minimizer produces a ratio whose logarithm approximates kappa*delta with a cubic error term. sourced_ratio_cubic_error · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.leanTHEOREM sourced_ratio_isAdmissible · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean
/-- **THEOREM (item 6, end-to-end admissibility of the sourced ratio).** Under the curvature bound |delta(h)| <= C_K h^2 on (0, h0), the sourced-stationary construction yields an admissible family with the EXPLICIT uniform constant C_R = |kappa|^3 * C_K^3 * h0^3 / (6 n^2), computed from the cubic error bound `sourced_ratio_cubic_error`: |log x(h) - kappa*delta(h)| = |n*arsinh(kappa*delta(h)/n) - kappa*delta(h)| <= |kappa*delta(h)|^3/(6n^2) <= (|kappa| C_K h^2)^3/(6n^2) <= (|kappa|^3 C_K^3 h0^3/(6n^2)) * h^3 for h in (0, h0). Two honest disclosures. (a) The curvature conjunct |delta(h)| <= C_K h^2 of the conclusion is a PASSTHROUGH of the hypothesis `hδ`, restated inside the predicate only so the admissibility record is self-contained; the new content of this theorem is entirely the bridge conjunct. (b) There is no 0 < h0 hypothesis: for h0 <= 0 the interval (0, h0) is empty and the predicate is vacuously true, so adding positivity would not strengthen the conclusion; the statement carries content exactly when 0 < h0. -/ theorem sourced_ratio_isAdmissible (n : ℕ) (hn : 1 ≤ n) (h₀ kappa C_K : ℝ) (δ : ℝ → ℝ) (hδ : ∀ h ∈ Set.Ioo (0 : ℝ) h₀, |δ h| ≤ C_K * h ^ 2) : (sourcedRatioFamily n kappa δ).IsAdmissible h₀ kappa C_K (|kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 / (6 * (n : ℝ) ^ 2)) := by intro h hh obtain ⟨hh1, hh2⟩ := hh have hδh := hδ h ⟨hh1, hh2⟩ refine ⟨hδh, ?_⟩ have hn0 : (0 : ℝ) < n := by exact_mod_cast hn have hCK : 0 ≤ C_K := by have hsq : (0 : ℝ) < h ^ 2 := by positivity nlinarith [abs_nonneg (δ h), hδh, hsq] have hh3 : h ^ 3 ≤ h₀ ^ 3 := pow_le_pow_left₀ hh1.le hh2.le 3 show |Real.log (Real.exp ((n : ℝ) * Real.arsinh (kappa * δ h / n))) - kappa * δ h| ≤ _ rw [Real.log_exp] have hnum : |kappa * δ h| ^ 3 ≤ |kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 * h ^ 3 := by have h1 : |kappa * δ h| ^ 3 = |kappa| ^ 3 * |δ h| ^ 3 := by rw [abs_mul, mul_pow] have h2 : |δ h| ^ 3 ≤ (C_K * h ^ 2) ^ 3 := pow_le_pow_left₀ (abs_nonneg _) hδh 3 have h3 : (C_K * h ^ 2) ^ 3 = C_K ^ 3 * (h ^ 3 * h ^ 3) := by ring have h4 : C_K ^ 3 * (h ^ 3 * h ^ 3) ≤ C_K ^ 3 * (h₀ ^ 3 * h ^ 3) := by refine mul_le_mul_of_nonneg_left ?_ (by positivity) exact mul_le_mul_of_nonneg_right hh3 (by positivity) calc |kappa * δ h| ^ 3 = |kappa| ^ 3 * |δ h| ^ 3 := h1 _ ≤ |kappa| ^ 3 * (C_K ^ 3 * (h₀ ^ 3 * h ^ 3)) := by refine mul_le_mul_of_nonneg_left ?_ (by positivity) calc |δ h| ^ 3 ≤ (C_K * h ^ 2) ^ 3 := h2 _ = C_K ^ 3 * (h ^ 3 * h ^ 3) := h3 _ ≤ C_K ^ 3 * (h₀ ^ 3 * h ^ 3) := h4 _ = |kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 * h ^ 3 := by ring calc |(n : ℝ) * Real.arsinh (kappa * δ h / n) - kappa * δ h| ≤ |kappa * δ h| ^ 3 / (6 * (n : ℝ) ^ 2) := sourced_ratio_cubic_error n hn (kappa * δ h) _ ≤ (|kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 * h ^ 3) / (6 * (n : ℝ) ^ 2) := by have hden : (0 : ℝ) ≤ (6 * (n : ℝ) ^ 2)⁻¹ := by positivity rw [div_eq_mul_inv, div_eq_mul_inv] exact mul_le_mul_of_nonneg_right hnum hden _ = |kappa| ^ 3 * C_K ^ 3 * h₀ ^ 3 / (6 * (n : ℝ) ^ 2) * h ^ 3 := by ringThe sourced ratio family satisfies the admissibility predicate with an explicit constant. sourced_ratio_isAdmissible · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.leanMODEL sourcedAction · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean
/-- 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 iThe coupling term is a constitutive model choice, not a derived consequence of the bare recognition ledger. sourcedAction · IndisputableMonolith/Gravity/SevenGaps/HingeStationarityCore.lean