inner_arg_tendsto_one
plain-language theorem explainer
The theorem establishes that 1 + 1/(φ N) tends to 1 as real N tends to positive infinity. Researchers deriving the high-N limit of Recognition Science Shannon capacity cite it to confirm the finite-N correction vanishes. The proof composes standard filter-tendsto rules for scaling by a positive constant, inversion at infinity, and addition of a constant sequence.
Claim. As $N → ∞$, $1 + 1/(φ N) → 1$, where φ is the golden-ratio constant from the Recognition Science constants bundle.
background
The ShannonHighNLimit module deepens the high-N analysis of Shannon capacity by showing the RS correction log₂(1 + 1/(φ N)) tends to zero, recovering the classical log₂ N. The inner argument is built from the correction definition that sets the additive term to 1/(φ N) for positive N. Constants is the structure that bundles the positive real φ together with other CPM parameters. This step rests on the PrimitiveDistinction axioms that derive four structural conditions from seven independent axioms and on the ContinuumBridge identification of the Laplacian action with the simplicial ledger.
proof idea
The tactic proof begins by invoking Constants.phi_pos. It applies Filter.Tendsto.const_mul_atTop to obtain that φ N tends to infinity, then Filter.Tendsto.inv_tendsto_atTop to produce the reciprocal tending to zero. A rewrite equates the reciprocal to the explicit 1/(φ N) form. Addition of the constant sequence 1 then yields the limit at 1.
why it matters
The lemma is invoked directly by correction_RS_tendsto_zero to conclude that the full RS correction tends to zero and by shannonHighNLimitCert to certify the high-N limit. It completes the explicit recovery of classical Shannon capacity in the Recognition Science framework, consistent with the forcing chain through T5 J-uniqueness and T6 phi fixed point. The module falsifier is a finite-N coding experiment in which measured capacity deviates from log₂(1 + 1/(φ N)) by more than 1 percent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.