n_resolutions_time
plain-language theorem explainer
The theorem establishes linear scaling of resolution time with the number of resolutions under the Recognition Science Bremermann bound. Modelers of information limits or debt resolution in fundamental physics cite it when extending single-cycle costs to multiple events. The proof is a short tactic sequence that unfolds the bound definition, confirms the octave is nonzero via octave_is_eight, and cancels via field_simp.
Claim. For any natural number $n$, if $B$ is the Bremermann bound (one resolution per octave cycle) and $O$ the octave period, then $n/B = n·O$.
background
Recognition Science sets the Bremermann limit from the minimum 8-tick cycle required for one debt resolution, with no faster physical process allowed. The module defines bremermannBound as 1/octave (in units where the tick is 1) and octave as the fundamental period. Upstream results include octave_is_eight proving octave equals 8, Constants.octave setting the period to 8·tick, and MusicalScale.octave giving the ratio 2; the module doc states the bound is tighter than the classical mass-energy version because each resolution uses a φ^5-energy quantum.
proof idea
Unfold bremermannBound to expose the reciprocal of octave. Introduce the auxiliary fact octave ≠ 0 by rewriting with octave_is_eight and normalizing to 8. Apply field_simp to clear the division and obtain the identity.
why it matters
The declaration supplies the direct proportionality needed to scale time costs for n resolutions inside the Q7 Bremermann framework, resting on the eight-tick octave (T7) and the definition bremermannBound = 1/octave. It follows the module doc-comment that multiple resolutions require proportionally more time and supports downstream estimates of information-processing rates. No used-by edges are recorded, leaving open whether it will be invoked in explicit time-bound derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.