module module high

`IndisputableMonolith.Engineering.ZMatchedTransceiverMesh`

Module defines per-node throughput T_node as dimensionless reference for Z-matched transceiver meshes. Engineers modeling RS-native communication networks cite these for latency and aggregate throughput. Content is definitions plus monotonicity properties built directly on Constants and Cost imports.

claimPer-node throughput $T_ {rm node}$ (dimensionless reference). Latency per pair and aggregate throughput functions satisfy aggregateThroughput(0) = 0, positivity, strict monotonicity, and doubling under node addition.

background

Module resides in the Engineering domain. Imports fundamental time quantum τ₀ = 1 tick from Constants and cost structures from Cost. Definitions center on T_node for reference throughput, pairwiseLatency as position-dependent delay, and aggregateThroughput with supporting lemmas for zero value, successor cases, positivity, strict monotonicity, and doubling.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Supplies engineering primitives for transceiver mesh throughput. Aligns with T5 J-uniqueness and T7 eight-tick octave via dimensionless phi-consistent references. Feeds no listed downstream theorems but enables network models consistent with D = 3 dimensions.

scope and limits

Does not incorporate specific hardware parameters or explicit Z-matching equations.
Does not address time-dependent dynamics or propagation beyond pairwise latency.
Does not connect to mass formulas, Berry thresholds, or alpha band constraints.

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