pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Information.QuantumChannelCapacityFromPhi

show as:
view Lean formalization →

QuantumChannelCapacityFromPhi supplies the phi-ladder finite-N correction factor for quantum channel capacity at input-symbol-count N. Information theorists working in Recognition Science cite it when deriving capacity bounds for discrete channels in RS-native units. The module introduces the correction term together with lemmas on its positivity and monotonicity, all resting on the imported Constants module.

claimThe finite-N correction factor correction(N) for quantum channel capacity C_N in the phi-ladder model, together with the properties correction_pos, correction_strictly_decreasing, and correction_le_inv.

background

The module sits in the Information domain and imports the RS time quantum tau_0 = 1 tick from Constants. It defines the correction function that adjusts quantum channel capacity for finite input symbol count N on the phi-ladder. Supporting lemmas establish that the correction is positive, strictly decreasing, and bounded above by its inverse.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the correction machinery required by QuantumChannelCapacityCert and quantumChannelCapacityCert. It fills the finite-N adjustment step in the Information domain, linking directly to the phi-ladder scaling that underlies capacity limits in the Recognition Science framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)