demandedRate_pos
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.