module module high

`IndisputableMonolith.Engineering.ZMatchedTransceiverMesh`

This module defines per-node throughput as a dimensionless reference quantity together with pairwise latency and aggregate throughput functions for Z-matched transceiver meshes. Network engineers applying Recognition Science to communication systems would cite these when sizing mesh capacities. The module consists of a collection of definitions and elementary monotonicity properties built directly on the imported Constants and Cost modules.

claimThe module introduces the per-node throughput $T$ (dimensionless reference), pairwise latency functions, and aggregate throughput $A$ with its zero, positivity, strict monotonicity, and doubling properties.

background

The module resides in the Engineering domain and imports Constants, which supplies the fundamental RS time quantum with doc-comment stating 'The fundamental RS time quantum (RS-native). τ₀ = 1 tick.', together with the Cost module. It defines sibling objects including T_node for per-node throughput, latency_per_pair, aggregateThroughput with its listed variants, and pairwiseLatency with its constant property. These quantities operate in RS-native units where throughput remains dimensionless.

proof idea

This is a definition module. The listed siblings consist of direct definitions of throughput and latency quantities together with short lemmas establishing zero, positivity, strict monotonicity, and doubling properties via the imported constants.

why it matters in Recognition Science

The module supplies the engineering primitives for per-node throughput that would feed parent theorems on network performance and capacity in the Recognition framework. It translates RS constants into transceiver-mesh models, supporting application of the phi-ladder and J-cost to practical communication design. No direct used_by edges are recorded.

scope and limits

Does not derive numerical throughput values for concrete hardware.
Does not model electromagnetic propagation or interference.
Does not incorporate modulation, coding, or error rates.
Does not address multi-hop routing beyond pairwise terms.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (16)

def T_node L39
theorem T_node_pos L41
def latency_per_pair L45
theorem latency_per_pair_pos L47
def aggregateThroughput L53
theorem aggregateThroughput_zero L55
theorem aggregateThroughput_succ L58
theorem aggregateThroughput_pos L62
theorem aggregateThroughput_strict_mono L67
theorem aggregateThroughput_double L74
def pairwiseLatency L82
theorem pairwiseLatency_constant L84
theorem pairwiseLatency_pos L87
structure ZMatchedTransceiverMeshCert L92
def zMatchedTransceiverMeshCert L101
theorem mesh_one_statement L113