demandedRate_pos
The positivity of the demanded recognition rate is established for positive mass and time parameters. Researchers modeling the transition to bandwidth saturation in Recognition Science cite this result when verifying that Newtonian demands can exceed the holographic ceiling. The proof is a one-line term that invokes the standard positivity of real division.
claimLet $M > 0$ and $T > 0$ be real numbers. Then the demanded rate, defined as the ratio of the mass parameter to the time parameter, satisfies $0 < M/T$.
background
This theorem appears in the Recognition Bandwidth module, which connects the holographic bound on information content to the per-bit recognition cost k_R = ln(φ) and the eight-tick cadence of the recognition operator. The module defines recognition bandwidth as R_max = S_holo / (k_R · 8τ₀) = A / (4ℓ_P² · ln(φ) · 8τ₀), imposing a hard ceiling on ledger throughput. Upstream results include the definition of fundamental periods T from Breath1024 and the active edge count A from IntegrationGap, which together set the temporal and spatial scales for the bound.
proof idea
The proof is a one-line wrapper that applies the div_pos lemma from the real numbers library to the hypotheses that M and T are positive.
why it matters in Recognition Science
This positivity result supports the definition of the bandwidth-saturated regime in the same module, where Newtonian dynamics demand more recognition events than the holographic bound permits, triggering ILG activation. It contributes to the core definitions needed for the unification of holographic bounds with recognition costs and the eight-tick cadence. No downstream uses are recorded yet.
scope and limits
- Does not specify the physical interpretation of the mass and time parameters beyond positivity.
- Does not derive the demanded rate from Newtonian dynamics.
- Does not compare the demanded rate to the holographic bandwidth bound.
- Does not handle cases where parameters are non-positive.
formal statement (Lean)
157theorem demandedRate_pos {M T : ℝ} (hM : 0 < M) (hT : 0 < T) :
158 0 < demandedRate M T :=
proof body
Term-mode proof.
159 div_pos hM hT
160
161/-! ## §6. Saturation Predicate -/
162
163/-- A gravitating system is **bandwidth-saturated** when its Newtonian dynamics
164 demand more recognition events per unit time than the holographic bound permits.
165
166 This is the regime where ILG must activate. -/